Four canonical outputs from a Nat-pair list and a Nat pair

InductiveStacks of the four-output pair-list decoder#✓fully proved

Two disjoint existing workspaces; the pair buffer also serves the initial outer-frame split and is cleared before normalization starts.

inductive K | items (k : ListNatPair.K) | pair (k : NatPair.K)
  deriving DecidableEq

Uses 2 · Used by 10

Statement usesStacks of the pair-list projector · Stacks of the number-pair projector

Used byFour-output pair-list decoder as a host component · List-projector stack embedding in the four-output decoder · Final pair-projector stack embedding in the four-output decoder · 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 · Stack invariant of the four-output pair-list decoder

InductiveControl labels of the four-output pair-list decoder#✓fully proved

The existing split, list projector, and final pair normalizer.

inductive Lab | split (l : PairSplit.Lab) | items (l : ListNatPair.Lab)
  | pair (l : NatPair.Lab) | good | bad
  deriving DecidableEq

Uses 3 · Used by 9

Statement usesControl labels of the pair-list projector · Control labels of the number-pair projector · Control labels of the raw pair-frame splitter

Used byFour-output pair-list decoder as a host component · Label map from the list projector to the final pair 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

DefinitionOuter-splitter stack embedding in the four-output decoder#✓fully proved

The outer splitter reuses the final pair's input and empty buffer.

def splitEmb : SEmb (fun _ : PairSplit.K => Bool) (fun _ : K => Bool) where
  e
    | .input => .pair (.pair .input)
    | .left => .items .input
    | .scratch => .pair .buffer
  inj a b h := by cases a <;> cases b <;> simp_all
  ι _ := Equiv.refl Bool

Uses 5 · Used by 3

Statement usesStacks of the pair-list projector · Stacks of the four-output pair-list decoder · Stacks of the number-pair projector · Stacks of the raw pair-frame splitter · Stack embedding

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

DefinitionList-projector stack embedding in the four-output decoder#✓fully proved

The list projector has its own disjoint workspace.

def itemsEmb : SEmb (fun _ : ListNatPair.K => Bool) (fun _ : K => Bool) where
  e := K.items
  inj _ _ h := K.items.inj h
  ι _ := Equiv.refl Bool

Uses 4 · Used by 3

Statement usesStacks of the pair-list projector · Stacks of the four-output pair-list decoder · Stacks of the number-pair projector · Stack embedding

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

DefinitionFinal pair-projector stack embedding in the four-output decoder#✓fully proved

The final pair projector has its own disjoint workspace.

def pairEmb : SEmb (fun _ : NatPair.K => Bool) (fun _ : K => Bool) where
  e := K.pair
  inj _ _ h := K.pair.inj h
  ι _ := Equiv.refl Bool

Uses 4 · Used by 3

Statement usesStacks of the pair-list projector · Stacks of the four-output pair-list decoder · Stacks of the number-pair projector · Stack embedding

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

DefinitionLabel map from the outer splitter to the list projector#✓fully proved

Successful outer framing enters the item-list projector.

def splitLabel : PairSplit.Lab → Lab
  | .good => .items .loop
  | .bad => .bad
  | l => .split l

Uses 3 · Used by 3

Statement usesControl labels of the pair-list projector · Control labels of the four-output pair-list decoder · Control labels of the raw pair-frame splitter

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

DefinitionLabel map from the list projector to the final pair decoder#✓fully proved

Successful item projection enters the final pair decoder.

def itemsLabel : ListNatPair.Lab → Lab
  | .good => .pair (.pair .read)
  | .bad => .bad
  | l => .items l

Uses 4 · Used by 3

Statement usesControl labels of the pair-list projector · Control labels of the four-output pair-list decoder · Control labels of the number-pair projector · Control labels of the raw pair-frame splitter

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

DefinitionLabel map from final pair halts to the decoder outcomes#✓fully proved

The final pair's actual halts are the whole decoder's outcomes.

def pairLabel : NatPair.Lab → Lab
  | .good => .good
  | .bad => .bad
  | l => .pair l

Uses 4 · Used by 3

