Agreement with the standard evaluator

den is a compositional Nat-level denotation of verbs using evalN at * nodes. den_step proves one-step preservation; runProgram_sound is small-step-to-big-step agreement.

The compositional denotation den of a verb

def Nock.Verb.den : Nat → Verb → Option Noun

Compositional denotation: * nodes use evalN; operator nodes apply the matching Nock.Noun operator; ⊥-nodes are cons; leaves are atoms.

Equations

• One or more equations did not get rendered due to their size.
• Nock.Verb.den x✝ (Nock.Verb.leaf k) = some (Nock.Noun.atom k)
• Nock.Verb.den 0 (Nock.Verb.node a a_1 a_2) = none
• Nock.Verb.den fuel.succ (Nock.Verb.node Nock.Action.null l r) = match Nock.Verb.den fuel l, Nock.Verb.den fuel r with | some a, some b => some (a.cell b) | x, x_1 => none
• Nock.Verb.den fuel.succ (Nock.Verb.node Nock.Action.star l r) = match Nock.Verb.den fuel l, Nock.Verb.den fuel r with | some a, some b => Nock.evalN fuel a b | x, x_1 => none
• Nock.Verb.den fuel.succ (Nock.Verb.node Nock.Action.slot l r) = match Nock.Verb.den fuel l, Nock.Verb.den fuel r with | some (Nock.Noun.atom ax), some b => Nock.Noun.slot ax b | x, x_1 => none
• Nock.Verb.den fuel.succ (Nock.Verb.node Nock.Action.equal l r) = match Nock.Verb.den fuel l, Nock.Verb.den fuel r with | some a, some b => some (a.tis b) | x, x_1 => none
• Nock.Verb.den fuel.succ (Nock.Verb.node Nock.Action.edit l (Nock.Verb.leaf a)) = none
• Nock.Verb.den fuel.succ (Nock.Verb.node Nock.Action.wut l r) = none

den is fuel-monotone (same shape as evalN_succ)

theorem Nock.Verb.den_succ {n : Nat} {v : Verb} {r : Noun} (h : den n v = some r) : den (n + 1) v = some r

theorem Nock.Verb.den_mono {n m : Nat} {v : Verb} {r : Noun} (hle : n ≤ m) (h : den n v = some r) : den m v = some r

(A) den of a terminal noun-verb is the noun itself

theorem Nock.Verb.den_ofNoun (n : Noun) (fuel : Nat) : n.size ≤ fuel → den fuel (ofNoun n) = some n

theorem Nock.Verb.den_terminal (v : Verb) (fuel : Nat) : v.isTerminal = true → v.noun.size ≤ fuel → den fuel v = some v.noun

Terminal verbs denote their underlying noun (given adequate fuel).

(B) The initial program verb denotes exactly what evalN computes

theorem Nock.Verb.den_program (s f : Noun) (fuel : Nat) (hs : s.size ≤ fuel) (hf : f.size ≤ fuel) : den (fuel + 1) (program s f) = evalN fuel s f

den of the initial program verb *[s, f] equals evalN s f.

theorem Nock.Verb.den_iff_evalN (s f r : Noun) : (∃ (fuel : Nat), den fuel (program s f) = some r) ↔ ∃ (fuel : Nat), evalN fuel s f = some r

den of *[s, f] and evalN s f define the same partial function.

Small-step to big-step simulation

def Nock.Verb.Den (v : Verb) (x : Noun) : Prop

A verb has a denotation when its evaluator succeeds with some finite fuel.

Equations

• v.Den x = ∃ (fuel : Nat), Nock.Verb.den fuel v = some x

def Nock.Verb.Ev (a b x : Noun) : Prop

Natural-number Nock evaluation succeeds with some finite fuel.

Equations

• Nock.Verb.Ev a b x = ∃ (fuel : Nat), Nock.evalN fuel a b = some x

theorem Nock.Verb.den_pair {l r : Verb} {a b : Noun} (hl : l.Den a) (hr : r.Den b) : ∃ (f : Nat), den f l = some a ∧ den f r = some b

theorem Nock.Verb.den_triple {a b c : Verb} {va vb vc : Noun} (ha : a.Den va) (hb : b.Den vb) (hc : c.Den vc) : ∃ (f : Nat), den f a = some va ∧ den f b = some vb ∧ den f c = some vc

theorem Nock.Verb.Den_leaf {k : Nat} {x : Noun} : (leaf k).Den x ↔ x = Noun.atom k

