vacuous - A node that arises from a vacuous assumption, often resulting from something like vm.assume(false).
stuck - A non-terminal leaf node in which the prover is unable to proceed further due to a lack of knowledge on how to proceed. This situation often requires a simplification lemma to resolve.
Rules:
terminal_rules - rules that indicate the end of program execution, such as EVM.halt or EVM.step in case of -break-every-step
cut_point_rules - rules that create a new node when reached, such as EVM.call, EVM.jumpi.true, EVM.success, etc.
Page with definitions/lists of rules, commands
Nodes can also be:
vacuous
- A node that arises from avacuous assumption
, often resulting from something like vm.assume(false).stuck
- A non-terminal leaf node in which the prover is unable to proceed further due to a lack of knowledge on how to proceed. This situation often requires a simplification lemma to resolve.Rules:
terminal_rules
- rules that indicate the end of program execution, such asEVM.halt
orEVM.step
in case of-break-every-step
cut_point_rules
- rules that create a new node when reached, such asEVM.call
,EVM.jumpi.true
,EVM.success
, etc.