Raw projection of the canonical pair frame

InductiveStacks of the raw pair-frame splitter#✓fully proved

The original input becomes the second field; left holds the first.

inductive K | input | left | scratch
  deriving DecidableEq

Used by 35

Used byPair-list projector main loop emits both lists in reverse · Pair-list projector as a host component · Pair-list projector emits one weight and one value frame per item · Program of the pair-list projector · Pair-list projector always terminates at the decoding outcome · Embedded pair-list projector preserves outside stacks · Pair-list projector fails on malformed input in linear time · Pair-list projector yields canonical weight and value lists · Four-output pair-list decoder as a host component · Program of the four-output pair-list decoder · Four-output decoder reaches exactly the canonical decoding outcome · Embedded four-output decoder preserves outside stacks · Four-output decoder fails on malformed input · Four-output decoder emits four canonical outputs on success · Outer-splitter stack embedding in the four-output decoder · Number-pair projector as a host component · Stacks of the number-pair projector · Field-normalizer stack embedding in the number-pair projector · Pair-frame splitter stack embedding in the number-pair projector · Program of the number-pair projector · Number-pair projector reaches the decoding outcome · Number-pair projector normalizes both fields of a raw pair frame · Embedded number-pair projector preserves outside stacks · Number-pair projector fails on malformed framing in linear time · Number-pair projector yields both canonical payloads on success · Six-stack invariant of the number-pair projector · Raw pair-frame splitter as a host component · Program of the raw pair-frame splitter · Pair-frame splitter reaches the framing outcome · Raw field projection agrees with the pair decoder · Pair-frame splitter extracts both raw fields · Embedded pair-frame splitter preserves caller stacks · Pair-frame splitter fails on malformed first-field framing · Pair-frame splitter projects every well-framed input in linear time · Stack layout of the raw pair-frame splitter

InductiveControl labels of the raw pair-frame splitter#✓fully proved

Read one frame, restore its order, then report success or failure.

inductive Lab | read | copy | good | bad
  deriving DecidableEq

Used by 32

Used byPair-list projector as a host component · Pair-list projector emits one weight and one value frame per item · Pair-normalizer halt redirection in the pair-list projector · Program of the pair-list projector · Pair-list projector fails on malformed input in linear time · Four-output pair-list decoder as a host component · Label map from the list projector to the final pair decoder · Control labels of the four-output pair-list decoder · Label map from final pair halts to the decoder outcomes · Program of the four-output pair-list decoder · Four-output decoder reaches exactly the canonical decoding outcome · Embedded four-output decoder preserves outside stacks · Four-output decoder fails on malformed input · Four-output decoder emits four canonical outputs on success · Label map from the outer splitter to the list projector · Number-pair projector as a host component · Control labels of the number-pair projector · Pair-frame splitter halt redirection in the number-pair projector · Program of the number-pair projector · Number-pair projector reaches the decoding outcome · Number-pair projector normalizes both fields of a raw pair frame · Embedded number-pair projector preserves outside stacks · Number-pair projector fails on malformed framing in linear time · Number-pair projector yields both canonical payloads on success · Raw pair-frame splitter as a host component · Program of the raw pair-frame splitter · Pair-frame splitter reaches the framing outcome · Raw field projection agrees with the pair decoder · Pair-frame splitter extracts both raw fields · Embedded pair-frame splitter preserves caller stacks · Pair-frame splitter fails on malformed first-field framing · Pair-frame splitter projects every well-framed input in linear time

DefinitionProgram of the raw pair-frame splitter#✓fully proved

Pair framing is split using the existing delimiter and move kernels.

def prog : Lab → TM2.Stmt (fun _ : K => Bool) Lab Bool
  | .read => Block.read .input .scratch some id .read .copy .bad
  | .copy => moveB .scratch .left some id .copy .good
  | .good | .bad => .halt

Uses 5 · Used by 13

Statement usesMachine step reading one framed payload pair · Stacks of the raw pair-frame splitter · Control labels of the raw pair-frame splitter · Flag bit of a machine state · Bit-moving loop

Used byProgram of the four-output pair-list decoder · Four-output decoder fails on malformed input · Four-output decoder emits four canonical outputs on success · Program of the number-pair projector · Number-pair projector normalizes both fields of a raw pair frame · Number-pair projector fails on malformed framing in linear time · Raw pair-frame splitter as a host component · Pair-frame splitter reaches the framing outcome · Raw field projection agrees with the pair decoder · Pair-frame splitter extracts both raw fields · Embedded pair-frame splitter preserves caller stacks · Pair-frame splitter fails on malformed first-field framing · Pair-frame splitter projects every well-framed input in linear time

DefinitionStack layout of the raw pair-frame splitter#✓fully proved

Explicit stack layout of the projection invariant.

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

Uses 1 · Used by 10

Statement usesStacks of the raw pair-frame splitter

Used byFour-output decoder fails on malformed input · Four-output decoder emits four canonical outputs on success · Number-pair projector normalizes both fields of a raw pair frame · Number-pair projector fails on malformed framing in linear time · Pair-frame splitter reaches the framing outcome · Raw field projection agrees with the pair decoder · Pair-frame splitter extracts both raw fields · Embedded pair-frame splitter preserves caller stacks · Pair-frame splitter fails on malformed first-field framing · Pair-frame splitter projects every well-framed input in linear time

TheoremPair-frame splitter extracts both raw fields#✓fully proved

Extract both raw fields, restore first-field order, and clear scratch in exactly two steps per first-field bit plus two.

theorem run_delimit (p r out : List Bool) (v : Bool) :
    ∃ v', Run prog (2 * p.length + 2)
      ⟨some .read, v, st (delimit p ++ r) out []⟩
      ⟨some .good, v', st r (p ++ out) []⟩