theorem Nock.Verb.Den_null {l r : Verb} {x : Noun} : (node Action.null l r).Den x ↔ ∃ (a : Noun), ∃ (b : Noun), x = a.cell b ∧ l.Den a ∧ r.Den b

theorem Nock.Verb.Den_star {l r : Verb} {x : Noun} : (node Action.star l r).Den x ↔ ∃ (a : Noun), ∃ (b : Noun), l.Den a ∧ r.Den b ∧ Ev a b x

theorem Nock.Verb.Den_slot {l r : Verb} {x : Noun} : (node Action.slot l r).Den x ↔ ∃ (ax : Nat), ∃ (b : Noun), l.Den (Noun.atom ax) ∧ r.Den b ∧ Noun.slot ax b = some x

theorem Nock.Verb.Den_equal {l r : Verb} {x : Noun} : (node Action.equal l r).Den x ↔ ∃ (a : Noun), ∃ (b : Noun), l.Den a ∧ r.Den b ∧ x = a.tis b

theorem Nock.Verb.Den_minus {l r : Verb} {x : Noun} : (node Action.minus l r).Den x ↔ ∃ (b : Noun), r.Den b ∧ (l.Den (Noun.atom 3) ∧ x = b.wut ∨ l.Den (Noun.atom 4) ∧ b.lus = some x)

theorem Nock.Verb.Den_edit_node {l : Verb} {b : Action} {nw od : Verb} {x : Noun} : (node Action.edit l (node b nw od)).Den x ↔ ∃ (ax : Nat), ∃ (n : Noun), ∃ (o : Noun), l.Den (Noun.atom ax) ∧ nw.Den n ∧ od.Den o ∧ Noun.edit ax n o = some x

theorem Nock.Verb.Den_edit_leaf {l : Verb} {k : Nat} {x : Noun} : ¬(node Action.edit l (leaf k)).Den x

theorem Nock.Verb.Den_wut {l r : Verb} {x : Noun} : ¬(node Action.wut l r).Den x

theorem Nock.Verb.ev2 {s1 f1 x1 s2 f2 x2 : Noun} (h1 : Ev s1 f1 x1) (h2 : Ev s2 f2 x2) : ∃ (f : Nat), evalN f s1 f1 = some x1 ∧ evalN f s2 f2 = some x2

theorem Nock.Verb.ev3 {s1 f1 x1 s2 f2 x2 s3 f3 x3 : Noun} (h1 : Ev s1 f1 x1) (h2 : Ev s2 f2 x2) (h3 : Ev s3 f3 x3) : ∃ (f : Nat), evalN f s1 f1 = some x1 ∧ evalN f s2 f2 = some x2 ∧ evalN f s3 f3 = some x3

theorem Nock.Verb.EvN_autocons {subj hb hc d x : Noun} : Ev subj ((hb.cell hc).cell d) x ↔ ∃ (l : Noun), ∃ (r : Noun), x = l.cell r ∧ Ev subj (hb.cell hc) l ∧ Ev subj d r

theorem Nock.Verb.EvN_op0 {subj tail x : Noun} : Ev subj ((Noun.atom 0).cell tail) x ↔ ∃ (ax : Nat), tail = Noun.atom ax ∧ Noun.slot ax subj = some x

theorem Nock.Verb.EvN_op1 {subj tail x : Noun} : Ev subj ((Noun.atom 1).cell tail) x ↔ x = tail

theorem Nock.Verb.EvN_op2 {subj tail x : Noun} : Ev subj ((Noun.atom 2).cell tail) x ↔ ∃ (hb : Noun), ∃ (hc : Noun), ∃ (sb : Noun), ∃ (sc : Noun), tail = hb.cell hc ∧ Ev subj hb sb ∧ Ev subj hc sc ∧ Ev sb sc x

theorem Nock.Verb.EvN_op3 {subj tail x : Noun} : Ev subj ((Noun.atom 3).cell tail) x ↔ ∃ (y : Noun), Ev subj tail y ∧ x = y.wut

theorem Nock.Verb.EvN_op4 {subj tail x : Noun} : Ev subj ((Noun.atom 4).cell tail) x ↔ ∃ (y : Noun), Ev subj tail y ∧ y.lus = some x

theorem Nock.Verb.EvN_op5 {subj tail x : Noun} : Ev subj ((Noun.atom 5).cell tail) x ↔ ∃ (hb : Noun), ∃ (hc : Noun), ∃ (sb : Noun), ∃ (sc : Noun), tail = hb.cell hc ∧ Ev subj hb sb ∧ Ev subj hc sc ∧ x = sb.tis sc

