Resource-proof infrastructure for structured RAM programs

This internal module packages the generic proof obligations that arise when a structured program is verified against the concrete logarithmic-cost RAM: finite register envelopes, their induced finsum space bounds, and compositional source executions carrying exact steps with upper bounds on time and space.

structure Complexity.RAM.Structured.Internal.StoreEnvelope (indexBound valueBound : ℕ) (store : Store) : Prop

A register store fits an index/value envelope. Every nonzero register lies below indexBound, and every stored value is at most valueBound.

• index_lt (index : ℕ) : store index ≠ 0 → index < indexBound
• value_le (index : ℕ) : store index ≤ valueBound

theorem Complexity.RAM.Structured.Internal.StoreEnvelope.mono {indexBound valueBound largerIndex largerValue : ℕ} {store : Store} (hstore : StoreEnvelope indexBound valueBound store) (hindex : indexBound ≤ largerIndex) (hvalue : valueBound ≤ largerValue) : StoreEnvelope largerIndex largerValue store

Enlarging either side of a store envelope preserves the bound.

theorem Complexity.RAM.Structured.Internal.Input.bitStoreEnvelope {lengthReg inputBase indexBound valueBound : ℕ} (bits : List Bool) (hlengthReg : lengthReg < indexBound) (hinputEnd : inputBase + bits.length ≤ indexBound) (hlength : bits.length ≤ valueBound) (hone : 1 ≤ valueBound) : StoreEnvelope indexBound valueBound (Input.bitStore lengthReg inputBase bits)

A reserved-prefix bit input fits any envelope containing its length register, input interval, list length, and Boolean values.

def Complexity.RAM.Structured.Internal.envelopeSpace (indexBound valueBound : ℕ) : ℕ

Logarithmic space occupied by the largest store admitted by an envelope.

Equations

• Complexity.RAM.Structured.Internal.envelopeSpace indexBound valueBound = indexBound * (Complexity.RAM.bitlen indexBound + Complexity.RAM.bitlen valueBound)

theorem Complexity.RAM.Structured.Internal.StoreEnvelope.space_le {indexBound valueBound : ℕ} {store : Store} (hstore : StoreEnvelope indexBound valueBound store) : store.space ≤ envelopeSpace indexBound valueBound

A store envelope bounds the real finite-sum source-space measure.

theorem Complexity.RAM.Structured.Internal.StoreEnvelope.update {indexBound valueBound index value : ℕ} {store : Store} (hstore : StoreEnvelope indexBound valueBound store) (hindex : index < indexBound) (hvalue : value ≤ valueBound) : StoreEnvelope indexBound valueBound (Function.update store index value)

Updating an in-envelope register with an in-envelope value preserves the store envelope.

def Complexity.RAM.Structured.Internal.Basic.writeIndex : Basic → Store → ℕ

Register written by a basic instruction in a given store. The store argument is relevant only for indirect writes.

Equations

• Complexity.RAM.Structured.Internal.Basic.writeIndex (Complexity.RAM.Structured.Basic.imm dst value) x✝ = dst
• Complexity.RAM.Structured.Internal.Basic.writeIndex (Complexity.RAM.Structured.Basic.add dst left right) x✝ = dst
• Complexity.RAM.Structured.Internal.Basic.writeIndex (Complexity.RAM.Structured.Basic.sub dst left right) x✝ = dst
• Complexity.RAM.Structured.Internal.Basic.writeIndex (Complexity.RAM.Structured.Basic.mul dst left right) x✝ = dst
• Complexity.RAM.Structured.Internal.Basic.writeIndex (Complexity.RAM.Structured.Basic.load dst address) x✝ = dst
• Complexity.RAM.Structured.Internal.Basic.writeIndex (Complexity.RAM.Structured.Basic.store address src) x✝ = x✝ address

def Complexity.RAM.Structured.Internal.Basic.writeValue : Basic → Store → ℕ

Value written by a basic instruction in a given store.

Equations

• Complexity.RAM.Structured.Internal.Basic.writeValue (Complexity.RAM.Structured.Basic.imm dst value) x✝ = value
• Complexity.RAM.Structured.Internal.Basic.writeValue (Complexity.RAM.Structured.Basic.add dst left right) x✝ = x✝ left + x✝ right
• Complexity.RAM.Structured.Internal.Basic.writeValue (Complexity.RAM.Structured.Basic.sub dst left right) x✝ = x✝ left - x✝ right
• Complexity.RAM.Structured.Internal.Basic.writeValue (Complexity.RAM.Structured.Basic.mul dst left right) x✝ = x✝ left * x✝ right
• Complexity.RAM.Structured.Internal.Basic.writeValue (Complexity.RAM.Structured.Basic.load dst address) x✝ = x✝ (x✝ address)
• Complexity.RAM.Structured.Internal.Basic.writeValue (Complexity.RAM.Structured.Basic.store address src) x✝ = x✝ src