Statement usesControl labels of the payload normalizer machine · Control labels of the four-output pair-list decoder · Control labels of the number-pair projector · Control labels of the raw pair-frame splitter

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

DefinitionProgram of the four-output pair-list decoder#✓fully proved

The whole finite program is a composition of existing components.

def prog : Lab → TM2.Stmt (fun _ : K => Bool) Lab Bool
  | .split l => mapS splitEmb splitLabel (PairSplit.prog l)
  | .items l => mapS itemsEmb itemsLabel (ListNatPair.prog l)
  | .pair l => mapS pairEmb pairLabel (NatPair.prog l)
  | .good | .bad => .halt

Uses 18 · Used by 5

Statement usesStacks of the pair-list projector · Control labels of the pair-list projector · Program of the pair-list projector · Stacks of the four-output pair-list decoder · Control labels of the four-output pair-list decoder · List-projector stack embedding in the four-output decoder · Label map from the list projector to the final pair decoder · Final pair-projector stack embedding in the four-output decoder · Label map from final pair halts to the decoder outcomes · Outer-splitter stack embedding in the four-output decoder · Label map from the outer splitter to the list projector · Stacks of the number-pair projector · Control labels of the number-pair projector · Program of the number-pair projector · Stacks of the raw pair-frame splitter · Control labels of the raw pair-frame splitter · Program of the raw pair-frame splitter · Translating a statement along a stack embedding

Used byFour-output pair-list decoder as a host component · 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

DefinitionStack invariant of the four-output pair-list decoder#✓fully proved

Exact raw-field and four-output invariant, with empty private scratch. At entry the item field is empty and the entire raw input is pairRaw.

def st (itemsRaw pairRaw weights values capacity threshold : List Bool) :
    K → List Bool
  | .items k => ListNatPair.st itemsRaw [] [] weights values
      (NatPair.st [] [] [] [] [] []) k
  | .pair k => NatPair.st pairRaw [] [] [] capacity threshold k

Uses 5 · Used by 4

Statement usesStacks of the pair-list projector · Eleven-stack invariant of the pair-list projector · Stacks of the four-output pair-list decoder · Stacks of the number-pair projector · Six-stack invariant of the number-pair projector

Used byFour-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

TheoremFour-output decoder emits four canonical outputs on success#✓fully proved

The entire raw decoder emits four canonical outputs, preserving caller suffixes and emptying all input and private scratch on success.

theorem run_some {x : List Bool} {as : List (Nat × Nat)} {c t : Nat}
    (h : bitDecode x = some (as, (c, t)))
    (weights values capacity threshold : List Bool) (v : Bool) :
    ∃ w, RunLe prog (9 * x.length + 2)
      ⟨some (.split .read), v, st [] x weights values capacity threshold⟩
      ⟨some .good, w,
        st [] [] (bitEncode (as.map Prod.fst) ++ weights)
          (bitEncode (as.map Prod.snd) ++ values)
          (Computability.encodeNat c ++ capacity)
          (Computability.encodeNat t ++ threshold)⟩

Uses 44 · Used by 1

Statement usesStacks of the pair-list projector · Stacks of the four-output pair-list decoder · Control labels of the four-output pair-list decoder · Program of the four-output pair-list decoder · Stack invariant of the four-output pair-list decoder · Stacks of the number-pair projector · Stacks of the raw pair-frame splitter · Control labels 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 · Parsing a list of booleans into self-delimiting blocks · Bounded parsing of self-delimiting blocks · Runs within a step budget

Proof usesControl labels of the payload normalizer machine · Control labels of the pair-list projector · Program of the pair-list projector · Pair-list projector yields canonical weight and value lists · Eleven-stack invariant of the pair-list projector · List-projector stack embedding in the four-output decoder · Label map from the list projector to the final pair decoder · Final pair-projector stack embedding in the four-output decoder · Label map from final pair halts to the decoder outcomes · Outer-splitter stack embedding in the four-output decoder · Label map from the outer splitter to the list projector · Control labels of the number-pair projector · Program of the number-pair projector · Number-pair projector yields both canonical payloads on success · Six-stack invariant of the number-pair projector · Program of the raw pair-frame splitter · Pair-frame splitter extracts both raw fields · Stack layout of the raw pair-frame splitter · Decoded pair exposes its raw component payloads · Agreement of host and sub-machine stacks · Embedding of a machine in a host · Frame condition for a stack embedding · Stack embedding · Translating a statement along a stack embedding · Run embedding for bounded runs · Run embedding · Exact-length runs of a TM2 machine

