Executable evaluation-trace certificates

Nock.Verb.run (Nock/Verb.lean) iterates the small-step next to a result noun but discards the intermediate states. This module adds runTrace, which returns the full list of visited verbs, and proves it is a certificate of the paper's evaluation trace (Def:eval_trace, main.tex:1114–1128; transition checker Algorithm:Transition_Function, main.tex:1633–1666):

• runTrace_traceOf — the emitted list is a consistent trace of the input (TraceOf);
• runTrace_complete — it is complete (ends at a terminal/⊥ verb);
• runTrace_adjacent_nockCheck — every adjacent pair is accepted by the two-verb checker Nock (NockCheck _ (some _) = true);
• runTrace_run — its last verb carries exactly the run result;
• runTrace_unique — the emitted trace is independent of the fuel budget.

runTrace_unique is the executable realization of Thm:deterministic_Trace (main.tex:1156–1158): because next is a function, the trace from a verb is forced, so any two successful runs coincide. These are Lean consistency theorems, not numbered paper theorems.

def Nock.Verb.runTrace : Nat → Verb → Option (List Verb)

Fuel-indexed iteration of next that records every visited verb. some T iff evaluation reached a terminal/⊥ state within the budget (so T ends there); none iff fuel ran out.

Equations

• Nock.Verb.runTrace 0 x✝ = none
• Nock.Verb.runTrace fuel.succ x✝ = match x✝.next with | some v' => Option.map (fun (T : List Nock.Verb) => x✝ :: T) (Nock.Verb.runTrace fuel v') | none => some [x✝]

def Nock.Verb.runTraceProgram (fuel : Nat) (subject formula : Noun) : Option (List Verb)

Run a Nock program *[subject, formula], recording the full evaluation trace.

Equations

• Nock.Verb.runTraceProgram fuel subject formula = Nock.Verb.runTrace fuel (Nock.Verb.program subject formula)

The trace is a consistent, complete trace of the input

theorem Nock.Verb.runTrace_spec (fuel : Nat) (v : Verb) (T : List Verb) : runTrace fuel v = some T → v.TraceOf T ∧ Complete T

runTrace produces a consistent, complete trace headed at the input. Bundles the three facts carried through the fuel recursion: head = v, Consistent, and Complete.

theorem Nock.Verb.runTrace_traceOf {fuel : Nat} {v : Verb} {T : List Verb} (h : runTrace fuel v = some T) : v.TraceOf T

The emitted list is a consistent trace of the input (TraceOf, main.tex:1114–1118).

theorem Nock.Verb.runTrace_complete {fuel : Nat} {v : Verb} {T : List Verb} (h : runTrace fuel v = some T) : Complete T

The emitted trace is complete (main.tex:1122): it ends at a terminal or ⊥ verb.

Every adjacent pair is accepted by the transition checker Nock

def Nock.Verb.AdjNockCheck : List Verb → Prop

Every consecutive pair of a list is accepted by the paper's two-verb checker Nock (NockCheck _ (some _) = true). Mirrors the shape of Consistent.

Equations

• Nock.Verb.AdjNockCheck [] = True
• Nock.Verb.AdjNockCheck [head] = True
• Nock.Verb.AdjNockCheck (a :: b :: rest) = (a.NockCheck (some b) = true ∧ Nock.Verb.AdjNockCheck (b :: rest))

theorem Nock.Verb.adjNockCheck_of_consistent (T : List Verb) : Consistent T → AdjNockCheck T

A consistent trace is accepted pairwise by the transition checker: every Step a b (next a = some b) makes NockCheck a (some b) = true (nockCheck_eq_true_iff).

def Nock.Verb.adjNockCheckB : List Verb → Bool

Executable two-verb transition checker over a whole trace: Bool-valued reflection of AdjNockCheck, so the certificate can actually be run (and extracted).

Equations

• Nock.Verb.adjNockCheckB [] = true
• Nock.Verb.adjNockCheckB [head] = true
• Nock.Verb.adjNockCheckB (a :: b :: rest) = (a.NockCheck (some b) && Nock.Verb.adjNockCheckB (b :: rest))

theorem Nock.Verb.adjNockCheckB_iff (T : List Verb) : adjNockCheckB T = true ↔ AdjNockCheck T

adjNockCheckB decides AdjNockCheck: the executable checker returns true iff every adjacent pair passes the paper's transition checker Nock.

theorem Nock.Verb.runTrace_adjacent_nockCheck {fuel : Nat} {v : Verb} {T : List Verb} (h : runTrace fuel v = some T) : AdjNockCheck T

Every adjacent pair of the emitted trace passes the transition checker Nock. The certificate is checkable by the paper's Algorithm:Transition_Function.

theorem Nock.Verb.runTrace_adjNockCheckB {fuel : Nat} {v : Verb} {T : List Verb} (h : runTrace fuel v = some T) : adjNockCheckB T = true

The executable checker accepts every emitted trace. Running adjNockCheckB on the output of runTrace returns true — the certificate is machine-checkable, not just a Prop.

The last verb carries the run result

theorem Nock.Verb.runTrace_run (fuel : Nat) (v : Verb) (T : List Verb) : runTrace fuel v = some T → ∃ (w : Verb), T.getLast? = some w ∧ run fuel v = w.result

The emitted trace's last verb carries exactly the run result. run fuel v is the result (terminal noun, or none on crash) of the trace's final verb.

The emitted trace is independent of the fuel budget

theorem Nock.Verb.runTrace_unique (fuel₁ fuel₂ : Nat) (v : Verb) (T₁ T₂ : List Verb) : runTrace fuel₁ v = some T₁ → runTrace fuel₂ v = some T₂ → T₁ = T₂

The emitted trace is unique. Because next is a function, any two successful runs of runTrace on the same verb — at any fuel budgets — produce the same trace. This is the executable form of Thm:deterministic_Trace (main.tex:1156–1158).

theorem Nock.Verb.runTrace_final_edge {fuel : Nat} {v : Verb} {T : List Verb} (h : runTrace fuel v = some T) : ∃ (w : Verb), T.getLast? = some w ∧ (w.isTerminal = true ∨ w.NockCheck none = true)

The completion edge is accounted for. The emitted trace's last verb is either terminal (a valid completion, main.tex:1123) or crashes, and in the crash case the transition to ⊥ passes the checker (NockCheck w none = true, main.tex:1124, 1644, 1650). Together with runTrace_adjacent_nockCheck, every edge of the certificate — including the final ⊥ edge on a crash — is Nock-checked; there is no unchecked step.

theorem Nock.Verb.runTraceProgram_certificate {fuel : Nat} {subject formula : Noun} {T : List Verb} (h : runTraceProgram fuel subject formula = some T) : (program subject formula).TraceOf T ∧ Complete T ∧ AdjNockCheck T ∧ ∃ (w : Verb), T.getLast? = some w ∧ (w.isTerminal = true ∨ w.NockCheck none = true)

runTraceProgram emits a certified trace of the program. Its head is the program verb, it is consistent and complete, every adjacent step passes the checker Nock, and the final state is terminal or has a crash edge accepted by the checker.