theorem Complexity.RAM.Structured.Internal.Basic.exec_eq_update (op : Basic) (store : Store) : op.exec store = Function.update store (writeIndex op store) (writeValue op store)

Basic execution is a single functional update, uniformly across direct and indirect instructions.

def Complexity.RAM.Structured.Internal.Basic.EnvelopeChain (indexBound valueBound : ℕ) : List Basic → Store → Prop

A concrete straight-line execution stays inside one store envelope at its initial store and after every instruction. Unlike a uniform preservation condition, this certificate can use semantic facts about the actual store at each program point.

Equations

• One or more equations did not get rendered due to their size.
• Complexity.RAM.Structured.Internal.Basic.EnvelopeChain indexBound valueBound [] x✝ = Complexity.RAM.Structured.Internal.StoreEnvelope indexBound valueBound x✝

theorem Complexity.RAM.Structured.Internal.Basic.EnvelopeChain.append {indexBound valueBound : ℕ} {first second : List Basic} {store : Store} (hfirst : EnvelopeChain indexBound valueBound first store) (hsecond : EnvelopeChain indexBound valueBound second (Basic.execList first store)) : EnvelopeChain indexBound valueBound (first ++ second) store

theorem Complexity.RAM.Structured.Internal.Basic.EnvelopeChain.final {indexBound valueBound : ℕ} {ops : List Basic} {store : Store} (hchain : EnvelopeChain indexBound valueBound ops store) : StoreEnvelope indexBound valueBound (Basic.execList ops store)

theorem Complexity.RAM.Structured.Internal.StoreEnvelope.execBasic {indexBound valueBound : ℕ} {store : Store} (hstore : StoreEnvelope indexBound valueBound store) (op : Basic) (hindex : Basic.writeIndex op store < indexBound) (hvalue : Basic.writeValue op store ≤ valueBound) : StoreEnvelope indexBound valueBound (op.exec store)

A basic instruction preserves an envelope when its destination and written value fit that envelope.

theorem Complexity.RAM.Structured.Internal.Basic.execList_imm_apply_of_not_mem (writes : List (ℕ × ℕ)) (store : Store) (index : ℕ) (hnot : index ∉ List.map Prod.fst writes) : Basic.execList (List.map (fun (write : ℕ × ℕ) => Basic.imm write.1 write.2) writes) store index = store index

A straight-line list of immediate writes preserves a register whose index does not occur among the destinations.

theorem Complexity.RAM.Structured.Internal.Basic.execList_imm_apply_of_mem (writes : List (ℕ × ℕ)) (store : Store) (hnodup : (List.map Prod.fst writes).Nodup) {index value : ℕ} (hmem : (index, value) ∈ writes) : Basic.execList (List.map (fun (write : ℕ × ℕ) => Basic.imm write.1 write.2) writes) store index = value

With distinct destinations, a listed immediate write determines the final value at its destination.

def Complexity.RAM.Structured.Internal.valueWidth (valueBound : ℕ) : ℕ

A one-bit cushion over the width of the envelope's largest value.

Equations

• Complexity.RAM.Structured.Internal.valueWidth valueBound = Complexity.RAM.bitlen valueBound + 1

theorem Complexity.RAM.Structured.Internal.bitlen_le_valueWidth {valueBound value : ℕ} (hvalue : value ≤ valueBound) : bitlen value ≤ valueWidth valueBound

theorem Complexity.RAM.Structured.Internal.one_le_valueWidth (valueBound : ℕ) : 1 ≤ valueWidth valueBound

theorem Complexity.RAM.Structured.Internal.Basic.logCost_le_four_valueWidth {indexBound valueBound : ℕ} (op : Basic) (store : Store) (hstore : StoreEnvelope indexBound valueBound store) (hnext : StoreEnvelope indexBound valueBound (op.exec store)) : op.logCost store ≤ 4 * valueWidth valueBound

Any basic instruction whose pre- and post-stores fit the same envelope has logarithmic cost at most four times the envelope value width.

def Complexity.RAM.Structured.Internal.MeasuredRuns (cmd : Cmd) (initial final : Store) (steps costBound spaceLimit : ℕ) : Prop

A source execution with an exact transition count and upper bounds on its logarithmic cost and peak space.

Equations

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

theorem Complexity.RAM.Structured.Internal.exec_basics_exists (ops : List Basic) (initial : Store) : ∃ (cost : ℕ) (space : ℕ), Exec (Cmd.basics ops) initial (Basic.execList ops initial) ops.length cost space

