Projecting and normalizing a pair of binary naturals

InductiveStacks of the number-pair projector#✓fully proved

Pair workspace, one reusable Nat buffer, and two canonical outputs.

inductive K | pair (k : PairSplit.K) | buffer | left | right
  deriving DecidableEq

Uses 1 · Used by 32

Statement usesStacks of the raw pair-frame splitter

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 · Stacks of the pair-list projector · Stack embedding of the pair normalizer in the pair-list projector · 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 · Eleven-stack invariant of the pair-list projector · Four-output pair-list decoder as a host component · List-projector stack embedding in the four-output decoder · Stacks of the four-output pair-list 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 · Number-pair projector as a host component · 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

InductiveControl labels of the number-pair projector#✓fully proved

Pair projection followed by normalization of the two fields.

inductive Lab | pair (l : PairSplit.Lab)
  | norm (second : Bool) (l : NormalizeMachine.Lab) | good | bad
  deriving DecidableEq

Uses 2 · Used by 22

Statement usesControl labels of the payload normalizer machine · Control labels of the raw pair-frame splitter

Used byPair-list projector as a host component · Pair-list projector emits one weight and one value frame per item · Control labels of the pair-list projector · 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 fails on malformed input · Four-output decoder emits four canonical outputs on success · Number-pair projector as a host component · Label map chaining the two field normalizers · 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

DefinitionPair-frame splitter stack embedding in the number-pair projector#✓fully proved

The pair-frame component acts only on its three own stacks.

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

Uses 3 · Used by 3

Statement usesStacks of the number-pair projector · Stacks of the raw pair-frame splitter · Stack embedding

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

DefinitionField-normalizer stack embedding in the number-pair projector#✓fully proved

Each normalizer consumes its raw field, sharing only an empty buffer.

def normEmb (second : Bool) :
    SEmb (fun _ : NormalizeMachine.K => Bool) (fun _ : K => Bool) where
  e
    | .input => if second then .pair .input else .pair .left
    | .buffer => .buffer
    | .output => if second then .right else .left
  inj a b h := by cases second <;> cases a <;> cases b <;> simp_all
  ι _ := Equiv.refl Bool

Uses 4 · Used by 2

Statement usesStacks of the payload normalizer machine · Stacks of the number-pair projector · Stacks of the raw pair-frame splitter · Stack embedding

Used byProgram of the number-pair projector · Number-pair projector normalizes both fields of a raw pair frame

DefinitionPair-frame splitter halt redirection in the number-pair projector#✓fully proved

Only actual pair halt labels are redirected.

def pairLabel : PairSplit.Lab → Lab
  | .good => .norm false (.read none)
  | .bad => .bad
  | l => .pair l

Uses 3 · Used by 3

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

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

DefinitionLabel map chaining the two field normalizers#✓fully proved

Normalizing the first field continues with the second.

def normLabel (second : Bool) : NormalizeMachine.Lab → Lab
  | .done => if second then .good else .norm true (.read none)
  | l => .norm second l

Uses 2 · Used by 2

Statement usesControl labels of the payload normalizer machine · Control labels of the number-pair projector

Used byProgram of the number-pair projector · Number-pair projector normalizes both fields of a raw pair frame

DefinitionProgram of the number-pair projector#✓fully proved

All work is performed by the two existing finite components.

def prog : Lab → TM2.Stmt (fun _ : K => Bool) Lab Bool
  | .pair l => mapS pairEmb pairLabel (PairSplit.prog l)
  | .norm s l => mapS (normEmb s) (normLabel s) (NormalizeMachine.prog l)
  | .good | .bad => .halt

Uses 13 · Used by 12

Statement usesStacks of the payload normalizer machine · Control labels of the payload normalizer machine · Program of the payload normalizer machine · Stacks of the number-pair projector · Control labels of the number-pair projector · Field-normalizer stack embedding in the number-pair projector · Label map chaining the two field normalizers · Pair-frame splitter stack embedding in the number-pair projector · Pair-frame splitter halt redirection in 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 byPair-list projector emits one weight and one value frame per item · Program of the pair-list projector · Pair-list projector fails on malformed input in linear time · Program of the four-output pair-list decoder · Four-output decoder fails on malformed input · Four-output decoder emits four canonical outputs on success · Number-pair projector as a host component · 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

