1  // LinearFeeFunction is the abstract model of our fee function. We use one
  2  // here to indicate that only one of them exists in our model. Our model will
  3  // use time to drive this single instance.
  4  one sig LinearFeeFunction {
  5    // startFeeRate is the starting fee rate of our model.
  6    var startingFeeRate: Int, 
  7    
  8    // endingFeeRate is the max fee rate we'll be ending out once the deadline
  9    // has been reached.
 10    var endingFeeRate: Int,
 11  
 12    // currentFeeRate is the current fee rate we're using to bump the
 13    // transaction.
 14    var currentFeeRate: Int,
 15  
 16    // width is the number of blocks between the starting block height and the
 17    // deadline height.
 18    var width: Int,
 19  
 20    // position is the number of between the current height and the starting
 21    // height. This is our progress as time passes, we'll increment by a single
 22    // block.
 23    var position: Int, 
 24  
 25    // deltaFeeRate is the fee rate time step in msat/kw that we'll take each
 26    // time we update our progress (scaled by position). In this simplified
 27    // model, this will always be 1.
 28    var deltaFeeRate: Int,
 29  } {
 30    // Here we have some _implicit_ facts attached to the definition of
 31    // LinearFeeFunction. These ensure that we always get well formed traces in
 32    // our model.
 33  
 34    // position must be positive, and can never exceed our width. In our model,
 35    // position is the amount of blocks that have elapsed, and width is the conf
 36    // target.
 37    position >= 0
 38    position <= width
 39  
 40    // startingFeeRate must be positive.
 41    startingFeeRate > 0 
 42  
 43    // currentFeeRate must be positive.
 44    currentFeeRate > 0 
 45  
 46    // endingFeeRate must be positive.
 47    endingFeeRate > 0 
 48  
 49    // deltaFeeRate always just increments by one. This simplifies our model, as
 50    // Alloy doesn't support arithmetics with large numbers easily.
 51    deltaFeeRate = 1
 52  }
 53  
 54  // ActiveFeeFunctions is a signature for the set of all active fee functions.
 55  // This is used to properly initialize a fee function before it can be used
 56  // elsewhere in the model.
 57  sig ActiveFeeFunctions {
 58     // activeFuncs is the set of all active functions.
 59     var activeFuncs: set LinearFeeFunction
 60  }
 61  
 62  // feeFuncInitZeroValues is a basic fact that capture the semantics of fee
 63  // functions and initialization.
 64  fact feeFuncInitZeroValues {
 65     // If a function isn't in the set of active functions, then its position
 66     // must be zero.
 67     all f: LinearFeeFunction | 
 68         f not in ActiveFeeFunctions.activeFuncs => f.position = 0
 69  }
 70  
 71  // feeFuncSetStartsEmpty captures a basic fact that at the very start of the
 72  // trace, there are no active fee functions. There're no temporal operators in
 73  // this fact, so it only applies to the very start of the trace.
 74  fact feeFuncSetStartsEmpty {
 75    no activeFuncs
 76  }
 77  
 78  // init is a predicate to initialize the params of the fee function.
 79  pred init[f: LinearFeeFunction, maxFeeRate, startFeeRate: Int, confTarget: Int] {
 80    // We only want to initiate once, so we'll have a guard that only proceeds if
 81    // f isn't in the set of active functions.
 82    f not in ActiveFeeFunctions.activeFuncs
 83  
 84    // The starting rate and the ending rate shouldn't be equal to each other. 
 85    maxFeeRate != startFeeRate
 86    maxFeeRate > startFeeRate
 87  
 88    // If the conf target is zero, then we'll just jump straight to max params.
 89    confTarget = 0 implies {
 90      f.startingFeeRate' = maxFeeRate
 91      f.endingFeeRate' = maxFeeRate
 92      f.currentFeeRate' = maxFeeRate
 93      f.position' = 0
 94      f.width' = confTarget
 95      f.deltaFeeRate' = 1
 96      ActiveFeeFunctions.activeFuncs' = ActiveFeeFunctions.activeFuncs + f
 97    } else {
 98      // Otherwise, we'll be starting from a position that we can use to drive
 99      // forward the system. 
100      confTarget != 0 
101  
102      f.startingFeeRate' = startFeeRate
103      f.currentFeeRate' = startFeeRate
104      f.endingFeeRate' = maxFeeRate
105      f.width' = confTarget
106      f.position' = 0
107  
108      // Our delta fee rate is just always 1, we'll take a single step towards
109      // the final solution at a time. 
110      f.deltaFeeRate' = 1
111      ActiveFeeFunctions.activeFuncs' = ActiveFeeFunctions.activeFuncs + f
112    }
113  }
114  
115  // increment is a predicate that implements our fee bumping routine.
116  pred increment[f: LinearFeeFunction] {
117    // Update our fee rate to take into account our new position.  Increase our
118    // position by one, as a single block has past.
119    increase_fee_rate[f, f.position.add[1]]
120  }
121  
122  // increase_fee_rate takes a new position, and our fee function, then updates
123  // based on this relationship:
124  //  feeRate = startingFeeRate + position * delta.
125  //	- width: deadlineBlockHeight - startingBlockHeight
126  //	- delta: (endingFeeRate - startingFeeRate) / width
127  //	 - position: currentBlockHeight - startingBlockHeight
128  pred increase_fee_rate[f : LinearFeeFunction, newPosition: Int] {
129    // Update the position of the model in the next timestep.
130    f.position' = newPosition
131  
132    // Ensure that our position hasn't passed our width yet. This is an error
133    // scenario in the original Go code.
134    f.position' <= f.width
135  
136    // Our new position is the distance between the 
137    f.currentFeeRate' = fee_rate_at_position[f, newPosition]
138   
139    f.startingFeeRate' = f.startingFeeRate
140    f.endingFeeRate' = f.endingFeeRate
141    f.width' = f.width
142    f.deltaFeeRate' = f.deltaFeeRate
143    activeFuncs' = activeFuncs
144  }
145  
146  // fee_rate_at_position computes the new fee rate based on an updated position.
147  fun fee_rate_at_position[f: LinearFeeFunction, p: Int]: Int {
148    // If the position is equal to the width, then we'll go straight to the max
149    // fee rate.
150    p >= f.width.sub[1] => f.endingFeeRate
151    //p >= f.width => f.endingFeeRate -- NOTE: Uncomment this to re-introduce the original bug.
152    else 
153      // Otherwise, we'll do the fee rate bump.
154      let deltaRate = f.deltaFeeRate,
155          newFeeRate = f.currentFeeRate.add[deltaRate] |
156  
157          // If the new fee rate would exceed the ending rate, then we clamp it
158          // to our max fee rate.  Otherwise we return our normal fee rate.
159          newFeeRate > f.endingFeeRate => f.endingFeeRate else newFeeRate
160  }
161  
162  // fee_bump is a predicate that executes a fee bump step.
163  pred fee_bump[f: LinearFeeFunction] {
164    // We use a guard to ensure that fee_bump can only be called after init
165    // (which will add the func to the set of active funcs).
166    f in ActiveFeeFunctions.activeFuncs
167  
168    increment[f]
169  }
170  
171  // stutter does nothing. This just assigns all variables to themselves, this is
172  // useful in a trace to allow it to noop.
173  pred stutter[f: LinearFeeFunction] {
174    // No change in any of our variables.
175    f.startingFeeRate' = f.startingFeeRate
176    f.endingFeeRate' = f.endingFeeRate
177    f.currentFeeRate' = f.currentFeeRate
178    f.position' = f.position 
179    f.width' = f.width
180    f.deltaFeeRate' = f.deltaFeeRate
181    activeFuncs' = activeFuncs
182  }
183  
184  // Event is used to generate easier to follow traces. These these enums are
185  // events that correspond to the main state transition predicates above.
186  //
187  // See this portion of documentation for more information on this idiom:
188  // https://haslab.github.io/formal-software-design/modelling-tips/index.html#an-idiom-to-depict-events.
189  enum Event { Stutter, Init, FeeBump }
190  
191  // stutter is a derived relation that's populated whenever a stutter event
192  // happens.
193  fun stutter : set Event -> LinearFeeFunction {
194    { e: Stutter, f: LinearFeeFunction | stutter[f] }
195  }
196  
197  // init is a derived relation that's populated whenever an init event happens.
198  fun init : Event -> LinearFeeFunction -> Int -> Int -> Int {
199    { e: Init, f: LinearFeeFunction, m: Int, s: Int, c: Int | init[f, m, s, c] }
200  }
201  
202  // fee_bump is a derived relation that's populated whenever a fee_bump event
203  // happens.
204  fun fee_bump : Event -> LinearFeeFunction {
205    { e: FeeBump, f: LinearFeeFunction | fee_bump[f] }
206  }
207  
208  // events is our final derived relation that stores all the possible event
209  // types.
210  fun events : set Event {
211    stutter.LinearFeeFunction + init.Int.Int.Int.LinearFeeFunction + fee_bump.LinearFeeFunction
212  }
213  
214  // traces is a fact to ensure that we always get one of the above events in
215  // traces we generate.
216  fact traces {
217    always some events
218  }
219  
220  // init_traces builds on the fact traces above, and also asserts that there's
221  // always at least one init event (to ensure proper initialization).
222  fact init_traces {
223    eventually (one init)
224  }
225  
226  // fee_bump_happens ensures that within our trace, there's always at least a
227  // single fee bump event.
228  fact fee_bump_happens {
229    eventually (some fee_bump)
230  }
231  
232  
233  // valid_fee_rates is a fact that ensures that the ending fee rate is always
234  // greater than the starting fee rate.
235  fact valid_fee_rates {
236    all f: LinearFeeFunction | f.endingFeeRate > f.startingFeeRate
237  }
238  
239  // init_correctness is an assertion that makes sure once an init event happens,
240  // then we have the function in our set of active functions.
241  assert init_correctness {
242    all f: LinearFeeFunction | {
243      eventually (some init) implies 
244        eventually f in ActiveFeeFunctions.activeFuncs
245    }
246  }
247  
248  // check init_correctness
249  
250  // init_always_happens is a trivial assertion that ensures that an init
251  // eventually happens in a trace.
252  assert init_always_happens {
253     eventually (some init)
254  }
255  
256  // check init_always_happens
257  
258  // init_then_fee_bump asserts that within our trace, we'll always have at least
259  // a single fee bump event after an init.
260  assert init_then_fee_bump {
261    eventually (some init => some fee_bump)
262  }
263  
264  // check init_then_fee_bump
265  
266  // bump_to_completion is a predicate that can be used to force fee_bump events
267  // to be emitted until we're right at our confirmation deadline.
268  pred bump_to_completion {
269    always (all f: LinearFeeFunction | f.position < f.width => eventually (some fee_bump))
270  }
271  
272  // bump_to_final_block is a predicate that can be used to force fee_bump events
273  // to be emitted until we're one block before our confirmation deadline.
274  pred bump_to_final_block {
275    always (all f: LinearFeeFunction | f.position < f.width.sub[1] => eventually (some fee_bump))
276  }
277  
278  // req_num_blocks_to_conf is a predicate that can be used to restrict the
279  // functions in a fact to a given confirmation target.
280  pred req_num_blocks_to_conf[n: Int] {
281    all f: LinearFeeFunction | f.width = n
282  }
283  
284  // req_starting_fee_rate is a predicate that can be used to restrict functions
285  // in a fact to a given starting fee rate.
286  pred req_starting_fee_rate[n: Int] {
287    all f: LinearFeeFunction | f.startingFeeRate = n
288  }
289  
290  // max_fee_rate_before_deadline is the main assertion in this model. This
291  // captures a model violation for our fee function, but only if the line in
292  // fee_rate_at_position is uncommented.
293  //
294  // In this assertion, we declare that if we have a fee function that has a conf
295  // target of 4 (we want a few fee bumps), and we bump to the final block, then
296  // at that point our current fee rate is the ending fee rate. In the original
297  // code, assertion isn't upheld, due to an off by one error.
298  assert max_fee_rate_before_deadline {
299    always req_num_blocks_to_conf[4] => bump_to_final_block => eventually (
300      all f: LinearFeeFunction | f.position = f.width.sub[1] => f.currentFeeRate = f.endingFeeRate
301    )
302  }
303  
304  check max_fee_rate_before_deadline
305  
306  run {
307    // Our default command just shows a trace that has at least 4 fee bump
308    // events.
309    always req_num_blocks_to_conf[4] 
310    always bump_to_completion
311  }