Counting frames of a concrete List Nat input

InductiveStacks of the frame counter for lists of naturals#✓fully proved

Input, one-block scratch, and a unary element counter.

inductive K | input | scratch | count
  deriving DecidableEq

Used by 9

Used byFrame counter yields the number of raw frames in unary · Frame counter for lists of naturals as a host component · One frame adds one unary count bit · Program of the frame counter for lists of naturals · Frame counter decides decodability and counts length in unary · Embedded frame counter preserves caller stacks · Frame counter fails on malformed list framing · Frame counter counts every successfully decoded list of naturals · Stack contents of the frame counter for lists of naturals

InductiveControl labels of the frame counter for lists of naturals#✓fully proved

Each complete frame increments the counter and clears its scratch.

inductive Lab | loop | block | bump | clear | good | bad
  deriving DecidableEq

Used by 8

Used byFrame counter yields the number of raw frames in unary · Frame counter for lists of naturals as a host component · One frame adds one unary count bit · Program of the frame counter for lists of naturals · Frame counter decides decodability and counts length in unary · Embedded frame counter preserves caller stacks · Frame counter fails on malformed list framing · Frame counter counts every successfully decoded list of naturals

DefinitionProgram of the frame counter for lists of naturals#✓fully proved

Count by repeated shared block reading and shared scratch cleanup.

def prog : Lab → TM2.Stmt (fun _ : K => Bool) Lab Bool
  | .loop => .peek .input (fun _ o => o.isSome) <| .branch id
      (.goto fun _ => .block) (.goto fun _ => .good)
  | .block => Block.read .input .scratch some id .block .bump .bad
  | .bump => .push .count (fun _ => true) (.goto fun _ => .clear)
  | .clear => cleanS [.scratch] .clear .loop
  | .good | .bad => .halt

Uses 5 · Used by 7

Statement usesMachine step reading one framed payload pair · Stacks of the frame counter for lists of naturals · Control labels of the frame counter for lists of naturals · Flag bit of a machine state · Cleanup round

Used byFrame counter yields the number of raw frames in unary · Frame counter for lists of naturals as a host component · One frame adds one unary count bit · Frame counter decides decodability and counts length in unary · Embedded frame counter preserves caller stacks · Frame counter fails on malformed list framing · Frame counter counts every successfully decoded list of naturals

DefinitionStack contents of the frame counter for lists of naturals#✓fully proved

The three actual stack contents.

def st (input scratch count : List Bool) : K → List Bool
  | .input => input
  | .scratch => scratch
  | .count => count

Uses 1 · Used by 6

Statement usesStacks of the frame counter for lists of naturals

Used byFrame counter yields the number of raw frames in unary · One frame adds one unary count bit · Frame counter decides decodability and counts length in unary · Embedded frame counter preserves caller stacks · Frame counter fails on malformed list framing · Frame counter counts every successfully decoded list of naturals

TheoremOne frame adds one unary count bit#✓fully proved

One complete frame contributes exactly one unary count bit and leaves no payload scratch, independently of the decoded Nat's value.

theorem element_run (p x count : List Bool) (v : Bool) :
    RunLe prog (4 * (delimit p).length)
      ⟨some .loop, v, st (delimit p ++ x) [] count⟩
      ⟨some .loop, false, st x [] (true :: count)⟩

Uses 11 · Used by 2

Statement usesStacks of the frame counter for lists of naturals · Control labels of the frame counter for lists of naturals · Program of the frame counter for lists of naturals · Stack contents of the frame counter for lists of naturals · Self-delimiting form of a bitstring · Runs within a step budget

Proof usesReading a complete framed block · Flag bit of a machine state · Exact-length runs of a TM2 machine · A single step executes the statement at the current label · Cleanup empties its stacks

Used byFrame counter yields the number of raw frames in unary · Frame counter fails on malformed list framing

TheoremFrame counter yields the number of raw frames in unary#✓fully proved

Counting a sequence of raw frames yields its length in unary, with the caller's counter suffix preserved and scratch empty.

theorem blocks_run (bs : List (List Bool)) (count : List Bool) (v : Bool) :
    RunLe prog (4 * ((bs.map delimit).flatten).length + 1)
      ⟨some .loop, v, st (bs.map delimit).flatten [] count⟩
      ⟨some .good, false,
        st [] [] (List.replicate bs.length true ++ count)⟩

Uses 9 · Used by 1

Statement usesStacks of the frame counter for lists of naturals · Control labels of the frame counter for lists of naturals · Program of the frame counter for lists of naturals · Stack contents of the frame counter for lists of naturals · Self-delimiting form of a bitstring · Runs within a step budget

Proof usesOne frame adds one unary count bit · Exact-length runs of a TM2 machine · A single step executes the statement at the current label

Used byFrame counter counts every successfully decoded list of naturals

TheoremFrame counter counts every successfully decoded list of naturals#✓fully proved

Count every successfully decoded List Nat, including noncanonical Nat payloads; the count suffix is preserved exactly.

theorem run_some {x : List Bool} {as : List Nat}
    (h : bitDecode x = some as) (count : List Bool) (v : Bool) :
    RunLe prog (4 * x.length + 1)
      ⟨some .loop, v, st x [] count⟩
      ⟨some .good, false,
        st [] [] (List.replicate as.length true ++ count)⟩

Uses 16 · Used by 1

