docs/alloy-models: add new folder for Alloy models along w/ model for Linear Fee Function bug fix #8943
Conversation
Roasbeef
added
testing
|
Important Review skippedAuto reviews are limited to specific labels. Labels to auto review (1)
Please check the settings in the CodeRabbit UI or the You can disable this status message by setting the Thank you for using CodeRabbit. We offer it for free to the OSS community and would appreciate your support in helping us grow. If you find it useful, would you consider giving us a shout-out on your favorite social media? TipsChatThere are 3 ways to chat with CodeRabbit:
Note: Be mindful of the bot's finite context window. It's strongly recommended to break down tasks such as reading entire modules into smaller chunks. For a focused discussion, use review comments to chat about specific files and their changes, instead of using the PR comments. CodeRabbit Commands (invoked as PR comments)
Additionally, you can add CodeRabbit Configuration File (
|
|
How does this improve over fuzzing? At least for the fee function bug it seems a fuzz test would be simpler and more readable. |
I don't think one can necessarily compare them like that. This is a simplified formal specification of the fee bumping algorithm, it exists independent of the code implementing the algorithm, but can be used to gain more confidence in the algorithm by leveraging the Alloy model checker. Fuzzing can help us find bugs in our code, formal modeling can help us find defects in our design.
Consider if this was written before/during the original implementation, the model checker would've found a counter example before the code was even written. Fuzzing operates on an entirely different level of abstraction, you can't fuzz the design of a system. Formal methods are yet another tool in our tool box which includes: fuzzing, property based tests, mutation testing, etc, etc. I recommend checking out these blog posts to help answer the "why" behind my motivations:
Zooming out: we have some components in the LN spec that after all this time, are still somewhat poorly understood, lack comprehensive test vectors, and/or have insufficient specifications. Tools like Alloy can allow us to elevate the spec further, capturing the desired semantics in a formal model, with the ability to rule out certain invariants, and also serve as another guide for implementers. One such example is the channel state machine, which is pretty much the cornerstone of LN interactions. We can use tools such as Alloy to better specify a model of the channel state machine, which can increase our understanding as a hole, and potentially find new gaps in the channel state machine beyond what's commonly known by implementors. Alloy supports temporal logic, so we can model both expected execution, and also error cases. Consider the following fragment that could be used to verify invariants around sending empty sigs in the protocol: assert empty_sig_leads_to_error {
always no pending_changes
eventually (some commit_dance)
eventually (some empty_sig_errors)
}From here I plan to write a trivial model for the way ping/ping works in the protocol to get a better feel of how to best model message passing. Then I plan to write a model for the As far as readability goes, IMO Alloy is the most readable of any of the formal specification languages I've come across. Compare the syntax in this PR to TLA+: VARIABLES counter, pc
vars == << counter, pc >>
ProcSet == (Threads)
Init == (* Global variables *)
/\ counter = 0
/\ pc = [self \in ProcSet |-> "IncCounter"]
IncCounter(self) == /\ pc[self] = "IncCounter"
/\ counter' = counter + 1
/\ pc' = [pc EXCEPT ![self] = "Done"]
thread(self) == IncCounter(self)
(* Allow infinite stuttering to prevent deadlock on termination. *)
Terminating == /\ \A self \in ProcSet: pc[self] = "Done"
/\ UNCHANGED vars
Next == (\E self \in Threads: thread(self))
\/ Terminating
Spec == Init /\ [][Next]_varsIt may look unfamiliar to you, but that's because you don't yet have exposure to it, just as any new langauge. |
| // bump_to_completion is a predicate that can be used to force fee_bump events | ||
| // to be emitted until we're right at our confirmation deadline. | ||
| pred bump_to_completion { | ||
| always (all f: LinearFeeFunction | f.position < f.width => eventually (some fee_bump)) |
There was a problem hiding this comment.
Do you need the eventually here? can't you just use set here to capture the no bump case. Or are you trying to say that we must eventually get at least one fee_bump every time position < width?
There was a problem hiding this comment.
If I remove the eventually then even just the run example at the very end fails. However, It looks non-essential for bump_to_final_block, as that doesn't have a noop case of no fee bump as you've noted.
Would need to experiment more, but I think removing it for bump_to_completion fails as if you have an init, then stutter f.position < f.width is true, but we can have another stutter right after that, so in the exact time step that it's true, we don't yet have a fee_bump.
Roasbeef
force-pushed
the
alloy-linear-fee-model
branch
from
3a49d3e
to
50053c8
Compare
|
Posted revision 3: https://reviewable.io/reviews/lightningnetwork/lnd/8943 |
| @@ -0,0 +1,50 @@ | |||
| # Alloy Models | |||
Yep! Depending at which point in the design/implementation/testing/review cycle we insert things in, it can help to refine thinking of a new system, or even help model concurrent interactions with other systems. The blog I linked above even has an example where they use it to model a DB migration, and find some issues with the design in general. This post also has good suggestion on how to gradually integrate into your workflow: https://www.hillelwayne.com/post/using-formal-methods/ Part of the learning curve is figuring out which level of abstraction is sufficient for the model. Eg: if we were trying to model the channel state machine, we could add things like: payment hashes, commit txn construction, signs, etc. Or, we can have the model operate at a higher level, and use a more abstract notion of a inbox/queue for new changes and acked/unacked set, etc. One other example that pops to mind would be some of the repeated bug fixes and refactoring we've done w.r.t the router's payment/HTLC dispatch. So how to handle timeouts, updating the main state, etc, etc. Nice part is that it can also idrectly help to generate diagrams of everything via the visualizer. The visualizer also has a lot of settings to make what it generates more useful w/ colors, diff shapes, focusing on certain aspect, etc. etc |
If you haven't already, it'll also be useful to download the Analyzer and run the model in it. Throughput the process I either had Vim open and then used the Analyzer to run stuff (using the reload), or just ran things directly in the Analyzer. It also has a REPL like interface that can be used to debug stuff or just see how it would evaluate certain expressions/statements. |
In this commit, we add a model for the linear fee function we use in lnd for fee bumping. This models can be used to reproduce the issue reported in lightningnetwork#8741, and can also be shown that that bug fix resolves a counter example found by the model checker.
|
Also right now CI doesn't do much, but in the future we can have it run the Java binary for Alloy on the models checked in to make sure they don't have obvious counter examples and have valid syntax, etc. |
Roasbeef
force-pushed
the
alloy-linear-fee-model
branch
from
50053c8
to
9aa7e75
Compare
|
@ProofOfKeags: review reminder |
Alloy Models
This PR adds a new Alloy Model, which is a method of "lightweight formal models"
written using the Alloy model checker and language.
Compared to typical formal methods, Alloy is a bounded model checker,
considered a lightweight method 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 re 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, which enables creation of state machines and other interactive transcripts),
serving as a complement to a written specification.
Linear Fee Function
In this PR, we add the first Alloy model, for the Linear Fee
Function fee bumping mechanism in lnd.
This model was inspired by a bug fix, due to an off-by-one error in the
original code: #8741.
The bug in the original code was fixed in this PR:
#8751.
Model & Bug Fix Walk-through
The model includes an assertion that captures the essence of the bug:
max_fee_rate_before_deadline:We can modify the model to find the bug described in the original issue.
First, we modify the model by forcing a
checkon themax_fee_rate_before_deadlineassertion:alloy check max_fee_rate_before_deadlineNext, we'll modify the
fee_rate_at_positionpredicate to re-introducethe off by one error:
alloy p >= f.width => f.endingFeeRate // -- NOTE: Uncomment this to re-introduce the original bug.If we hit
Executein the Alloy Analyzer, then we get a counter example:We can hit
Showin the analyzer to visualize it: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_positionto have the correct logic:Then Alloy is unable to find any counterexamples:
