Sparse-store control instructions #
This proof layer realizes conditional-zero jump, unconditional jump, and halt over the reusable sparse-lookup ABI and a disjoint canonical binary program- counter tape.
theorem
Complexity.RAM.RegisterStore.Machine.setProgramCounterTM_hoareTime_frame_internal
{n : ℕ}
(pc : Fin n)
(pcValue target : ℕ)
(inp₀ : Tape)
(work₀ : Fin n → Tape)
(out₀ : Tape)
(hpc : (work₀ pc).HasBinaryNat pcValue)
(hinput : TM.Parked inp₀)
(hwork : ∀ (i : Fin n), TM.Parked (work₀ i))
(houtput : TM.Parked out₀)
:
(setProgramCounterTM pc target).HoareTime
(fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => inp = inp₀ ∧ work = work₀ ∧ out = out₀)
(fun (inp : Tape) (work : Fin n → Tape) (out : Tape) =>
inp = inp₀ ∧ work = Function.update work₀ pc ((Tape.init (List.map Γ.ofBool target.bits)).move Dir3.right) ∧ out = out₀)
(setProgramCounterTime pcValue target)
Reset a canonical PC and load a fixed target, preserving the literal external frame.
theorem
Complexity.RAM.RegisterStore.Machine.jumpInstructionTM_hoareTime_frame_internal
{n : ℕ}
(tapes : ControlInstructionTapes n)
(store : Store)
(pcValue target : ℕ)
(initialWork : Fin n → Tape)
(inp₀ out₀ : Tape)
(hready : ControlInstructionReady tapes store pcValue initialWork)
(hinput : TM.Parked inp₀)
(houtput : TM.Parked out₀)
:
(jumpInstructionTM tapes target).HoareTime
(fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => inp = inp₀ ∧ work = initialWork ∧ out = out₀)
(fun (inp : Tape) (work : Fin n → Tape) (out : Tape) =>
inp = inp₀ ∧ ControlInstructionResult tapes store target initialWork work ∧ out = out₀)
(jumpInstructionTime pcValue target)
Unconditional jump replaces the PC and preserves the clean sparse-lookup boundary.
theorem
Complexity.RAM.RegisterStore.Machine.zeroJumpInstructionTM_hoareTime_frame_internal
{n : ℕ}
(tapes : ControlInstructionTapes n)
(store : Store)
(pcValue source target : ℕ)
(initialWork : Fin n → Tape)
(inp₀ out₀ : Tape)
(hready : ControlInstructionReady tapes store pcValue initialWork)
(hinput : TM.Parked inp₀)
(houtput : TM.Parked out₀)
:
(zeroJumpInstructionTM tapes source target).HoareTime
(fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => inp = inp₀ ∧ work = initialWork ∧ out = out₀)
(fun (inp : Tape) (work : Fin n → Tape) (out : Tape) =>
inp = inp₀ ∧ ControlInstructionResult tapes store (if read store source = 0 then target else pcValue + 1) initialWork work ∧ out = out₀)
(zeroJumpInstructionTime tapes store pcValue source target)
Conditional-zero lookup and PC update realize the sparse interpreter's
jz semantics and restore the lookup operand to zero.
theorem
Complexity.RAM.RegisterStore.Machine.haltInstructionTM_hoareTime_frame_internal
{n : ℕ}
(tapes : ControlInstructionTapes n)
(store : Store)
(pcValue : ℕ)
(initialWork : Fin n → Tape)
(inp₀ out₀ : Tape)
(hready : ControlInstructionReady tapes store pcValue initialWork)
(hinput : TM.Parked inp₀)
(houtput : TM.Parked out₀)
:
Halt is an exact one-step no-op at the clean control boundary.