The realize tactic

The tactic is available inside Cslib.WordRAM, or after open Cslib.WordRAM or open scoped Cslib.WordRAM. Importing this module alone does not activate its syntax.

realize proves a goal Realizes B p input output safe work for a memory client p. It walks the client syntax, unfolding definitions, with one rule per form:

• bind: compose the component work at the actual reply and next memory, absorbing fixed control work. After each bind the live words are the previous ones followed by the answer's encoding (WordEncoding); realize keeps this layout itself.
• pure: Realizes.pure₀, with each result word certified by a GlueComputable proof assembled from the closure rules of CslibFrontier.Computability.WordRAM.Glue: projections, constants, and the exact- or standard-basis arithmetic and bitwise operations. Conditional values, natural minima/maxima and Boolean decisions are lifted to paid branches, including inside returned constructors; only the selected alternative contributes fit and definedness conditions.
• the four memory queries: Realizes.read, write, alloc and allocDirty.
• a method with a local Realizes certificate: Realizes.reindex, selecting its arguments from live words before unfolding its implementation. Computed arguments are first staged by certified glue using the method's input encoding; the method's work is retained.
• if on natural =, ≠, <, ≤, > or ≥, combined with ¬, ∧ and ∨: Realizes.branch (branch₀ for zero component work), retaining short-circuiting. Named guards unfold to these forms.
• match on an optional word or word pair: the client equals the branch on its presence tag (Realizes.congr, proved by cases).
• iterate step D n a: Realizes.iterateRuntime, after adapting D and any captured live words to the whole environment. The source and reached-state domain and iterationWork are transported back to the client's original loop.
• boundedWhile G step D n a: Realizes.whileBounded. The guard G D r may be a = b, a < b, a > b, a ≠ 0 (tested as 0 < a), or a + 1 ≤ b (tested as a < b), with any decidability instance, over the live words and the state's words. An operand independent of the state is computed before the loop. The cutoff n is a ghost bound and is not computed. The certificate is transported to the client's guard, step and D (boundedWhile_congr, whileSafe_imp), so the loop's domain is whileSafe G step … in the client's terms, under the loop's valid history (Realizes.consequence_valid), ready for whileSafe_of_measure.

Operands are located among the live words by definitional equality. An operand that is not a live word is first computed by an inserted pure, preserving the program by a checked equality.

Exact subtraction, division and remainder add their definedness conditions to the visible domain. The common glue envelope is the maximum of every intermediate value; realize proves that it fits from the fit of the live words, from the domain, and from the fit of the values it cannot derive, which become the visible fit conditions. A value is derived when another fitting value dominates it, for example a - b and b by a, or the summands by a sum.

Fixed glue and finite control work is absorbed (Realizes.mono_mul). Called methods retain their work; binds sum it and branches select only the reached alternative's work. Loops retain iterationWork or whileWork, including one control unit per reached iteration. A zero-work body that begins with a query keeps the existing query-paid rule (iterate₀ or while₀). Intermediate domains and grades are stated in the client's own terms, with the replies of earlier queries written as s.mem a, s.frontier, updated memories, or the interpreter's result of a called method; a loop contributes its iterationSafe or whileSafe domain.

After composition, realize introduces w d s hwords hmem h: the word width, the environment, memory, input fits, memory well-formedness and the goal's domain. Nonzero generated work also adds the client's valid history as hv. It splits conjunctions and ifs of the domain, then leaves the generated work's comparison with the requested budget under the same entry assumptions. Zero work and definitionally matching budgets close automatically. Local method certificates are tried in context order; the remaining rule selection follows the client syntax, without searching for bounds. An unsupported form is reported with its subterm. A called method whose arguments are not all live words first stages its whole encoded argument with a charged pure step. This also supports custom input encodings without requiring a WordEncoding instance for the method's argument type.

realize [certificate₁, …] first adds the supplied proof terms as local facts in list order, then runs the same tactic. Existing local certificates retain priority.

Each certificate is stated for the client form as written, with its domain in the client's terms (certify), so certificates compose syntactically. A bind's continuation domain is stated at the first client's reply and next memory in closed form (Realizes.bind₀_of_run), not at the interpreter's run. The kernel checks, locally at each form, that the rule's statement agrees.

Main definitions

• realize: the tactic.

Word glue

Realization

def Cslib.WordRAM.tacticRealize : Lean.ParserDescr

Prove Realizes B p input output safe work, leaving genuine fit, domain and budget conditions in the entry context, with valid history also available for nonzero generated work.

def Cslib.WordRAM.«tacticRealize[_,,]» : Lean.ParserDescr

Supply method certificates as local facts before running realize.