Uses 9 · Used by 4

Statement usesStacks of the raw pair-frame splitter · Control labels of the raw pair-frame splitter · Program of the raw pair-frame splitter · Stack layout of the raw pair-frame splitter · Self-delimiting form of a bitstring · Exact-length runs of a TM2 machine

Proof usesReading a complete framed block · Flag bit of a machine state · Running the bit-moving loop

Used byFour-output decoder fails on malformed input · Four-output decoder emits four canonical outputs on success · Number-pair projector normalizes both fields of a raw pair frame · Pair-frame splitter projects every well-framed input in linear time

TheoremPair-frame splitter projects every well-framed input in linear time#✓fully proved

Every successful raw pair frame is projected within input length plus one; its two payloads are left unnormalized.

theorem run_some {x p r : List Bool}
    (h : undelimit x = some (p, r)) (out : List Bool) (v : Bool) :
    ∃ v', RunLe prog (x.length + 1)
      ⟨some .read, v, st x out []⟩
      ⟨some .good, v', st r (p ++ out) []⟩

Uses 10 · Used by 2

Statement usesStacks of the raw pair-frame splitter · Control labels of the raw pair-frame splitter · Program of the raw pair-frame splitter · Stack layout of the raw pair-frame splitter · Parsing one self-delimiting block · Runs within a step budget

Proof usesPair-frame splitter extracts both raw fields · Parsing a self-delimiting block · Self-delimiting form of a bitstring · Exact-length runs of a TM2 machine

Used byPair-frame splitter reaches the framing outcome · Raw field projection agrees with the pair decoder

TheoremPair-frame splitter fails on malformed first-field framing#✓fully proved

Malformed first-field framing reaches the actual failure label. Scratch may contain a partial field and must be cleared before reuse.

theorem run_none {x : List Bool} (h : undelimit x = none)
    (out : List Bool) (v : Bool) :
    ∃ v' S, RunLe prog (x.length + 1)
      ⟨some .read, v, st x out []⟩ ⟨some .bad, v', S⟩

Uses 7 · Used by 3

Statement usesStacks of the raw pair-frame splitter · Control labels of the raw pair-frame splitter · Program of the raw pair-frame splitter · Stack layout of the raw pair-frame splitter · Parsing one self-delimiting block · Runs within a step budget

Proof usesFramed block reader fails on truncated framing

Used byFour-output decoder fails on malformed input · Number-pair projector fails on malformed framing in linear time · Pair-frame splitter reaches the framing outcome

AbbreviationRaw pair-frame splitter as a host component#✓fully proved

The finite component interface used by fixed nested-codec callers.

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

Uses 4

Statement usesComponent machine · Stacks of the raw pair-frame splitter · Control labels of the raw pair-frame splitter · Program of the raw pair-frame splitter

TheoremRaw field projection agrees with the pair decoder#✓fully proved

Raw field projection agrees with the existing pair decoder. This is not a runtime assumption or implementation of either element codec.

theorem run_decoded {α β : Type}
    [MetaMathlibExt.BitstringEncoding α] [MetaMathlibExt.BitstringEncoding β]
    {x : List Bool} {a : α} {b : β} (h : bitDecode x = some (a, b))
    (v : Bool) :
    ∃ p r v', RunLe prog (x.length + 1)
      ⟨some .read, v, st x [] []⟩ ⟨some .good, v', st r p []⟩ ∧
      bitDecode p = some a ∧ bitDecode r = some b

Uses 14

Statement usesStacks of the raw pair-frame splitter · Control labels of the raw pair-frame splitter · Program of the raw pair-frame splitter · Stack layout of the raw pair-frame splitter · 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 · Runs within a step budget

Proof usesPair-frame splitter projects every well-framed input in linear time · Decoded pair exposes its raw component payloads · Parsing a self-delimiting block

TheoremPair-frame splitter reaches the framing outcome#✓fully proved

Total framing outcome, without prematurely accepting either field as a value of its eventual element type.

theorem run (x : List Bool) (v : Bool) :
    ∃ v' S, RunLe prog (x.length + 1)
      ⟨some .read, v, st x [] []⟩
      ⟨some (if (undelimit x).isSome then .good else .bad), v', S⟩ ∧
      ∀ p r, undelimit x = some (p, r) → S = st r p []

Uses 8 · Used by 1

Statement usesStacks of the raw pair-frame splitter · Control labels of the raw pair-frame splitter · Program of the raw pair-frame splitter · Stack layout of the raw pair-frame splitter · Parsing one self-delimiting block · Runs within a step budget

Proof usesPair-frame splitter fails on malformed first-field framing · Pair-frame splitter projects every well-framed input in linear time

Used byEmbedded pair-frame splitter preserves caller stacks

TheoremEmbedded pair-frame splitter preserves caller stacks#✓fully proved

Embedded projection preserves all caller stacks outside the three-stack workspace, even when framing fails.

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 (x.length + 1)
      ⟨some (φ .read), v, S⟩
      ⟨some (φ (if (undelimit x).isSome then .good else .bad)), v', T⟩ ∧
      MetaMathlibExt.TM2Embedding.Frame E S T ∧
      ∀ p r, undelimit x = some (p, r) →
        MetaMathlibExt.TM2Embedding.Agree E (st r p []) T

Uses 12

Statement usesStacks of the raw pair-frame splitter · Control labels of the raw pair-frame splitter · Program of the raw pair-frame splitter · Stack layout of the raw pair-frame splitter · Parsing one self-delimiting block · 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 usesPair-frame splitter reaches the framing outcome · Run embedding for bounded runs

11 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.