Reading a framed bit block

DefinitionMachine step reading one framed payload pair#✓fully proved

Consume one framed-payload pair or its terminator.

def read (a b : K) (d : Γ a → Option Bool) (g : Bool → Γ b)
    (self good bad : Λ) : TM2.Stmt Γ Λ Bool :=
  .peek a (fun _ o => isBit d o) <| .branch id
    (.pop a (fun _ o => bitOf d o) <| .branch id
      (.peek a (fun _ o => isBit d o) <| .branch id
        (.pop a (fun _ o => bitOf d o) <| .push b g <|
          .goto fun _ => self)
        (.goto fun _ => bad))
      (.goto fun _ => good))
    (.goto fun _ => bad)

Uses 2 · Used by 11

Statement usesBit on top of a stack · Bit test for the top of a stack

Used byProgram of the list-of-naturals canonicalizer · Program of the pair-list projector · Program of the frame counter for lists of naturals · Program of the raw pair-frame splitter · Reading a complete framed block · Framed block reader fails on truncated framing · Program of the unary-to-binary converter · Converter turns a unary count into a canonical binary frame · Converter turns a unary count into a raw canonical binary payload · Quadratic run of the raw-input SUBSET-SUM to PARTITION machine · Raw-input PARTITION membership machine runs in quadratic time

TheoremReading a complete framed block#✓fully proved

Read a complete block, preserving an arbitrary suffix and all stacks other than the input and reversed-payload destination.

theorem run_delimit {M : Λ → TM2.Stmt Γ Λ Bool}
    {a b : K} {d : Γ a → Option Bool} {g : Bool → Γ b}
    {self good bad : Λ} (hM : M self = read a b d g self good bad)
    (hab : a ≠ b) (ga : Bool → Γ a) (hga : ∀ c, d (ga c) = some c)
    (payload : List Bool) : ∀ (tail : List (Γ a)) (v : Bool)
      (S : ∀ k, List (Γ k)),
      S a = (delimit payload).map ga ++ tail →
      ∃ S', Run M (payload.length + 1) ⟨some self, v, S⟩
        ⟨some good, false, S'⟩ ∧ S' a = tail ∧
        S' b = (payload.map g).reverse ++ S b ∧
        ∀ k, k ≠ a → k ≠ b → S' k = S k

Uses 4 · Used by 6

Statement usesMachine step reading one framed payload pair · Self-delimiting form of a bitstring · Exact-length runs of a TM2 machine

Proof usesA single step executes the statement at the current label

Used byList canonicalizer normalizes one element · Pair-list projector emits one weight and one value frame per item · Pair-list projector fails on malformed input in linear time · One frame adds one unary count bit · Pair-frame splitter extracts both raw fields · Converter turns a unary count into a raw canonical binary payload

TheoremFramed block reader fails on truncated framing#✓fully proved

Truncated framing reaches the failure branch within input length plus one, without assuming that the input is an encoder image. The destination may contain a partial payload on failure; the caller must discard or clear it before using that stack again.

theorem run_none {M : Λ → TM2.Stmt Γ Λ Bool}
    {a b : K} {d : Γ a → Option Bool} {g : Bool → Γ b}
    {self good bad : Λ} (hM : M self = read a b d g self good bad)
    (hab : a ≠ b) (ga : Bool → Γ a) (hga : ∀ c, d (ga c) = some c)
    (input : List Bool) (v : Bool) (S : ∀ k, List (Γ k))
    (hS : S a = input.map ga) (hn : undelimit input = none) :
    ∃ v' S', RunLe M (input.length + 1) ⟨some self, v, S⟩
      ⟨some bad, v', S'⟩

Uses 5 · Used by 4

Statement usesMachine step reading one framed payload pair · Parsing one self-delimiting block · Runs within a step budget

Proof usesExact-length runs of a TM2 machine · A single step executes the statement at the current label

Used byList canonicalizer fails on malformed input · Pair-list projector fails on malformed input in linear time · Frame counter fails on malformed list framing · Pair-frame splitter fails on malformed first-field framing

3 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.