Derived OP₀–OP₁₀ evaluator

Fuel-indexed evalPaper from the opcode equations at main.tex:1054–1076 (rejects OP₁₁; refines evalN).

def Nock.evalPaper : Nat → Noun → Noun → Option Noun

*[subject formula], fuel-indexed, paper fragment only (OP₀..OP₁₀ + cons). Identical to evalN except an OP₁₁ head (op = 11) is an unknown opcode and crashes, matching the paper's opHeadOk (op < 11) and the small-step machine runProgram.

Equations

• One or more equations did not get rendered due to their size.
• Nock.evalPaper 0 x✝¹ x✝ = none
• Nock.evalPaper n.succ x✝ (Nock.Noun.atom a) = none
• Nock.evalPaper fuel.succ x✝ ((b.cell c).cell d) = match Nock.evalPaper fuel x✝ (b.cell c), Nock.evalPaper fuel x✝ d with | some l, some r => some (l.cell r) | x, x_1 => none
• Nock.evalPaper fuel.succ x✝ ((Nock.Noun.atom 0).cell (Nock.Noun.atom ax)) = Nock.Noun.slot ax x✝
• Nock.evalPaper fuel.succ x✝ ((Nock.Noun.atom 0).cell tail) = none
• Nock.evalPaper fuel.succ x✝ ((Nock.Noun.atom 1).cell tail) = some tail
• Nock.evalPaper fuel.succ x✝ ((Nock.Noun.atom 2).cell (b.cell c)) = match Nock.evalPaper fuel x✝ b, Nock.evalPaper fuel x✝ c with | some sb, some sc => Nock.evalPaper fuel sb sc | x, x_1 => none
• Nock.evalPaper fuel.succ x✝ ((Nock.Noun.atom 2).cell tail) = none
• Nock.evalPaper fuel.succ x✝ ((Nock.Noun.atom 3).cell tail) = Option.map Nock.Noun.wut (Nock.evalPaper fuel x✝ tail)
• Nock.evalPaper fuel.succ x✝ ((Nock.Noun.atom 4).cell tail) = (Nock.evalPaper fuel x✝ tail).bind Nock.Noun.lus
• Nock.evalPaper fuel.succ x✝ ((Nock.Noun.atom 5).cell (b.cell c)) = match Nock.evalPaper fuel x✝ b, Nock.evalPaper fuel x✝ c with | some sb, some sc => some (sb.tis sc) | x, x_1 => none
• Nock.evalPaper fuel.succ x✝ ((Nock.Noun.atom 5).cell tail) = none
• Nock.evalPaper fuel.succ x✝ ((Nock.Noun.atom 6).cell tail) = none
• Nock.evalPaper fuel.succ x✝ ((Nock.Noun.atom 7).cell (b.cell c)) = match Nock.evalPaper fuel x✝ b with | some sb => Nock.evalPaper fuel sb c | none => none
• Nock.evalPaper fuel.succ x✝ ((Nock.Noun.atom 7).cell tail) = none
• Nock.evalPaper fuel.succ x✝ ((Nock.Noun.atom 8).cell (b.cell c)) = match Nock.evalPaper fuel x✝ b with | some sb => Nock.evalPaper fuel (sb.cell x✝) c | none => none
• Nock.evalPaper fuel.succ x✝ ((Nock.Noun.atom 8).cell tail) = none
• Nock.evalPaper fuel.succ x✝ ((Nock.Noun.atom 9).cell tail) = none
• Nock.evalPaper fuel.succ x✝ ((Nock.Noun.atom 10).cell tail) = none
• Nock.evalPaper fuel.succ x✝ ((Nock.Noun.atom op).cell tail) = none

theorem Nock.evalPaper_succ {n : Nat} {s form r : Noun} (h : evalPaper n s form = some r) : evalPaper (n + 1) s form = some r

Fuel monotonicity (single step) for evalPaper (same shape as evalN_succ).

theorem Nock.evalPaper_mono {n m : Nat} {s form r : Noun} (hle : n ≤ m) (h : evalPaper n s form = some r) : evalPaper m s form = some r

Fuel monotonicity for evalPaper.

theorem Nock.evalPaper_deterministic {n m : Nat} {s form r₁ r₂ : Noun} (h₁ : evalPaper n s form = some r₁) (h₂ : evalPaper m s form = some r₂) : r₁ = r₂

evalPaper is a partial function (output uniqueness). Two successful paper-fragment evaluations of the same subject/formula, at any fuel budgets, return the same noun.

theorem Nock.evalPaper_le_evalN {n : Nat} {s form r : Noun} (h : evalPaper n s form = some r) : evalN n s form = some r

evalPaper refines evalN. Every paper-fragment evaluation is a standard Nock evaluation with the same result: evalPaper and evalN differ only where evalN fires OP₁₁ (which evalPaper crashes on). Proof: functional induction; every clause is identical except OP₁₁, where evalPaper returns none so the hypothesis is absurd.