Kontrol Glossary page

[reekamaharaj]

Page with definitions/lists of rules, commands

Nodes can also be:

• 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.

[reekamaharaj]

Needed definitions/descriptions:

• vacuous assumption
• EVM.halt
• EVM.step
• EVM.call
• EVM.jumpi-true
• EVM.success
• -break-every-step