Used byFour-output decoder reaches exactly the canonical decoding outcome

TheoremFour-output decoder output is at most twice the input length#✓fully proved

The combined newly emitted output size is at most twice raw input length, independently of decoded magnitudes and caller output suffixes.

theorem output_length_le {x : List Bool} {as : List (Nat × Nat)} {c t : Nat}
    (h : bitDecode x = some (as, (c, t))) :
    (bitEncode (as.map Prod.fst)).length +
      (bitEncode (as.map Prod.snd)).length +
      (Computability.encodeNat c).length +
      (Computability.encodeNat t).length ≤ 2 * x.length

Uses 11

Statement usesBitstring 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

Proof usesProjected pair lists total at most four times the input length · Canonical payloads of a decoded pair are bounded by the raw input · Decoded pair exposes its raw component payloads

TheoremFour-output decoder fails on malformed input#✓fully proved

Every failed raw decode reaches bad within the same whole-input bound. Failed owned workspace can be partial and must be discarded or cleared.

theorem run_none {x : List Bool}
    (h : bitDecode (α := List (Nat × Nat) × (Nat × Nat)) x = none)
    (weights values capacity threshold : List Bool) (v : Bool) :
    ∃ w S, RunLe prog (9 * x.length + 2)
      ⟨some (.split .read), v, st [] x weights values capacity threshold⟩
      ⟨some .bad, w, S⟩

Uses 46 · Used by 1

Statement usesStacks of the pair-list projector · Stacks of the four-output pair-list decoder · Control labels of the four-output pair-list decoder · Program of the four-output pair-list decoder · Stack invariant of the four-output pair-list decoder · Stacks of the number-pair projector · Stacks of the raw pair-frame splitter · Control labels 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 · Parsing a list of booleans into self-delimiting blocks · Bounded parsing of self-delimiting blocks · Runs within a step budget

Proof usesControl labels of the payload normalizer machine · Control labels of the pair-list projector · Program of the pair-list projector · Pair-list projector fails on malformed input in linear time · Pair-list projector yields canonical weight and value lists · Eleven-stack invariant of the pair-list projector · List-projector stack embedding in the four-output decoder · Label map from the list projector to the final pair decoder · Final pair-projector stack embedding in the four-output decoder · Label map from final pair halts to the decoder outcomes · Outer-splitter stack embedding in the four-output decoder · Label map from the outer splitter to the list projector · Control labels of the number-pair projector · Program of the number-pair projector · Number-pair projector fails on malformed framing in linear time · Six-stack invariant of the number-pair projector · Program of the raw pair-frame splitter · Pair-frame splitter extracts both raw fields · Pair-frame splitter fails on malformed first-field framing · Stack layout of the raw pair-frame splitter · Parsing a 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 · Translating a statement along a stack embedding · Run embedding for bounded runs · Run embedding · Exact-length runs of a TM2 machine

Used byFour-output decoder reaches exactly the canonical decoding outcome

AbbreviationFour-output pair-list decoder as a host component#✓fully proved

The fixed seventeen-stack decoder in the existing Host interface.

Cslib.Complexity.PolynomialEncoding.ListNatPairPair.component · 15 lines

abbrev component : Host.Comp where
  K := K
  Γ := fun _ => Bool
  L := Lab
  prog := prog
  ks := ListNatPair.component.ks.map K.items ++ NatPair.component.ks.map K.pair
  ks_nodup := by decide
  mem_ks k := by
    simp only [List.mem_append]
    cases k with
    | items k =>
      exact Or.inl (List.mem_map.mpr
        ⟨k, ListNatPair.component.mem_ks k, rfl⟩)
    | pair k =>
      exact Or.inr (List.mem_map.mpr ⟨k, NatPair.component.mem_ks k, rfl⟩)