DefinitionSix-stack invariant of the number-pair projector#✓fully proved

Explicit six-stack invariant.

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

Uses 2 · Used by 14

Statement usesStacks of the number-pair projector · Stacks of the raw pair-frame splitter

Used byPair-list projector main loop emits both lists in reverse · Pair-list projector emits one weight and one value frame per item · 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 decoder fails on malformed input · Four-output decoder emits four canonical outputs on success · Stack invariant of the four-output pair-list decoder · 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

TheoremNumber-pair projector normalizes both fields of a raw pair frame#✓fully proved

Every raw pair frame is projected and normalized without changing the total Nat decoding semantics. Previous output suffixes survive.

theorem run_delimit (p r left right : List Bool) (v : Bool) :
    ∃ v', RunLe prog (2 * (delimit p ++ r).length + 6)
      ⟨some (.pair .read), v, st (delimit p ++ r) [] [] [] left right⟩
      ⟨some .good, v',
        st [] [] [] [] (normalizeNat p ++ left) (normalizeNat r ++ right)⟩

Uses 29 · Used by 1

Statement usesNormalization of a raw binary natural-number payload · Stacks of the number-pair projector · Control labels of the number-pair projector · Program of the number-pair projector · Six-stack invariant of the number-pair projector · Stacks of the raw pair-frame splitter · Control labels of the raw pair-frame splitter · Self-delimiting form of a bitstring · Runs within a step budget

Proof usesStacks of the payload normalizer machine · Control labels of the payload normalizer machine · Program of the payload normalizer machine · Stack contents for the payload normalizer invariant · Field-normalizer stack embedding in the number-pair projector · Label map chaining the two field normalizers · Pair-frame splitter stack embedding in the number-pair projector · Pair-frame splitter halt redirection in 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 · Number normalizer restores its work stacks and prepends its answer · 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 byNumber-pair projector yields both canonical payloads on success

TheoremDecoding a pair of naturals fails exactly on a malformed first frame#✓fully proved

Pair Nat decoding fails exactly when the first frame is malformed; both raw field payloads use Mathlib's total Nat decoder.

theorem decode_pair_nat (x : List Bool) :
    bitDecode (α := Nat × Nat) x = (undelimit x).map (fun p =>
      (Computability.decodeNat p.1, Computability.decodeNat p.2))

Uses 6 · Used by 1

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

Used byNumber-pair projector fails on malformed framing in linear time

TheoremNumber-pair projector yields both canonical payloads on success#✓fully proved

A successful pair decode produces both canonical binary payloads, with all scratch empty and arbitrary previous output suffixes preserved.

theorem run_some {x : List Bool} {m n : Nat}
    (h : bitDecode x = some (m, n)) (left right : List Bool) (v : Bool) :
    ∃ v', RunLe prog (2 * x.length + 6)
      ⟨some (.pair .read), v, st x [] [] [] left right⟩
      ⟨some .good, v', st [] [] [] [] (Computability.encodeNat m ++ left)
        (Computability.encodeNat n ++ right)⟩

Uses 17 · Used by 3

Statement usesStacks of the number-pair projector · Control labels of the number-pair projector · Program of the number-pair projector · Six-stack invariant 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 · Runs within a step budget

Proof usesNormalization of a raw binary natural-number payload · Payload normalization agrees with decode-then-encode · Number-pair projector normalizes both fields of a raw pair frame · Decoded pair exposes its raw component payloads

Used byPair-list projector emits one weight and one value frame per item · Four-output decoder emits four canonical outputs on success · Number-pair projector reaches the decoding outcome

TheoremNumber-pair projector fails on malformed framing in linear time#✓fully proved

Malformed pair framing fails in linear time. Private partial workspace contents must be cleared before another invocation.

