1  # Linear Fee Function
 2  
 3  This is a model of the default [Linear Fee
 4  Function](https://github.com/lightningnetwork/lnd/blob/b7c59b36a74975c4e710a02ea42959053735402e/sweep/fee_function.go#L66-L109)
 5  fee bumping mechanism in lnd.
 6  
 7  This model was inspired by a bug fix, due to an off-by-one error in the
 8  original code: https://github.com/lightningnetwork/lnd/issues/8741.
 9  
10  The bug in the original code was fixed in this PR:
11  https://github.com/lightningnetwork/lnd/pull/8751.
12  
13  
14  ## Model & Bug Fix Walk-through
15  
16  The model includes an assertion that captures the essence of the bug:
17  `max_fee_rate_before_deadline`:
18  ```alloy
19  // max_fee_rate_before_deadline is the main assertion in this model. This
20  // captures a model violation for our fee function, but only if the line in
21  // fee_rate_at_position is uncommented.
22  //
23  // In this assertion, we declare that if we have a fee function that has a conf
24  // target of 4 (we want a few fee bumps), and we bump to the final block, then
25  // at that point our current fee rate is the ending fee rate. In the original
26  // code, assertion isn't upheld, due to an off by one error.
27  assert max_fee_rate_before_deadline {
28    always req_num_blocks_to_conf[4] => bump_to_final_block => eventually (
29      all f: LinearFeeFunction | f.position = f.width.sub[1] &&
30                                 f.currentFeeRate = f.endingFeeRate
31    )
32  }
33  ```
34  
35  We can modify the model to find the bug described in the original issue.
36    1. First, we modify the model by forcing a `check` on the
37       `max_fee_rate_before_deadline` assertion: 
38      ```alloy
39      check max_fee_rate_before_deadline
40      ```
41  
42    2. Next, we'll modify the `fee_rate_at_position` predicate to re-introduce
43       the off by one error:
44      ```alloy
45      p >= f.width => f.endingFeeRate // -- NOTE: Uncomment this to re-introduce the original bug.
46      ```
47  
48  If we hit `Execute` in the Alloy Analyzer, then we get a counter example:
49  ![Counter Example](counter-example.png)
50  
51  
52  We can hit `Show` in the analyzer to visualize it: 
53  ![Counter Example Show](counter-example-show.png)
54  
55  We can see that even though we're one block (`position`) before the deadline
56  (`width`), our fee rate isn't at the ending fee rate yet.
57  
58  If we modify the `fee_rate_at_position` to have the correct logic: 
59  ```alloy
60  p >= f.width.sub[1] => f.endingFeeRate
61  ```
62  
63  Then Alloy is unable to find any counterexamples:
64  ![Correct Model](fixed-model.png)