Uses 13

Statement usesControl labels of the payload normalizer machine · Component machine · Stacks of the pair-list projector · Control labels of the pair-list projector · Pair-list projector as a host component · Stacks of the four-output pair-list decoder · Control labels of the four-output pair-list decoder · Program of the four-output pair-list decoder · Stacks of the number-pair projector · Control labels of the number-pair projector · Number-pair projector as a host component · Stacks of the raw pair-frame splitter · Control labels of the raw pair-frame splitter

TheoremFour-output decoder reaches exactly the canonical decoding outcome#✓fully proved

Total raw decoder contract with four output suffixes. Exactly the canonical decoder's success/failure label is reached, with empty scratch on success.

theorem run (x weights values capacity threshold : List Bool) (v : Bool) :
    ∃ w S, RunLe prog (9 * x.length + 2)
      ⟨some (.split .read), v, st [] x weights values capacity threshold⟩
      ⟨some (if (bitDecode (α := List (Nat × Nat) × (Nat × Nat)) x).isSome
        then .good else .bad), w, S⟩ ∧
      ∀ (as : List (Nat × Nat)) (c t : Nat),
        bitDecode x = some (as, (c, t)) →
        S = st [] [] (bitEncode (as.map Prod.fst) ++ weights)
          (bitEncode (as.map Prod.snd) ++ values)
          (Computability.encodeNat c ++ capacity)
          (Computability.encodeNat t ++ threshold)

Uses 19 · Used by 1

Statement usesStacks of the pair-list projector · Stacks of the four-output pair-list decoder · Control labels of the four-output pair-list decoder · Program of the four-output pair-list decoder · Stack invariant of the four-output pair-list decoder · Stacks of the number-pair projector · Stacks of the raw pair-frame splitter · Control labels 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 · Parsing a list of booleans into self-delimiting blocks · Bounded parsing of self-delimiting blocks · Runs within a step budget

Proof usesFour-output decoder fails on malformed input · Four-output decoder emits four canonical outputs on success

Used byEmbedded four-output decoder preserves outside stacks

TheoremEmbedded four-output decoder preserves outside stacks#✓fully proved

Embedded execution preserves every outside stack on both outcomes. Successful output suffixes survive and private scratch is empty. Failed workspace may be partial. Callers establish continuation-label separation.

Cslib.Complexity.PolynomialEncoding.ListNatPairPair.run_embedded · 16 lines

theorem run_embedded {J L : Type} [DecidableEq J] {Γ : J → Type}
    (E : SEmb (fun _ : K => Bool) Γ) (φ : Lab → L)
    {M : L → TM2.Stmt Γ L Bool} (hm : Embeds E φ prog M)
    (x weights values capacity threshold : List Bool) (v : Bool)
    (S : ∀ j, List (Γ j))
    (hs : Agree E (st [] x weights values capacity threshold) S) :
    ∃ w T, RunLe M (9 * x.length + 2)
      ⟨some (φ (.split .read)), v, S⟩
      ⟨some (φ (if (bitDecode (α := List (Nat × Nat) × (Nat × Nat)) x).isSome
        then .good else .bad)), w, T⟩ ∧ Frame E S T ∧
      ∀ (as : List (Nat × Nat)) (c t : Nat),
        bitDecode x = some (as, (c, t)) →
        Agree E (st [] [] (bitEncode (as.map Prod.fst) ++ weights)
          (bitEncode (as.map Prod.snd) ++ values)
          (Computability.encodeNat c ++ capacity)
          (Computability.encodeNat t ++ threshold)) T

Uses 23

Statement usesStacks of the four-output pair-list decoder · Control labels of the four-output pair-list decoder · Program of the four-output pair-list decoder · Stack invariant of the four-output pair-list decoder · Control labels 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 · 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 usesStacks of the pair-list projector · Four-output decoder reaches exactly the canonical decoding outcome · Stacks of the number-pair projector · Stacks of the raw pair-frame splitter · Run embedding for bounded runs

16 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.