-
Notifications
You must be signed in to change notification settings - Fork 2.1k
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Merge pull request #8943 from Roasbeef/alloy-linear-fee-model
docs/alloy-models: add new folder for Alloy models along w/ model for Linear Fee Function bug fix
- Loading branch information
Showing
6 changed files
with
425 additions
and
0 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,50 @@ | ||
# Alloy Models | ||
|
||
This folder houses "lightweight formal models" written using the | ||
[Alloy](https://alloytools.org/about.html) model checker and language. | ||
|
||
Compared to typical formal methods, Alloy is a _bounded_ model checker, | ||
considered a [lightweight | ||
method](https://en.wikipedia.org/wiki/Formal_methods#:~:text=As%20an%20alternative,Tools.%5B31) | ||
to formal analysis. Lightweight formal methods are easier to use than fully | ||
fledged formal methods as rather than attempting to prove the that a model is | ||
_always_ correct (for all instances), they instead operate on an input of a set | ||
of bounded parameters and iterations. These models can then be used to specify | ||
a model, then use the model checker to find counter examples of a given | ||
assertion. If a counter example can't be found, then the model _may_ be valid. | ||
|
||
Alloy in particular is an expressive, human readable language for formal | ||
modeling. It also has a nice visualizer which can show counter examples, aiding | ||
in development and understanding. | ||
|
||
Alloy is useful as when used during upfront software design (or even after the | ||
fact), one can create a formal model of a software system to gain better | ||
confidence in the _correctness_ of a system. The model can then be translated | ||
to code. Many times, writing the model (either before or after the code) can | ||
help one to better understand a given software system. Models can also be used | ||
to specify protocols in p2p systems such as Lightning (as it [supports temporal | ||
logic](https://alloytools.org/alloy6.html#:~:text=Meaning%20of%20temporal%20connectives), | ||
which enables creation of state machines and other interactive transcripts), | ||
serving as a complement to a normal prosed based specification. | ||
|
||
## How To Learn Alloy? | ||
|
||
We recommend the following places to learn Alloy: | ||
* [The online tutorial for Alloy 4.0](https://alloytools.org/about.html): | ||
* Even though this is written with Alloy 4.0 (which doesn't support | ||
temporal logic), the tutorial is very useful, as it introduces | ||
fundamental concept of Alloy, using an accessible example based on a file | ||
system. | ||
|
||
* [Alloy Docs](https://alloy.readthedocs.io/en/latest/index.html): | ||
* This serves as a one stop shop for reference to the Alloy language. It | ||
explains all the major syntax, tooling, and also how to model time in | ||
Alloy. | ||
|
||
* [Formal Software Design with Alloy 6](https://haslab.github.io/formal-software-design/index.html): | ||
* A more in depth tutorial which uses Alloy 6. This tutorial covers more | ||
advanced topics such as [event | ||
reification](https://alloytools.discourse.group/t/modelling-a-state-machine-in-electrum-towards-alloy-6/88). | ||
This tutorial is also very useful, as it includes examples for how to | ||
model interactions in a p2p network, such as one peer sending a message | ||
to another. |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,64 @@ | ||
# Linear Fee Function | ||
|
||
This is a model of the default [Linear Fee | ||
Function](https://github.com/lightningnetwork/lnd/blob/b7c59b36a74975c4e710a02ea42959053735402e/sweep/fee_function.go#L66-L109) | ||
fee bumping mechanism in lnd. | ||
|
||
This model was inspired by a bug fix, due to an off-by-one error in the | ||
original code: https://github.com/lightningnetwork/lnd/issues/8741. | ||
|
||
The bug in the original code was fixed in this PR: | ||
https://github.com/lightningnetwork/lnd/pull/8751. | ||
|
||
|
||
## Model & Bug Fix Walk-through | ||
|
||
The model includes an assertion that captures the essence of the bug: | ||
`max_fee_rate_before_deadline`: | ||
```alloy | ||
// max_fee_rate_before_deadline is the main assertion in this model. This | ||
// captures a model violation for our fee function, but only if the line in | ||
// fee_rate_at_position is uncommented. | ||
// | ||
// In this assertion, we declare that if we have a fee function that has a conf | ||
// target of 4 (we want a few fee bumps), and we bump to the final block, then | ||
// at that point our current fee rate is the ending fee rate. In the original | ||
// code, assertion isn't upheld, due to an off by one error. | ||
assert max_fee_rate_before_deadline { | ||
always req_num_blocks_to_conf[4] => bump_to_final_block => eventually ( | ||
all f: LinearFeeFunction | f.position = f.width.sub[1] && | ||
f.currentFeeRate = f.endingFeeRate | ||
) | ||
} | ||
``` | ||
|
||
We can modify the model to find the bug described in the original issue. | ||
1. First, we modify the model by forcing a `check` on the | ||
`max_fee_rate_before_deadline` assertion: | ||
```alloy | ||
check max_fee_rate_before_deadline | ||
``` | ||
|
||
2. Next, we'll modify the `fee_rate_at_position` predicate to re-introduce | ||
the off by one error: | ||
```alloy | ||
p >= f.width => f.endingFeeRate // -- NOTE: Uncomment this to re-introduce the original bug. | ||
``` | ||
|
||
If we hit `Execute` in the Alloy Analyzer, then we get a counter example: | ||
![Counter Example](counter-example.png) | ||
|
||
|
||
We can hit `Show` in the analyzer to visualize it: | ||
![Counter Example Show](counter-example-show.png) | ||
|
||
We can see that even though we're one block (`position`) before the deadline | ||
(`width`), our fee rate isn't at the ending fee rate yet. | ||
|
||
If we modify the `fee_rate_at_position` to have the correct logic: | ||
```alloy | ||
p >= f.width.sub[1] => f.endingFeeRate | ||
``` | ||
|
||
Then Alloy is unable to find any counterexamples: | ||
![Correct Model](fixed-model.png) |
Loading
Sorry, something went wrong. Reload?
Sorry, we cannot display this file.
Sorry, this file is invalid so it cannot be displayed.
Loading
Sorry, something went wrong. Reload?
Sorry, we cannot display this file.
Sorry, this file is invalid so it cannot be displayed.
Loading
Sorry, something went wrong. Reload?
Sorry, we cannot display this file.
Sorry, this file is invalid so it cannot be displayed.
Oops, something went wrong.