theorem Nock.Verb.EvN_op7 {subj tail x : Noun} : Ev subj ((Noun.atom 7).cell tail) x ↔ ∃ (hb : Noun), ∃ (hc : Noun), ∃ (sb : Noun), tail = hb.cell hc ∧ Ev subj hb sb ∧ Ev sb hc x

theorem Nock.Verb.EvN_op8 {subj tail x : Noun} : Ev subj ((Noun.atom 8).cell tail) x ↔ ∃ (hb : Noun), ∃ (hc : Noun), ∃ (sb : Noun), tail = hb.cell hc ∧ Ev subj hb sb ∧ Ev (sb.cell subj) hc x

theorem Nock.Verb.EvN_op10 {subj tail x : Noun} : Ev subj ((Noun.atom 10).cell tail) x ↔ ∃ (ax : Nat), ∃ (c : Noun), ∃ (d : Noun), ∃ (new : Noun), ∃ (old : Noun), tail = ((Noun.atom ax).cell c).cell d ∧ Ev subj c new ∧ Ev subj d old ∧ Noun.edit ax new old = some x

theorem Nock.Verb.EvN_op6 {subj tail x : Noun} : Ev subj ((Noun.atom 6).cell tail) x ↔ ∃ (b : Noun), ∃ (c : Noun), ∃ (d : Noun), ∃ (cv : Noun), tail = b.cell (c.cell d) ∧ Ev subj b cv ∧ (cv = Noun.atom 0 ∧ Ev subj c x ∨ cv = Noun.atom 1 ∧ Ev subj d x)

theorem Nock.Verb.EvN_op9 {subj tail x : Noun} : Ev subj ((Noun.atom 9).cell tail) x ↔ ∃ (ax : Nat), ∃ (c : Noun), ∃ (core : Noun), ∃ (arm : Noun), tail = (Noun.atom ax).cell c ∧ Ev subj c core ∧ Noun.slot ax core = some arm ∧ Ev core arm x

helpers: determinism of den, terminal denotation, ofNoun facts

theorem Nock.Verb.den_det {v : Verb} {r1 r2 : Noun} (h1 : v.Den r1) (h2 : v.Den r2) : r1 = r2

theorem Nock.Verb.Den_terminal_iff {v : Verb} {x : Noun} (ht : v.isTerminal = true) : v.Den x ↔ x = v.noun

theorem Nock.Verb.ofNoun_noun (n : Noun) : (ofNoun n).noun = n

theorem Nock.Verb.ofNoun_terminal (n : Noun) : (ofNoun n).isTerminal = true

theorem Nock.Verb.Den_ofNoun_iff {n x : Noun} : (ofNoun n).Den x ↔ x = n

well-formedness: edit nodes never carry a pending r-child

def Nock.Verb.editOk : Verb → Bool

Every edit node has a non-pending right child, recursively throughout the verb.

Equations

• (Nock.Verb.leaf a).editOk = true
• (Nock.Verb.node Nock.Action.edit l r).editOk = (!r.isPending && l.editOk && r.editOk)
• (Nock.Verb.node a l r).editOk = (true && l.editOk && r.editOk)

theorem Nock.Verb.editOk_ofNoun (n : Noun) : (ofNoun n).editOk = true

theorem Nock.Verb.editOk_program (s f : Noun) : (program s f).editOk = true

theorem Nock.Verb.editOk_null_eq {l r : Verb} : (node Action.null l r).editOk = (l.editOk && r.editOk)

theorem Nock.Verb.editOk_star_eq {l r : Verb} : (node Action.star l r).editOk = (l.editOk && r.editOk)

theorem Nock.Verb.editOk_children {a : Action} {l r : Verb} (h : (node a l r).editOk = true) : l.editOk = true ∧ r.editOk = true

slot equation lemmas

theorem Nock.Verb.slot_one {n : Noun} : Noun.slot 1 n = some n

theorem Nock.Verb.slot_two {a b : Noun} : Noun.slot 2 (a.cell b) = some a

theorem Nock.Verb.slot_three {a b : Noun} : Noun.slot 3 (a.cell b) = some b

theorem Nock.Verb.slot_two_atom {k : Nat} : Noun.slot 2 (Noun.atom k) = none

theorem Nock.Verb.slot_three_atom {k : Nat} : Noun.slot 3 (Noun.atom k) = none

theorem Nock.Verb.lus_atom {k : Nat} : (Noun.atom k).lus = some (Noun.atom (k + 1))