Statement usesStacks of the frame counter for lists of naturals · Control labels of the frame counter for lists of naturals · Program of the frame counter for lists of naturals · Stack contents of the frame counter for lists of naturals · Bitstring encodings · Decoding function of a bitstring encoding · Decoding inverts bitstring encoding · Encoding function of a bitstring encoding · Self-delimiting form of a bitstring · Parsing one self-delimiting block · Parsing a list of booleans into self-delimiting blocks · Bounded parsing of self-delimiting blocks · Runs within a step budget

Proof usesFrame counter yields the number of raw frames in unary · Successful block parsing reconstructs the input · Decoding a list of naturals is block parsing then number decoding

Used byFrame counter decides decodability and counts length in unary

TheoremFrame counter fails on malformed list framing#✓fully proved

Malformed List Nat framing reaches the failure endpoint. The counter and scratch may be partial and must be cleared before reuse.

theorem run_none {x : List Bool} (h : bitDecode (α := List Nat) x = none)
    (count : List Bool) (v : Bool) :
    ∃ v' S, RunLe prog (4 * x.length + 2)
      ⟨some .loop, v, st x [] count⟩ ⟨some .bad, v', S⟩

Uses 19 · Used by 1

Statement usesStacks of the frame counter for lists of naturals · Control labels of the frame counter for lists of naturals · Program of the frame counter for lists of naturals · Stack contents of the frame counter for lists of naturals · Bitstring encodings · Decoding function of a bitstring encoding · Decoding inverts bitstring encoding · Encoding function of a bitstring encoding · Self-delimiting form of a bitstring · Parsing one self-delimiting block · Parsing a list of booleans into self-delimiting blocks · Bounded parsing of self-delimiting blocks · Runs within a step budget

Proof usesFramed block reader fails on truncated framing · One frame adds one unary count bit · Decoding a list of naturals is block parsing then number decoding · Parsing a self-delimiting block · Exact-length runs of a TM2 machine · A single step executes the statement at the current label

Used byFrame counter decides decodability and counts length in unary

AbbreviationFrame counter for lists of naturals as a host component#✓fully proved

The frame counter is a finite component of the existing Host.

abbrev component : Host.Comp where
  K := K
  Γ := fun _ => Bool
  L := Lab
  prog := prog
  ks := [.input, .scratch, .count]
  ks_nodup := by decide
  mem_ks k := by cases k <;> decide

Uses 4

Statement usesComponent machine · Stacks of the frame counter for lists of naturals · Control labels of the frame counter for lists of naturals · Program of the frame counter for lists of naturals

TheoremFrame counter decides decodability and counts length in unary#✓fully proved

Total List Nat decoding outcome and exact unary length on success.

theorem run (x : List Bool) (v : Bool) :
    ∃ v' S, RunLe prog (4 * x.length + 2)
      ⟨some .loop, v, st x [] []⟩
      ⟨some (if (bitDecode (α := List Nat) x).isSome then .good else .bad),
        v', S⟩ ∧
      ∀ as : List Nat, bitDecode x = some as →
        S = st [] [] (List.replicate as.length true)

Uses 16 · Used by 1

Statement usesStacks of the frame counter for lists of naturals · Control labels of the frame counter for lists of naturals · Program of the frame counter for lists of naturals · Stack contents of the frame counter for lists of naturals · Bitstring encodings · Decoding function of a bitstring encoding · Decoding inverts bitstring encoding · Encoding function of a bitstring encoding · Self-delimiting form of a bitstring · Parsing one self-delimiting block · Parsing a list of booleans into self-delimiting blocks · Bounded parsing of self-delimiting blocks · Runs within a step budget

Proof usesFrame counter fails on malformed list framing · Frame counter counts every successfully decoded list of naturals · Exact-length runs of a TM2 machine

Used byEmbedded frame counter preserves caller stacks

TheoremEmbedded frame counter preserves caller stacks#✓fully proved

Embedded counting preserves every caller stack outside its workspace on success and failure. Scratch is empty on success.

theorem run_embedded {J L : Type} [DecidableEq J] {Γ : J → Type}
    (E : MetaMathlibExt.TM2Embedding.SEmb (fun _ : K => Bool) Γ)
    (φ : Lab → L) {M : L → TM2.Stmt Γ L Bool}
    (hm : MetaMathlibExt.TM2Embedding.Embeds E φ prog M)
    (x : List Bool) (v : Bool) (S : ∀ j, List (Γ j))
    (hs : MetaMathlibExt.TM2Embedding.Agree E (st x [] []) S) :
    ∃ v' T, RunLe M (4 * x.length + 2)
      ⟨some (φ .loop), v, S⟩
      ⟨some (φ (if (bitDecode (α := List Nat) x).isSome
        then .good else .bad)), v', T⟩ ∧
      MetaMathlibExt.TM2Embedding.Frame E S T ∧
      ∀ as : List Nat, bitDecode x = some as →
        MetaMathlibExt.TM2Embedding.Agree E
          (st [] [] (List.replicate as.length true)) T

Uses 19

Statement usesStacks of the frame counter for lists of naturals · Control labels of the frame counter for lists of naturals · Program of the frame counter for lists of naturals · Stack contents of the frame counter for lists of naturals · Bitstring encodings · Decoding function of a bitstring encoding · Decoding inverts bitstring encoding · Encoding function of a bitstring encoding · Self-delimiting form of a bitstring · Parsing one self-delimiting block · Parsing a list of booleans into self-delimiting blocks · Bounded parsing of self-delimiting blocks · Agreement of host and sub-machine stacks · Embedding of a machine in a host · Frame condition for a stack embedding · Stack embedding · Runs within a step budget

Proof usesFrame counter decides decodability and counts length in unary · Run embedding for bounded runs

11 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.