A straight-line basic block always has an exact source execution. This certificate deliberately leaves cost and space existential, allowing semantic proofs to proceed before a client chooses a resource envelope.

theorem Complexity.RAM.Structured.Internal.MeasuredRuns.skipEnvelope {indexBound valueBound : ℕ} {store : Store} (hstore : StoreEnvelope indexBound valueBound store) : MeasuredRuns Cmd.skip store store 0 0 (envelopeSpace indexBound valueBound)

theorem Complexity.RAM.Structured.Internal.MeasuredRuns.basicEnvelope {indexBound valueBound : ℕ} (op : Basic) (store : Store) (hstore : StoreEnvelope indexBound valueBound store) (hnext : StoreEnvelope indexBound valueBound (op.exec store)) : MeasuredRuns (Cmd.basic op) store (op.exec store) 1 (4 * valueWidth valueBound) (envelopeSpace indexBound valueBound)

theorem Complexity.RAM.Structured.Internal.MeasuredRuns.seq {first second : Cmd} {initial middle final : Store} {firstSteps secondSteps firstCost secondCost spaceLimit : ℕ} (hfirst : MeasuredRuns first initial middle firstSteps firstCost spaceLimit) (hsecond : MeasuredRuns second middle final secondSteps secondCost spaceLimit) : MeasuredRuns (first.seq second) initial final (firstSteps + secondSteps) (firstCost + secondCost) spaceLimit

theorem Complexity.RAM.Structured.Internal.MeasuredRuns.basicsEnvelope {indexBound valueBound : ℕ} (ops : List Basic) (initial : Store) (hinitial : StoreEnvelope indexBound valueBound initial) (hpreserve : ∀ op ∈ ops, ∀ (store : Store), StoreEnvelope indexBound valueBound store → StoreEnvelope indexBound valueBound (op.exec store)) : MeasuredRuns (Cmd.basics ops) initial (Basic.execList ops initial) ops.length (4 * ops.length * valueWidth valueBound) (envelopeSpace indexBound valueBound) ∧ StoreEnvelope indexBound valueBound (Basic.execList ops initial)

A straight-line list of basic instructions inherits uniform resource bounds when every listed instruction preserves the chosen store envelope.

theorem Complexity.RAM.Structured.Internal.MeasuredRuns.basicsEnvelopeChain {indexBound valueBound : ℕ} (ops : List Basic) (initial : Store) (hchain : Basic.EnvelopeChain indexBound valueBound ops initial) : MeasuredRuns (Cmd.basics ops) initial (Basic.execList ops initial) ops.length (4 * ops.length * valueWidth valueBound) (envelopeSpace indexBound valueBound) ∧ StoreEnvelope indexBound valueBound (Basic.execList ops initial)

A concrete per-program-point envelope chain yields the same exact-step, uniform-cost certificate as a globally uniform preservation proof.

theorem Complexity.RAM.Structured.Internal.MeasuredRuns.weakenCost {cmd : Cmd} {initial final : Store} {steps costBound largerBound spaceLimit : ℕ} (hrun : MeasuredRuns cmd initial final steps costBound spaceLimit) (hle : costBound ≤ largerBound) : MeasuredRuns cmd initial final steps largerBound spaceLimit

theorem Complexity.RAM.Structured.Internal.MeasuredRuns.weakenSpace {cmd : Cmd} {initial final : Store} {steps costBound spaceLimit largerLimit : ℕ} (hrun : MeasuredRuns cmd initial final steps costBound spaceLimit) (hle : spaceLimit ≤ largerLimit) : MeasuredRuns cmd initial final steps costBound largerLimit

theorem Complexity.RAM.Structured.Internal.MeasuredRuns.weaken {cmd : Cmd} {initial final : Store} {steps costBound largerCost spaceLimit largerSpace : ℕ} (hrun : MeasuredRuns cmd initial final steps costBound spaceLimit) (hcost : costBound ≤ largerCost) (hspace : spaceLimit ≤ largerSpace) : MeasuredRuns cmd initial final steps largerCost largerSpace

theorem Complexity.RAM.Structured.Internal.MeasuredRuns.ifZeroEnvelope {indexBound valueBound test : ℕ} {onZero onNonzero : Cmd} {initial final : Store} {steps costBound : ℕ} (htest : initial test = 0) (hstore : StoreEnvelope indexBound valueBound initial) (hbranch : MeasuredRuns onZero initial final steps costBound (envelopeSpace indexBound valueBound)) : MeasuredRuns (Cmd.ifZero test onZero onNonzero) initial final (steps + 1) (valueWidth valueBound + costBound) (envelopeSpace indexBound valueBound)