theorem Nock.Verb.slot_pair_some {p q : Nat} (m : Nat) (v : Noun) : Noun.slot m ((Noun.atom p).cell (Noun.atom q)) = some v → m = 1 ∨ m = 2 ∨ m = 3

On a pair of atoms [p,q], only axes 1,2,3 are addressable.

STEP-LOCAL: a reduce on an operator-ready node preserves Den

theorem Nock.Verb.den_local_opReady {sub r₀ : Verb} {x : Noun} (hor : sub.opReady = true) (hr : sub.reduce = some r₀) : sub.Den x ↔ r₀.Den x

STEP-LOCAL: a reduce (opcode redex) on an in-D node preserves Den

theorem Nock.Verb.den_local_opcode {sub r₀ : Verb} {x : Noun} (hd : sub.inOpcodeDomain = true) (hr : sub.reduce = some r₀) : sub.Den x ↔ r₀.Den x

STEP-CONG: den-congruence for splicing a den-equivalent redex back via replaceAt

inductive Nock.Verb.Rel : Verb → Verb → Prop

Structural relation: w is v with the subtree at one pending node replaced by a Den-equivalent verb. base is restricted to pending nodes so it can never sit at an edit node's ⊥ r-child (where den reads structure), the one place congruence needs care.

• leaf {k : Nat} : (Verb.leaf k).Rel (Verb.leaf k)
• base {v w : Verb} : v.isPending = true → (∀ (x : Noun), v.Den x ↔ w.Den x) → v.Rel w
• cong {a : Action} {l l' r r' : Verb} : l.Rel l' → r.Rel r' → (node a l r).Rel (node a l' r')

theorem Nock.Verb.Rel.refl (v : Verb) : v.Rel v

theorem Nock.Verb.replaceAux_counter (i : Nat) (new v : Verb) (c : Nat) : (replaceAux i new v c).fst = (v.enum c).fst

theorem Nock.Verb.replaceAux_rel (i : Nat) (r₀ v : Verb) (c : Nat) : (∀ (sub : Verb), findAt i (v.enum c).snd = some sub → sub.isPending = true ∧ ∀ (x : Noun), sub.Den x ↔ r₀.Den x) → v.Rel (replaceAux i r₀ v c).snd

theorem Nock.Verb.Rel_den (n : Nat) (v w : Verb) : v.noun.size ≤ n → v.Rel w → v.editOk = true → ∀ (x : Noun), v.Den x ↔ w.Den x

STEP-CONG (den-preservation of Rel). If Rel v w and v is edit-well-formed, then v and w have the same denotation.

