mockProgram
plain-language theorem explainer
The mock program definition supplies a constant BALANCE operation for cycle evaluation examples in the VM. It is referenced by cycle report constructions for smoke tests of commit boundaries. The definition is implemented as a direct constant function with no additional logic or computation.
Claim. Define the mock program $M$ by $M(x) = s$ where $s$ is the state with opcode BALANCE, for arbitrary input $x$.
background
The VM module models program execution under a conservative COMMIT boundary predicate with the v2 flag. Programs are functions from inputs to opcode states, and the mock supplies a baseline augmented state for examples. It depends on the for structure from UniversalForcingSelfReference, which records all structural properties that would be required of a meta-realization instance and proves that the meta-theorem already supplies each one.
proof idea
The definition is a direct one-line construction of the constant function returning the BALANCE opcode.
why it matters
This definition supports the cycleReport smoke-test for tooling, which evaluates lCycle on the mock and reports window index, winJ, and commit event. It provides simple inputs for testing cycle windows in the VM commit module and touches the self-reference axioms in the forcing chain by supplying baseline cases.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.