Verbs and local transitions

Def:verb–selection (main.tex:1034–1112); D/OP (1055–1076); Def:NockProgram (1090–1098); operators (1514–1626); Nock (1639–1661).

inductive Nock.Action : Type

Def:verb (main.tex:1034–1040). Alphabet X := ⟨?,=,/,#,−⟩; actions from X ∪ {*,⊥}.

• null : Action
• star : Action
• wut : Action
• equal : Action
• slot : Action
• edit : Action
• minus : Action

@[instance_reducible]

instance Nock.instReprAction : Repr Action

Equations

• Nock.instReprAction = { reprPrec := Nock.instReprAction.repr }

def Nock.instReprAction.repr : Action → Nat → Std.Format

Equations

• Nock.instReprAction.repr Nock.Action.null prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Nock.Action.null")).group prec✝
• Nock.instReprAction.repr Nock.Action.star prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Nock.Action.star")).group prec✝
• Nock.instReprAction.repr Nock.Action.wut prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Nock.Action.wut")).group prec✝
• Nock.instReprAction.repr Nock.Action.equal prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Nock.Action.equal")).group prec✝
• Nock.instReprAction.repr Nock.Action.slot prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Nock.Action.slot")).group prec✝
• Nock.instReprAction.repr Nock.Action.edit prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Nock.Action.edit")).group prec✝
• Nock.instReprAction.repr Nock.Action.minus prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Nock.Action.minus")).group prec✝

@[instance_reducible]

instance Nock.instDecidableEqAction : DecidableEq Action

Equations

• Nock.instDecidableEqAction x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Nock.instInhabitedAction : Inhabited Action

Equations

• Nock.instInhabitedAction = { default := Nock.instInhabitedAction.default }

def Nock.Action.isNull : Action → Bool

Is an action the null element ⊥?

Equations

• Nock.Action.null.isNull = true
• x✝.isNull = false

def Nock.Action.isOperator : Action → Bool

Is an action one of the operators in X (as opposed to ⊥ or *)?

Equations

• Nock.Action.null.isOperator = false
• Nock.Action.star.isOperator = false
• x✝.isOperator = true

inductive Nock.Verb : Type

Def:verb (main.tex:1034–1040). verb := (actions, noun) ∈ (X ∪ {*,⊥})^{λ−1} × N^λ(F); terminal iff actions all ⊥.

• leaf : Nat → Verb
• node : Action → Verb → Verb → Verb

def Nock.instReprVerb.repr : Verb → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance Nock.instReprVerb : Repr Verb

Equations

• Nock.instReprVerb = { reprPrec := Nock.instReprVerb.repr }