theorem run_none {x : List Bool} (h : bitDecode (α := Nat × Nat) x = none)
    (left right : List Bool) (v : Bool) :
    ∃ v' S, RunLe prog (x.length + 1)
      ⟨some (.pair .read), v, st x [] [] [] left right⟩
      ⟨some .bad, v', S⟩

Uses 25 · Used by 3

Statement usesStacks of the number-pair projector · Control labels of the number-pair projector · Program of the number-pair projector · Six-stack invariant 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 · Runs within a step budget

Proof usesDecoding a pair of naturals fails exactly on a malformed first frame · Pair-frame splitter stack embedding in the number-pair projector · Pair-frame splitter halt redirection in the number-pair projector · Program of the raw pair-frame splitter · Pair-frame splitter fails on malformed first-field framing · Stack layout of the raw pair-frame splitter · 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

Used byPair-list projector fails on malformed input in linear time · Four-output decoder fails on malformed input · Number-pair projector reaches the decoding outcome

AbbreviationNumber-pair projector as a host component#✓fully proved

The concrete two-Nat projector in the existing Host interface.

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

Uses 7 · Used by 1

Statement usesControl labels of the payload normalizer machine · Component machine · 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

Used byFour-output pair-list decoder as a host component

TheoremCanonical payloads of a decoded pair are bounded by the raw input#✓fully proved

Canonical output payload sizes are bounded by the raw input size, even when either field had a noncanonical final zero bit.

theorem decoded_payload_length_le {x : List Bool} {m n : Nat}
    (h : bitDecode x = some (m, n)) :
    (Computability.encodeNat m).length + (Computability.encodeNat n).length ≤
      x.length + 1

Uses 10 · Used by 3

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

Proof usesPayload normalization adds at most one bit · Normalization of a raw binary natural-number payload · Payload normalization agrees with decode-then-encode · Decoded pair exposes its raw component payloads

Used byPair-list projector emits one weight and one value frame per item · Projected pair lists total at most four times the input length · Four-output decoder output is at most twice the input length

TheoremNumber-pair projector reaches the decoding outcome#✓fully proved

Total decoder outcome with exact successful output and empty private scratch. Failure does not promise reusable workspace contents.

theorem run (x : List Bool) (v : Bool) :
    ∃ v' S, RunLe prog (2 * x.length + 6)
      ⟨some (.pair .read), v, st x [] [] [] [] []⟩
      ⟨some (if (bitDecode (α := Nat × Nat) x).isSome
        then .good else .bad), v', S⟩ ∧
      ∀ m n : Nat, bitDecode x = some (m, n) →
        S = st [] [] [] [] (Computability.encodeNat m)
          (Computability.encodeNat n)

Uses 16 · Used by 1

Statement usesStacks of the number-pair projector · Control labels of the number-pair projector · Program of the number-pair projector · Six-stack invariant 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 · Runs within a step budget

Proof usesNumber-pair projector fails on malformed framing in linear time · Number-pair projector yields both canonical payloads on success · Exact-length runs of a TM2 machine

Used byEmbedded number-pair projector preserves outside stacks

TheoremEmbedded number-pair projector preserves outside stacks#✓fully proved

Callers may embed this concrete projector without disturbing outside stacks. A failed workspace must be cleared before reuse.

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 : List Bool) (v : Bool) (S : ∀ j, List (Γ j))
    (hs : Agree E (st x [] [] [] [] []) S) :
    ∃ v' T, RunLe M (2 * x.length + 6)
      ⟨some (φ (.pair .read)), v, S⟩
      ⟨some (φ (if (bitDecode (α := Nat × Nat) x).isSome
        then .good else .bad)), v', T⟩ ∧ Frame E S T ∧
      ∀ m n : Nat, bitDecode x = some (m, n) →
        Agree E (st [] [] [] [] (Computability.encodeNat m)
          (Computability.encodeNat n)) T

Uses 19

Statement usesStacks of the number-pair projector · Control labels of the number-pair projector · Program of the number-pair projector · Six-stack invariant of the number-pair projector · 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 · 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 usesNumber-pair projector reaches the decoding outcome · 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.