theorem Complexity.RAM.Structured.Internal.MeasuredRuns.ifNonzeroEnvelope {indexBound valueBound test : ℕ} {onZero onNonzero : Cmd} {initial final : Store} {steps costBound : ℕ} (htest : initial test ≠ 0) (hstore : StoreEnvelope indexBound valueBound initial) (hbranch : MeasuredRuns onNonzero initial final steps costBound (envelopeSpace indexBound valueBound)) : MeasuredRuns (Cmd.ifZero test onZero onNonzero) initial final (steps + 2) (3 * valueWidth valueBound + costBound) (envelopeSpace indexBound valueBound)

theorem Complexity.RAM.Structured.Internal.MeasuredRuns.whileZeroEnvelope {indexBound valueBound test : ℕ} {body : Cmd} {store : Store} (htest : store test = 0) (hstore : StoreEnvelope indexBound valueBound store) : MeasuredRuns (Cmd.whileNonzero test body) store store 1 (valueWidth valueBound) (envelopeSpace indexBound valueBound)

theorem Complexity.RAM.Structured.Internal.MeasuredRuns.whileNonzeroEnvelope {indexBound valueBound test : ℕ} {body : Cmd} {initial middle final : Store} {bodySteps loopSteps bodyCost loopCost : ℕ} (htest : initial test ≠ 0) (hstore : StoreEnvelope indexBound valueBound initial) (hbody : MeasuredRuns body initial middle bodySteps bodyCost (envelopeSpace indexBound valueBound)) (hloop : MeasuredRuns (Cmd.whileNonzero test body) middle final loopSteps loopCost (envelopeSpace indexBound valueBound)) : MeasuredRuns (Cmd.whileNonzero test body) initial final (bodySteps + loopSteps + 2) (3 * valueWidth valueBound + bodyCost + loopCost) (envelopeSpace indexBound valueBound)

def Complexity.RAM.Structured.Internal.MeasuredRuns.whileFoldSteps {α : Type u_1} (bodySteps : α → ℕ) : List α → ℕ

Exact source transition count obtained by iterating bodies with the given per-element step count. Each nonempty iteration also pays two loop-control transitions, and the final zero test pays one.

Equations

• Complexity.RAM.Structured.Internal.MeasuredRuns.whileFoldSteps bodySteps [] = 1
• Complexity.RAM.Structured.Internal.MeasuredRuns.whileFoldSteps bodySteps (item :: rest) = bodySteps item + Complexity.RAM.Structured.Internal.MeasuredRuns.whileFoldSteps bodySteps rest + 2

def Complexity.RAM.Structured.Internal.MeasuredRuns.whileFoldCost {α : Type u_1} (width : ℕ) (bodyCost : α → ℕ) : List α → ℕ

Compositional cost bound for a list-indexed loop. Each nonempty iteration pays three envelope widths for its nonzero test and back edge; the final zero test pays one envelope width.

Equations

• One or more equations did not get rendered due to their size.
• Complexity.RAM.Structured.Internal.MeasuredRuns.whileFoldCost width bodyCost [] = width

theorem Complexity.RAM.Structured.Internal.MeasuredRuns.whileFoldEnvelope {α : Type u_1} {σ : Type u_2} {indexBound valueBound test : ℕ} {body : Cmd} (Inv : List α → σ → Store → Prop) (advance : σ → α → σ) (bodySteps bodyCost : α → ℕ) (hstore : ∀ (items : List α) (state : σ) (store : Store), Inv items state store → StoreEnvelope indexBound valueBound store) (hnil : ∀ (state : σ) (store : Store), Inv [] state store → store test = 0) (hcons : ∀ (item : α) (rest : List α) (state : σ) (store : Store), Inv (item :: rest) state store → store test ≠ 0) (hbody : ∀ (item : α) (rest : List α) (state : σ) (store : Store), Inv (item :: rest) state store → ∃ (next : Store), MeasuredRuns body store next (bodySteps item) (bodyCost item) (envelopeSpace indexBound valueBound) ∧ Inv rest (advance state item) next) {items : List α} {state : σ} {initial : Store} (hinv : Inv items state initial) : ∃ (final : Store), MeasuredRuns (Cmd.whileNonzero test body) initial final (whileFoldSteps bodySteps items) (whileFoldCost (valueWidth valueBound) bodyCost items) (envelopeSpace indexBound valueBound) ∧ Inv [] (List.foldl advance state items) final

Verify a structured loop by folding an abstract state over a logical input list. The client supplies only its invariant, one body certificate, and the zero/nonzero interpretations of the test register; run stitching and resource accounting are generic.