def Nock.instDecidableEqVerb.decEq (x✝ x✝¹ : Verb) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• Nock.instDecidableEqVerb.decEq (Nock.Verb.leaf a) (Nock.Verb.leaf b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Nock.instDecidableEqVerb.decEq (Nock.Verb.leaf a) (Nock.Verb.node a_1 a_2 a_3) = isFalse ⋯
• Nock.instDecidableEqVerb.decEq (Nock.Verb.node a a_1 a_2) (Nock.Verb.leaf a_3) = isFalse ⋯

@[instance_reducible]

instance Nock.instDecidableEqVerb : DecidableEq Verb

Equations

• Nock.instDecidableEqVerb = Nock.instDecidableEqVerb.decEq

@[instance_reducible]

instance Nock.instInhabitedVerb : Inhabited Verb

Equations

• Nock.instInhabitedVerb = { default := Nock.instInhabitedVerb.default }

def Nock.Verb.noun : Verb → Noun

The underlying noun (snd of the verb pair): forget the action labels.

Equations

• (Nock.Verb.leaf n).noun = Nock.Noun.atom n
• (Nock.Verb.node a l r).noun = l.noun.cell r.noun

def Nock.Verb.leaves : Verb → Nat

Number of leaves λ of the verb's noun.

Equations

• (Nock.Verb.leaf n).leaves = 1
• (Nock.Verb.node a l r).leaves = l.leaves + r.leaves

def Nock.Verb.isCell : Verb → Bool

type (main.tex:1045): is the underlying noun a cell?

Equations

• (Nock.Verb.node a a_1 a_2).isCell = true
• (Nock.Verb.leaf a).isCell = false

def Nock.Verb.rootAction : Verb → Option Action

Root action, if the verb is a cell (none at a leaf — leaves carry no action).

Equations

• (Nock.Verb.node a a_1 a_2).rootAction = some a
• (Nock.Verb.leaf a).rootAction = none

def Nock.Verb.isStar : Verb → Bool

Is the root action a pending *?

Equations

• (Nock.Verb.node Nock.Action.star a a_1).isStar = true
• x✝.isStar = false

def Nock.Verb.isPending : Verb → Bool

Does the root node carry a pending (non-⊥) action? * or any operator counts; a leaf or a ⊥-node does not.

Equations

• (Nock.Verb.node a a_1 a_2).isPending = !a.isNull
• (Nock.Verb.leaf a).isPending = false

def Nock.Verb.isTerminal : Verb → Bool

Def:verb (main.tex:1039). verb is (fully) executed or in terminal state if its actions array consists only of ⊥.

Equations

• (Nock.Verb.leaf n).isTerminal = true
• (Nock.Verb.node a l r).isTerminal = (a.isNull && l.isTerminal && r.isTerminal)

Selection (main.tex:1103–1112)

def Nock.Verb.enum : Verb → Nat → Nat × List (Nat × Verb)

Selection (main.tex:1103–1112). map := DFS; index of each internal node is the order a DFS from the root first explores it, excluding leaves.

Equations

• (Nock.Verb.leaf a).enum x✝ = (x✝, [])
• (Nock.Verb.node a l r).enum x✝ = ((r.enum (l.enum (x✝ + 1)).fst).fst, (x✝, Nock.Verb.node a l r) :: ((l.enum (x✝ + 1)).snd ++ (r.enum (l.enum (x✝ + 1)).fst).snd))

def Nock.Verb.nodes (v : Verb) : List (Nat × Verb)

All (index, subverb) pairs of internal nodes, in DFS pre-order.

Equations

• v.nodes = (v.enum 0).snd

def Nock.Verb.findAt : Nat → List (Nat × Verb) → Option Verb

Find the verb at an index in a list of enumerated internal nodes.

Equations

• Nock.Verb.findAt x✝ [] = none
• Nock.Verb.findAt x✝ ((j, v) :: t) = if x✝ = j then some v else Nock.Verb.findAt x✝ t

def Nock.Verb.map (i : Nat) (v : Verb) : Option Verb

Selection (main.tex:1103–1112). map := DFS: returns the verb at internal-node index i ∈ [λ−1].

Equations

• Nock.Verb.map i v = Nock.Verb.findAt i v.nodes

def Nock.Verb.maximumPendingIndex : List (Nat × Verb) → Option Nat

Greatest index of a pending verb in an enumerated list of internal nodes.

Equations

• One or more equations did not get rendered due to their size.
• Nock.Verb.maximumPendingIndex [] = none

def Nock.Verb.getIndex (v : Verb) : Option Nat

Selection (main.tex:1103–1112). getIndex^Λ(F) = argmax_{map(i,F) ∈ NockProgram^Λ}(map(i,F)); F₁ >_F F₂ ⇔ i₁ > i₂.

Equations

• v.getIndex = Nock.Verb.maximumPendingIndex v.nodes

def Nock.Verb.replaceAux (i : Nat) (new : Verb) : Verb → Nat → Nat × Verb

Rebuild v, replacing the internal node at DFS index i by new.

Equations

• One or more equations did not get rendered due to their size.
• Nock.Verb.replaceAux i new (Nock.Verb.leaf a) x✝ = (x✝, Nock.Verb.leaf a)

def Nock.Verb.replaceAt (i : Nat) (v new : Verb) : Verb

Splice: replace the subverb at DFS index i with new.

Equations

• Nock.Verb.replaceAt i v new = (Nock.Verb.replaceAux i new v 0).snd

Computable opcode domain D (main.tex:1055–1083)

def Nock.Verb.opHeadOk : Verb → Bool

type(i) = atom ∧ i ∈ [11], or type(i) = cell (⇒ the cons opcode).

Equations

• (Nock.Verb.leaf n).opHeadOk = decide (n < 11)
• (Nock.Verb.node a l r).opHeadOk = true

def Nock.Verb.inOpcodeDomain : Verb → Bool

Algorithm:Opcode_Updates_verb domain D (main.tex:1055–1058, 1078–1083). D := {v := (a,n) | n := [n₁,[i,n₂]], (i∈[11]) ∪ (type(i)=cell), a₁=⟨*⟩, ∀j≠1 aⱼ=⟨⊥⟩}; (1) v := *[n₁,[i,n₂]]; (2) n₁,[i,n₂] terminal; (3) i atom in [11] or cell.

Equations

• (Nock.Verb.node Nock.Action.star n1 (Nock.Verb.node ra i n2)).inOpcodeDomain = (n1.isTerminal && ra.isNull && i.isTerminal && n2.isTerminal && i.opHeadOk)
• x✝.inOpcodeDomain = false

def Nock.Verb.opReady : Verb → Bool

A node ready for an operator-application step: it carries an operator from X and both of its argument subtrees are already in terminal state (note 2b). These are the operator redexes that the paper's App A transition algorithm elides.

Equations

• (Nock.Verb.node a a_1 a_2).opReady = (a.isOperator && a_1.isTerminal && a_2.isTerminal)
• (Nock.Verb.leaf a).opReady = false

def Nock.Verb.inDomain (v : Verb) : Bool

The full domain of the transition function next: opcode redexes (inOpcodeDomain, = the paper's D) together with ready operator nodes (opReady). See note 2c; Trace.domain (Lem:domain) concludes membership here.

Equations

• v.inDomain = (v.inOpcodeDomain || v.opReady)

Opcode local rewrite (main.tex:1060–1076)

def Nock.Verb.redex : Verb → Option Verb

Algorithm:Opcode_Updates_verb (main.tex:1060–1076). OP₀: *[n₁,[0,n₂]] → /(n₂,n₁); OP₁ → n₂; OP₂ → *[*[n₁,h],*[n₁,t]]; OP₃ → -[3,*[n₁,n₂]]; OP₄ → -[4,*[n₁,n₂]]; OP₅ → =(*[n₁,h],*[n₁,t]); OP₆ → *[n₁,*[t,[0,*[[2,3],[0,*[n₁,[4,[4,h]]]]]]]]; OP₇ → *[*[n₁,h],t]; OP₈ → *[[*[n₁,h],n₁],t]; OP₉ → *[*[n₁,t],2,[[0,1],0,h]]; OP₁₀ → #[hh,*[n₁,th],*[n₁,t]]; cons: *[n₁,[i,n₂]] → [*[n₁,i],*[n₁,n₂]].

Equations

• One or more equations did not get rendered due to their size.
• (Nock.Verb.node Nock.Action.star n1 (Nock.Verb.node ra (Nock.Verb.leaf 0) n2)).redex = some (Nock.Verb.node Nock.Action.slot n2 n1)
• (Nock.Verb.node Nock.Action.star n1 (Nock.Verb.node ra (Nock.Verb.leaf 1) n2)).redex = some n2
• (Nock.Verb.node Nock.Action.star n1 (Nock.Verb.node ra (Nock.Verb.leaf 2) n2)).redex = none
• (Nock.Verb.node Nock.Action.star n1 (Nock.Verb.node ra (Nock.Verb.leaf 3) n2)).redex = some (Nock.Verb.node Nock.Action.minus (Nock.Verb.leaf 3) (Nock.Verb.node Nock.Action.star n1 n2))
• (Nock.Verb.node Nock.Action.star n1 (Nock.Verb.node ra (Nock.Verb.leaf 4) n2)).redex = some (Nock.Verb.node Nock.Action.minus (Nock.Verb.leaf 4) (Nock.Verb.node Nock.Action.star n1 n2))
• (Nock.Verb.node Nock.Action.star n1 (Nock.Verb.node ra (Nock.Verb.leaf 5) n2)).redex = none
• (Nock.Verb.node Nock.Action.star n1 (Nock.Verb.node ra (Nock.Verb.leaf 6) n2)).redex = none
• (Nock.Verb.node Nock.Action.star n1 (Nock.Verb.node ra (Nock.Verb.leaf 7) (Nock.Verb.node a b c))).redex = some (Nock.Verb.node Nock.Action.star (Nock.Verb.node Nock.Action.star n1 b) c)
• (Nock.Verb.node Nock.Action.star n1 (Nock.Verb.node ra (Nock.Verb.leaf 7) n2)).redex = none
• (Nock.Verb.node Nock.Action.star n1 (Nock.Verb.node ra (Nock.Verb.leaf 8) n2)).redex = none
• (Nock.Verb.node Nock.Action.star n1 (Nock.Verb.node ra (Nock.Verb.leaf 9) n2)).redex = none
• (Nock.Verb.node Nock.Action.star n1 (Nock.Verb.node ra (Nock.Verb.leaf 10) (Nock.Verb.node a b c))).redex = none
• (Nock.Verb.node Nock.Action.star n1 (Nock.Verb.node ra (Nock.Verb.leaf 10) n2)).redex = none
• (Nock.Verb.node Nock.Action.star n1 (Nock.Verb.node ra (Nock.Verb.leaf a) n2)).redex = none
• x✝.redex = none

Operator-application steps (Algorithm:Noun_Operators / Unroll_Operator)

def Nock.Verb.ofNoun : Noun → Verb

Convert a plain noun into a terminal verb (all actions ⊥).

Equations

• Nock.Verb.ofNoun (Nock.Noun.atom k) = Nock.Verb.leaf k
• Nock.Verb.ofNoun (l.cell r) = Nock.Verb.node Nock.Action.null (Nock.Verb.ofNoun l) (Nock.Verb.ofNoun r)

Local rewrite (main.tex:1060–1076, 1514–1626)

def Nock.Verb.reduce : Verb → Option Verb

Algorithm:Noun_Operators / Unroll_Operator (main.tex:1514–1626). Local rewrite: * via opcodes, or =, /, #, - (-[3,·]=?, -[4,·]=+) on terminal args.

Equations

• One or more equations did not get rendered due to their size.
• (Nock.Verb.node Nock.Action.star n1 t).reduce = (Nock.Verb.node Nock.Action.star n1 t).redex
• (Nock.Verb.node Nock.Action.equal l r).reduce = some (Nock.Verb.ofNoun (l.noun.tis r.noun))
• (Nock.Verb.node Nock.Action.slot l r).reduce = match l.noun with | Nock.Noun.atom ax => Option.map Nock.Verb.ofNoun (Nock.Noun.slot ax r.noun) | x => none
• (Nock.Verb.node Nock.Action.edit l (Nock.Verb.node a nw od)).reduce = Option.map Nock.Verb.ofNoun (Nock.Noun.edit ax nw.noun od.noun)
• (Nock.Verb.node Nock.Action.edit l r✝).reduce = none
• (Nock.Verb.node Nock.Action.wut a a_1).reduce = none
• (Nock.Verb.node Nock.Action.null a a_1).reduce = none
• (Nock.Verb.leaf a).reduce = none

def Nock.Verb.next (v : Verb) : Option Verb

One Nock step. Locate the pending redex of largest DFS index via getIndex/map; if it lies in the transition domain D (opcode redex or ready operator), apply the local rewrite (reduce) and splice the result back; otherwise crash (none). next v = none also when v is terminal (no pending action). Being a Lean function, next is deterministic — the concrete realization of the paper's "* is a deterministic mapping between program states".

Equations

• One or more equations did not get rendered due to their size.

Executable paper interpreter — iterate next to a result (note 2, PLAN §2)

def Nock.Verb.program (subject formula : Noun) : Verb

Def:NockProgram (main.tex:1090–1098). F = *[subject, formula] with subject, formula terminal; NockProgram^Λ := {F | λ ≤ Λ}.

Equations

• Nock.Verb.program subject formula = Nock.Verb.node Nock.Action.star (Nock.Verb.ofNoun subject) (Nock.Verb.ofNoun formula)

def Nock.Verb.result (v : Verb) : Option Noun

Extract the observable output of a stuck verb: its underlying noun if it is in terminal state (a valid completion, main.tex:1123), else none (a crash / invalid completion, main.tex:1124).

Equations

• v.result = if v.isTerminal = true then some v.noun else none

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

Fuel-indexed iteration of next from v to a terminal/⊥ state, returning the result noun (none on crash or fuel exhaustion). Nock is Turing-complete, so fuel is required for totality; none conflates a genuine crash with fuel exhaustion, exactly as evalN does.

Equations

• Nock.Verb.run 0 x✝ = none
• Nock.Verb.run fuel.succ x✝ = match x✝.next with | some v' => Nock.Verb.run fuel v' | none => x✝.result

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

Run a Nock program *[subject, formula] through the paper's small-step interpreter.

Equations

• Nock.Verb.runProgram fuel subject formula = Nock.Verb.run fuel (Nock.Verb.program subject formula)

Strictness of the DFS order (main.tex:1107)

theorem Nock.Verb.enum_ge_start (v : Verb) (c : Nat) : c ≤ (v.enum c).fst

The DFS counter never decreases: (enum v c).1 ≥ c.

theorem Nock.Verb.enum_index_range (v : Verb) (c : Nat) (p : Nat × Verb) : p ∈ (v.enum c).snd → c ≤ p.fst ∧ p.fst < (v.enum c).fst

Every internal-node index produced by enum v c lies in the half-open counter range [c, (enum v c).1). Distinct nodes therefore receive distinct indices: the DFS map enforces a strict ordering on subtrees (main.tex:1107).

DFS indices are distinct (main.tex:1107)

theorem Nock.Verb.findAt_append (i : Nat) (L1 L2 : List (Nat × Verb)) : findAt i (L1 ++ L2) = match findAt i L1 with | some v => some v | none => findAt i L2

findAt over an append: the left list wins if it has a match.

theorem Nock.Verb.findAt_eq_none {i : Nat} {L : List (Nat × Verb)} : (∀ (p : Nat × Verb), p ∈ L → p.fst ≠ i) → findAt i L = none

If no pair in L carries index i, then findAt i L = none.

theorem Nock.Verb.findAt_some_mem {i : Nat} {v : Verb} {L : List (Nat × Verb)} : findAt i L = some v → (i, v) ∈ L

findAt i L = some v witnesses membership (i, v) ∈ L.

theorem Nock.Verb.map_of_mem_nodes {a : Verb} {i : Nat} {v : Verb} (h : (i, v) ∈ a.nodes) : map i a = some v

map retrieves the unique node at an index. If (i, v) is one of the DFS internal-node pairs of a, then map i a = some v. (Uses DFS distinctness, enum_findAt.)

theorem Nock.Verb.mem_nodes_of_map {a : Verb} {i : Nat} {v : Verb} (h : map i a = some v) : (i, v) ∈ a.nodes

Membership of the retrieved node: map i a = some v ⇒ (i, v) ∈ nodes a.

getIndex = numeric argmax of pending indices (spec of maximumPendingIndex)

Strict redex-selection order (main.tex:1105-1109, 1156)

structure Nock.Verb.StrictSelect (lt : Nat → Nat → Prop) : Prop

A strict selection order on internal-node indices: a strict total order (the paper's "strict ordering", main.tex:1107). Irreflexive + transitive ⇒ asymmetric; total (connectedness) is what forbids ties, hence forces a unique maximum.

• irrefl (i : Nat) : ¬lt i i
• trans {i j k : Nat} : lt i j → lt j k → lt i k
• total {i j : Nat} : i ≠ j → lt i j ∨ lt j i

def Nock.Verb.IsPendingIdx (a : Verb) (i : Nat) : Prop

i is a pending internal-node index of a: map i a is a node with a pending (non-⊥) action.

Equations

• a.IsPendingIdx i = ∃ (v : Nock.Verb), Nock.Verb.map i a = some v ∧ v.isPending = true

def Nock.Verb.IsMaxPending (lt : Nat → Nat → Prop) (a : Verb) (i : Nat) : Prop

i is a maximal pending index of a under the order lt: a pending index that no other pending index exceeds. This is the paper's argmax characterization of getIndex.

Equations

• Nock.Verb.IsMaxPending lt a i = (a.IsPendingIdx i ∧ ∀ (j : Nat), a.IsPendingIdx j → ¬lt i j)

def Nock.Verb.SelStep (lt : Nat → Nat → Prop) (a b : Verb) : Prop

An abstract redex-selection step: pick a maximal pending index i under lt, and if the selected subverb is in the transition domain, apply the local rewrite and splice it back. With no strictness assumption this relation can be multi-valued (several maximal redexes); SelStep.det shows a strict order collapses it to a function.

Equations

• One or more equations did not get rendered due to their size.

theorem Nock.Verb.SelStep.det {lt : Nat → Nat → Prop} (hs : StrictSelect lt) {a b b' : Verb} (h : SelStep lt a b) (h' : SelStep lt a b') : b = b'

Determinism from strictness. If lt is a strict total order, a redex-selection step is deterministic: hs.total forces the two selected indices to coincide; the rest is functionality of map/reduce/replaceAt.

DFS instantiation: the concrete order is strict, and next realizes SelStep

@[reducible, inline]

abbrev Nock.Verb.dfsLt : Nat → Nat → Prop

The concrete DFS order on pre-order indices is the usual strict order on Nat.

Equations

• Nock.Verb.dfsLt x1✝ x2✝ = (x1✝ < x2✝)

theorem Nock.Verb.strictSelect_dfs : StrictSelect dfsLt

The DFS index order is a strict total order. This is why map = DFS "enforces a strict ordering on subtrees" (main.tex:1107): distinct internal nodes get distinct Nat indices (enum_index_range/map_of_mem_nodes), and Nat.lt is a strict total order.

theorem Nock.Verb.isPendingIdx_iff_mem {a : Verb} {i : Nat} : a.IsPendingIdx i ↔ ∃ (v : Verb), (i, v) ∈ a.nodes ∧ v.isPending = true

Pending-index membership, in list form. The ← direction uses DFS distinctness (map_of_mem_nodes): a pending node in the nodes list is retrieved by map on its (unique) index.

theorem Nock.Verb.getIndex_eq_some_iff {a : Verb} {i : Nat} : a.getIndex = some i ↔ IsMaxPending dfsLt a i

getIndex is exactly the DFS argmax: getIndex a = some i ↔ i is the maximal pending index under dfsLt. (Combines the maximumPendingIndex spec with DFS distinctness.)

theorem Nock.Verb.next_eq_some_iff {a b : Verb} : a.next = some b ↔ SelStep dfsLt a b

next faithfully realizes the strict DFS selection step. This is the bridge that makes deterministic_Trace an instance of the paper's conditional theorem: the concrete interpreter's step is SelStep for the (strict) DFS order.

Non-strict selection witness (main.tex:2325)

def Nock.Verb.emptyLt : Nat → Nat → Prop

The empty order — not total, hence not a StrictSelect. Every index is vacuously maximal under it.

Equations

• Nock.Verb.emptyLt x✝¹ x✝ = False

def Nock.Verb.twoRedex : Verb

A verb with two independent, equally-maximal redexes: two copies of *[0, [1, 5]] (each an OP₁ redex reducing to 5), spliced under a ⊥ root.

Equations

• One or more equations did not get rendered due to their size.

theorem Nock.Verb.selStep_multivalued_without_strictness : ∃ (a : Verb), ∃ (b : Verb), ∃ (b' : Verb), b ≠ b' ∧ SelStep emptyLt a b ∧ SelStep emptyLt a b'

Non-vacuity of strictness. Under a non-strict order, SelStep is not a function: it relates twoRedex to two distinct successors. Contrast SelStep.det, which uses StrictSelect.total to collapse exactly this ambiguity.

Terminal verbs cannot step (main.tex:1039, 1122)

theorem Nock.Verb.enum_nonpending_of_terminal (v : Verb) : v.isTerminal = true → ∀ (c : Nat) (p : Nat × Verb), p ∈ (v.enum c).snd → p.snd.isPending = false

Every internal node produced by enum of a terminal verb is non-pending.

theorem Nock.Verb.getIndex_none_of_terminal {v : Verb} (h : v.isTerminal = true) : v.getIndex = none

getIndex of a terminal verb is none: no internal node carries a pending action.

theorem Nock.Verb.next_none_of_terminal {v : Verb} (h : v.isTerminal = true) : v.next = none

A terminal verb cannot take a Nock step.

Converses: no pending redex ⇒ terminal (main.tex:1122)

theorem Nock.Verb.terminal_of_enum_nonpending (v : Verb) (c : Nat) : (∀ (p : Nat × Verb), p ∈ (v.enum c).snd → p.snd.isPending = false) → v.isTerminal = true

Converse of enum_nonpending_of_terminal. If every internal node enumerated from v is non-pending, then v is terminal.

theorem Nock.Verb.getIndex_none_iff_terminal {v : Verb} : v.getIndex = none ↔ v.isTerminal = true

getIndex is none iff terminal. The ← is getIndex_none_of_terminal; the → is terminal_of_enum_nonpending fed the maximumPendingIndex emptiness spec.

theorem Nock.Verb.enum_subtree_mem (v : Verb) (c i : Nat) (sub : Verb) : (i, sub) ∈ (v.enum c).snd → ∀ (p : Nat × Verb), p ∈ (sub.enum i).snd → p ∈ (v.enum c).snd

Subtree enumeration embeds. If sub is enumerated at index i within v (counter c), then every internal node of sub's own enumeration (counter i) also appears in v's enumeration. This is what lets a pending node inside the selected redex be seen as a pending index of the whole verb.

theorem Nock.Verb.children_terminal_of_getIndex {v : Verb} {i : Nat} {a : Action} {l r : Verb} (hidx : v.getIndex = some i) (hmap : map i v = some (node a l r)) : l.isTerminal = true ∧ r.isTerminal = true

The selected redex has terminal children. If getIndex v = some i picks the argmax pending node map i v = node a l r, then l and r are terminal: any pending node below them would have a strictly larger DFS index (enum_index_range + enum_subtree_mem), contradicting maximality (getIndex_eq_some_iff). This is the shape inDomain/reduce need at the redex.

NockVMROM without OP₁₀ (main.tex:1160)

def Nock.Verb.reduceROM : Verb → Option Verb

The ROM local rewrite: identical to reduce except every part of OP₁₀ (edit, # — main.tex:1071,1587) is rejected (none = crash), removing the ability to write to memory. Two things are excluded, exactly the two halves of OP₁₀ in our two-step encoding (note 2b): (i) the OP₁₀ opcode redex *[n₁,[10,n₂]] (i = 10), and (ii) the edit operator node it produces (#, the actual memory write). No other opcode produces edit, so this removes OP₁₀ and nothing else.

Equations

• (Nock.Verb.node Nock.Action.star a (Nock.Verb.node a_1 (Nock.Verb.leaf 10) a_2)).reduceROM = none
• (Nock.Verb.node Nock.Action.edit a a_1).reduceROM = none
• x✝.reduceROM = x✝.reduce

def Nock.Verb.nextROM (v : Verb) : Option Verb

One NockVMROM step: exactly next, but using reduceROM for the local rewrite, so a selected OP₁₀ redex (or a stray edit node) crashes. Every non-crashing ROM step is a genuine Nock step (next_of_nextROM).

Equations

• One or more equations did not get rendered due to their size.

theorem Nock.Verb.nextROM_none_of_terminal {v : Verb} (h : v.isTerminal = true) : v.nextROM = none

A terminal verb cannot take a ROM step either.

theorem Nock.Verb.reduce_of_reduceROM {v r : Verb} (h : v.reduceROM = some r) : v.reduce = some r

reduceROM refines reduce: whenever the ROM rewrite succeeds, the full Nock rewrite agrees (they differ only on OP₁₀, where reduceROM returns none).

theorem Nock.Verb.next_of_nextROM {v w : Verb} (h : v.nextROM = some w) : v.next = some w

Every ROM transition is a Nock transition. nextROM is a restriction of next (OP₁₀ removed): if nextROM v = some w then next v = some w. This is the verb-level sense in which NockVMROM is NockVM without OP₁₀.

Two-verb transition checker Nock (main.tex:1639–1661)

def Nock.Verb.NockCheck (Ti : Verb) (Tnext : Option Verb) : Bool

Algorithm:Transition_Function (main.tex:1639–1661). Nock(Tᵢ,Tᵢ₊₁): Fᵢ ← map(Tᵢ,getIndex(Tᵢ)); frame Tᵢ\Fᵢ = Tᵢ₊₁\Fᵢ₊₁; accept (0) iff Fᵢ₊₁ = OP:Fᵢ / cons:Fᵢ, or Fᵢ₊₁=⊥ when out of domain.

Equations

• One or more equations did not get rendered due to their size.

def Nock.Verb.Crashes (Ti : Verb) : Prop

Ti crashes. Ti selects a pending redex (getIndex Ti ≠ none, so Ti is not terminal, main.tex:1039) but that redex is out of the transition domain / does not reduce, so its only consistent successor is ⊥ (main.tex:1644,1650). Equivalently next Ti = none together with a pending redex.

Equations

• Ti.Crashes = (Ti.getIndex ≠ none ∧ Ti.next = none)

theorem Nock.Verb.map_some_of_getIndex {a : Verb} {i : Nat} (h : a.getIndex = some i) : ∃ (sub : Verb), map i a = some sub

getIndex a = some i names an actual internal node: map i a succeeds. (The argmax is achieved at a pending node, which map retrieves by DFS distinctness.)

theorem Nock.Verb.nockCheck_eq_true_iff {a : Verb} {b : Option Verb} : a.NockCheck b = true ↔ (∃ (v : Verb), b = some v ∧ a.next = some v) ∨ b = none ∧ a.Crashes

NockCheck ↔ forward semantics + crash. The two-verb checker accepts (a, b) (returns true = the paper's 0) iff b is a genuine one-step successor of a (next a = some v, i.e. Step a v) OR a crashes and b = ⊥ (b = none). This is a genuine biconditional: NockCheck is 1-1 with next (on non-⊥ successors) together with the crash branch — the checker Nock(Tᵢ,Tᵢ₊₁)=0 and the forward map coincide exactly.

Frame-invariance gate (main.tex:1642)

def Nock.Verb.FrameAgree (i : Nat) (Ti Tj : Verb) : Prop

Frame agreement at index i: Tj is Ti with the subverb at DFS index i replaced by some Fj — so Ti and Tj share the same frame (context) outside i. This is the map-complement equality Ti \ Fᵢ = Tj \ Fⱼ (main.tex:1642).

Equations

• Nock.Verb.FrameAgree i Ti Tj = ∃ (Fj : Nock.Verb), Tj = Nock.Verb.replaceAt i Ti Fj

theorem Nock.Verb.nockCheck_frameAgree {a b : Verb} (h : a.NockCheck (some b) = true) : ∃ (i : Nat), a.getIndex = some i ∧ FrameAgree i a b

Accepted steps pass the frame gate (main.tex:1642). If NockCheck accepts a non-⊥ successor b of a, then b agrees with a outside the selected index: FrameAgree. (The genuine-step branch of NockCheck is exactly the frame-preserving splice.)

Verifiable crash — a three-way outcome (value / crash / timeout)

run/runProgram return Option Noun, collapsing a genuine crash (a stuck, non-terminal ⊥ state, main.tex:1124) and fuel exhaustion into the same none. eval refines that: it mirrors run's fuel structure exactly, but at a halt (next v = none) it reports value (a terminal completion) or crash (a checked ⊥) instead of some/none; only a genuinely-steppable state can timeout. A crash thus becomes a positive, kernel-checkable outcome, not merely the absence of a value.

inductive Nock.Verb.Outcome : Type

Result of running a verb to a normal form.

• value (n : Noun) : Outcome
• crash : Outcome
• timeout : Outcome

def Nock.Verb.instReprOutcome.repr : Outcome → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Nock.Verb.instReprOutcome.repr Nock.Verb.Outcome.crash prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Nock.Verb.Outcome.crash")).group prec✝
• Nock.Verb.instReprOutcome.repr Nock.Verb.Outcome.timeout prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Nock.Verb.Outcome.timeout")).group prec✝

@[instance_reducible]

instance Nock.Verb.instReprOutcome : Repr Outcome

Equations

• Nock.Verb.instReprOutcome = { reprPrec := Nock.Verb.instReprOutcome.repr }

def Nock.Verb.instDecidableEqOutcome.decEq (x✝ x✝¹ : Outcome) : Decidable (x✝ = x✝¹)

Equations

• Nock.Verb.instDecidableEqOutcome.decEq (Nock.Verb.Outcome.value a) (Nock.Verb.Outcome.value b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Nock.Verb.instDecidableEqOutcome.decEq (Nock.Verb.Outcome.value n) Nock.Verb.Outcome.crash = isFalse ⋯
• Nock.Verb.instDecidableEqOutcome.decEq (Nock.Verb.Outcome.value n) Nock.Verb.Outcome.timeout = isFalse ⋯
• Nock.Verb.instDecidableEqOutcome.decEq Nock.Verb.Outcome.crash (Nock.Verb.Outcome.value n) = isFalse ⋯
• Nock.Verb.instDecidableEqOutcome.decEq Nock.Verb.Outcome.crash Nock.Verb.Outcome.crash = isTrue ⋯
• Nock.Verb.instDecidableEqOutcome.decEq Nock.Verb.Outcome.crash Nock.Verb.Outcome.timeout = isFalse Nock.Verb.instDecidableEqOutcome.decEq._proof_7
• Nock.Verb.instDecidableEqOutcome.decEq Nock.Verb.Outcome.timeout (Nock.Verb.Outcome.value n) = isFalse ⋯
• Nock.Verb.instDecidableEqOutcome.decEq Nock.Verb.Outcome.timeout Nock.Verb.Outcome.crash = isFalse Nock.Verb.instDecidableEqOutcome.decEq._proof_9
• Nock.Verb.instDecidableEqOutcome.decEq Nock.Verb.Outcome.timeout Nock.Verb.Outcome.timeout = isTrue ⋯

@[instance_reducible]

instance Nock.Verb.instDecidableEqOutcome : DecidableEq Outcome

Equations

• Nock.Verb.instDecidableEqOutcome = Nock.Verb.instDecidableEqOutcome.decEq

@[instance_reducible]

instance Nock.Verb.instInhabitedOutcome : Inhabited Outcome

Equations

• Nock.Verb.instInhabitedOutcome = { default := Nock.Verb.instInhabitedOutcome.default }

def Nock.Verb.haltOutcome (v : Verb) : Outcome

The halting outcome of a stopped verb (next v = none): its noun if terminal (a valid completion), else a crash (an invalid completion, main.tex:1124).

Equations

• v.haltOutcome = if v.isTerminal = true then Nock.Verb.Outcome.value v.noun else Nock.Verb.Outcome.crash

theorem Nock.Verb.haltOutcome_crash {v : Verb} (h : v.isTerminal = false) : v.haltOutcome = Outcome.crash

A non-terminal halt is a crash.

def Nock.Verb.eval : Nat → Verb → Outcome

Fuel-indexed evaluation distinguishing a crash from fuel exhaustion. Structurally identical to run, so eval and run agree on values at the same fuel (eval_value_iff_run); the crash branch turns run's conflated none into a positive crash.

Equations

• Nock.Verb.eval 0 x✝ = Nock.Verb.Outcome.timeout
• Nock.Verb.eval fuel.succ x✝ = match x✝.next with | some v' => Nock.Verb.eval fuel v' | none => x✝.haltOutcome

def Nock.Verb.evalProgram (fuel : Nat) (subject formula : Noun) : Outcome

Run a Nock program *[subject, formula], reporting value / crash / timeout.

Equations

• Nock.Verb.evalProgram fuel subject formula = Nock.Verb.eval fuel (Nock.Verb.program subject formula)

theorem Nock.Verb.eval_succ (n : Nat) (v : Verb) : eval (n + 1) v = match v.next with | some v' => eval n v' | none => v.haltOutcome

One-step unfolding of eval (definitional), to avoid over-unfolding nested eval calls.

theorem Nock.Verb.eval_value_iff_run {n : Nat} {v : Verb} {r : Noun} : eval n v = Outcome.value r ↔ run n v = some r

Values are preserved exactly. eval yields value r at fuel n iff the Option-valued run yields some r at the same fuel — successful evaluation is unchanged.

theorem Nock.Verb.eval_crash_mono {n : Nat} {v : Verb} (h : eval n v = Outcome.crash) : eval (n + 1) v = Outcome.crash

Crash is stable one step on: if eval reports crash at fuel n, it reports crash at n + 1. (The general "any larger fuel" form is eval_crash_mono_le.)

theorem Nock.Verb.eval_crash_mono_le {n m : Nat} {v : Verb} (hnm : n ≤ m) (h : eval n v = Outcome.crash) : eval m v = Outcome.crash

Crash is permanent (so a single successful eval certifies it at every fuel): once eval reports crash at fuel n, it reports crash at every m ≥ n.