editOk is preserved by next (the invariant discharging den_step's hypothesis)

theorem Nock.Verb.editOk_reduce {sub r₀ : Verb} (hr : sub.reduce = some r₀) (hok : sub.editOk = true) : r₀.editOk = true

theorem Nock.Verb.editOk_edit_cond {l r : Verb} (h : (node Action.edit l r).editOk = true) : r.isPending = false

theorem Nock.Verb.editOk_editN_eq {l r : Verb} : (node Action.edit l r).editOk = (!r.isPending && l.editOk && r.editOk)

theorem Nock.Verb.isPending_replaceAux (i : Nat) (r₀ v : Verb) (c : Nat) : c ≠ i → (replaceAux i r₀ v c).snd.isPending = v.isPending

theorem Nock.Verb.editOk_replaceAux (i : Nat) (r₀ : Verb) (hr0 : r₀.editOk = true) (v : Verb) (c : Nat) : v.editOk = true → (∀ (s : Verb), findAt i (v.enum c).snd = some s → s.isPending = true) → (replaceAux i r₀ v c).snd.editOk = true

theorem Nock.Verb.editOk_enum (v : Verb) (c : Nat) : v.editOk = true → ∀ (p : Nat × Verb), p ∈ (v.enum c).snd → p.snd.editOk = true

STEP-LOCAL combined, den_step, and the editOk invariant threaded through

theorem Nock.Verb.den_local {sub r₀ : Verb} {x : Noun} (hd : sub.inDomain = true) (hr : sub.reduce = some r₀) : sub.Den x ↔ r₀.Den x

theorem Nock.Verb.editOk_next {v v' : Verb} (h : v.next = some v') (hok : v.editOk = true) : v'.editOk = true

theorem Nock.Verb.den_step {v v' : Verb} (hwf : v.editOk = true) (h : v.next = some v') {r : Noun} : (∃ (fuel : Nat), den fuel v = some r) ↔ ∃ (fuel : Nat), den fuel v' = some r

theorem Nock.Verb.run_sound {v : Verb} {r : Noun} (fuel : Nat) : v.editOk = true → run fuel v = some r → ∃ (f : Nat), den f v = some r

theorem Nock.Verb.runProgram_sound {s f r : Noun} {fuel : Nat} (h : runProgram fuel s f = some r) : ∃ (fuel' : Nat), evalN fuel' s f = some r

edit/slot characterization — the %10 soundness relation

`Noun.edit ax new old` (the `#` operator, opcode 10's structural write, `main.tex:1071`,
`1587–1607`) replaces the subtree of `old` at axis `ax` with `new`.  The paper's
`NockVMROM` excludes `%10` entirely, so this relation is stated nowhere in the manuscript;
it is the noun-level soundness relation an `%edit`-table arithmetization must prove
against.  Two **necessary** properties an `%edit`-table arithmetization must discharge
(sufficiency / uniqueness of `res` is not proved here):

  * `slot_edit_eq`      — **read-back**: on a successful edit, reading axis `ax` of the
                          result yields `new`.
  * `slot_edit_sibling` — **sibling carry**: every off-path sibling encountered from `ax`
                          to the root is carried unchanged from `old` (the property whose
                          absence lets a fraudulent proof mutate an unrelated subtree).

Both are over the fuel-free `Noun.slot`/`Noun.edit` (`Algorithm:Noun_Operators`,
`main.tex:1537–1607`).  `Noun.edit` recurses bottom-up — it rebuilds each parent by
pairing `new` with the sibling read from the *original* `old`, then edits the halved
(parent) axis.  Read-back uses strong induction on `ax`; full sibling carry then follows by
induction over the siblings encountered by that same `ax / 2` walk. 

def Nock.Verb.siblingAxis (ax : Nat) : Nat

The sibling axis of ax = a+2: its co-child under the shared parent ax / 2. Even axes are left children (sibling ax+1); odd axes are right children (sibling ax-1). This is exactly the sibAxis local of Noun.edit's a+2 branch.

Equations

• Nock.Verb.siblingAxis ax = if (ax % 2 == 0) = true then ax + 1 else ax - 1

inductive Nock.Verb.SiblingOf : Nat → Nat → Prop

SiblingOf ax sib says that sib is an off-path sibling encountered while following ax toward the root: either the immediate sibling of ax, or a sibling of one of ax's proper ancestors. For example, both axes 5 and 3 are siblings of target axis 4.

• immediate (a : Nat) : SiblingOf (a + 2) (siblingAxis (a + 2))
• ancestor (a : Nat) {sib : Nat} : SiblingOf ((a + 2) / 2) sib → SiblingOf (a + 2) sib

theorem Nock.Verb.siblingAxis_half (a : Nat) : siblingAxis (a + 2) / 2 = (a + 2) / 2

A sibling shares its parent: siblingAxis (a+2) / 2 = (a+2) / 2.

theorem Nock.Verb.siblingAxis_parity (a : Nat) : (siblingAxis (a + 2) % 2 == 0) = !(a + 2) % 2 == 0

A sibling has the opposite parity to its axis.

theorem Nock.Verb.slot_edit_eq (ax : Nat) {new old res : Noun} : Noun.edit ax new old = some res → Noun.slot ax res = some new

Read-back (#// round-trip). If editing old at axis ax with new succeeds, reading axis ax of the result res returns new: slot ax res = some new (conditional on edit ax new old = some res). The "terminal replaced node equals the patch" half of the %10 relation.

theorem Nock.Verb.slot_ge_two (m : Nat) (hm : 2 ≤ m) (n : Noun) : Noun.slot m n = match Noun.slot (m / 2) n with | some (l.cell r) => some (if (m % 2 == 0) = true then l else r) | x => none

slot at any axis ≥ 2 in terms of the parent read slot (m/2) and the parity pick — the slot equation stated for a general m rather than the a+2 constructor pattern.

theorem Nock.Verb.slot_edit_sibling {ax sib : Nat} (hsib : SiblingOf ax sib) {new old res : Noun} : Noun.edit ax new old = some res → Noun.slot sib res = Noun.slot sib old

Sibling carry. If editing old at axis ax succeeds, every off-path sibling subtree encountered from ax to the root is unchanged in the result. Thus an edit cannot mutate either the target's immediate sibling or a sibling branching from any proper ancestor of the target.