A finite List Nat canonicalizer

InductiveStacks of the list-of-naturals canonicalizer#✓fully proved

External input, reverse accumulator, final output, and Nat workspace.

inductive K | input | acc | output | nat (k : NormalizeMachine.K)
  deriving DecidableEq

Uses 1 · Used by 22

Statement usesStacks of the payload normalizer machine

Used byList canonicalizer normalizes a sequence of framed payloads · List-of-naturals canonicalizer as a host component · List canonicalizer normalizes one element · Stack embedding of the number normalizer in the list canonicalizer · Program of the list-of-naturals canonicalizer · List canonicalizer reaches the decoding outcome with canonical output · Embedded list canonicalizer preserves outside stacks · List canonicalizer fails on malformed input · List canonicalizer runs in linear time on decodable input · Workspace layout of the list-of-naturals canonicalizer · Raw-input SUBSET-SUM to PARTITION machine as a host component · Raw-input PARTITION membership machine as a host component · Numeric-core workspace of the raw-input PARTITION membership machine · SUBSET-SUM to PARTITION map is polynomial-time · PARTITION to SUBSET-SUM map is polynomial-time · Stacks of the raw-input SUBSET-SUM to PARTITION machine · Stacks of the raw-input PARTITION membership machine · Normalizer workspace of the raw-input PARTITION membership machine · Program of the raw-input SUBSET-SUM to PARTITION machine · Program of the raw-input PARTITION membership machine · Quadratic run of the raw-input SUBSET-SUM to PARTITION machine · Raw-input PARTITION membership machine runs in quadratic time

DefinitionStack embedding of the number normalizer in the list canonicalizer#✓fully proved

Only the Nat workspace is visible to the shared normalizer.

def emb : SEmb (fun _ : NormalizeMachine.K => Bool) (fun _ : K => Bool) where
  e := K.nat
  inj _ _ h := K.nat.inj h
  ι _ := Equiv.refl Bool

Uses 3 · Used by 4

Statement usesStacks of the payload normalizer machine · Stacks of the list-of-naturals canonicalizer · Stack embedding

Used byList canonicalizer normalizes one element · Program of the list-of-naturals canonicalizer · Quadratic run of the raw-input SUBSET-SUM to PARTITION machine · Raw-input PARTITION membership machine runs in quadratic time

InductiveControl labels of the list-of-naturals canonicalizer#✓fully proved

The normalizer's halt resumes frame emission.

inductive Lab
  | loop | block | back | nat (l : NormalizeMachine.Lab) | emit | finish
  | good | bad
  deriving DecidableEq

Uses 1 · Used by 18

Statement usesControl labels of the payload normalizer machine

Used byList canonicalizer normalizes a sequence of framed payloads · List-of-naturals canonicalizer as a host component · List canonicalizer normalizes one element · Label embedding of the number normalizer in the list canonicalizer · Program of the list-of-naturals canonicalizer · List canonicalizer reaches the decoding outcome with canonical output · Embedded list canonicalizer preserves outside stacks · List canonicalizer fails on malformed input · List canonicalizer runs in linear time on decodable input · Raw-input SUBSET-SUM to PARTITION machine as a host component · Raw-input PARTITION membership machine as a host component · PARTITION to SUBSET-SUM map is polynomial-time · Control labels of the raw-input SUBSET-SUM to PARTITION machine · Control labels of the raw-input PARTITION membership machine · Program of the raw-input SUBSET-SUM to PARTITION machine · Program of the raw-input PARTITION membership machine · Quadratic run of the raw-input SUBSET-SUM to PARTITION machine · Raw-input PARTITION membership machine runs in quadratic time

DefinitionLabel embedding of the number normalizer in the list canonicalizer#✓fully proved

Label embedding of the actual shared Nat normalizer.

def natLabel : NormalizeMachine.Lab → Lab
  | .done => .emit
  | l => .nat l

Uses 2 · Used by 4

Statement usesControl labels of the payload normalizer machine · Control labels of the list-of-naturals canonicalizer

Used byList canonicalizer normalizes one element · Program of the list-of-naturals canonicalizer · Quadratic run of the raw-input SUBSET-SUM to PARTITION machine · Raw-input PARTITION membership machine runs in quadratic time

DefinitionProgram of the list-of-naturals canonicalizer#✓fully proved

The concrete canonicalizer program.

def prog : Lab → TM2.Stmt (fun _ : K => Bool) Lab Bool
  | .loop => .peek .input (fun _ o => o.isSome) <| .branch id
      (.goto fun _ => .block) (.goto fun _ => .finish)
  | .block => Block.read .input (.nat .output) some id .block .back .bad
  | .back => moveB (.nat .output) (.nat .input) some id .back
      (.nat (.read none))
  | .nat l => mapS emb natLabel (NormalizeMachine.prog l)
  | .emit => emitFrame (.nat .output) .acc some id .emit .loop
  | .finish => moveB .acc .output some id .finish .good
  | .good | .bad => .halt

Uses 12 · Used by 11

Statement usesMachine step reading one framed payload pair · Stacks of the payload normalizer machine · Control labels of the payload normalizer machine · Program of the payload normalizer machine · Stacks of the list-of-naturals canonicalizer · Control labels of the list-of-naturals canonicalizer · Stack embedding of the number normalizer in the list canonicalizer · Label embedding of the number normalizer in the list canonicalizer · Reversed self-delimiting frame emitter · Translating a statement along a stack embedding · Flag bit of a machine state · Bit-moving loop

Used byList canonicalizer normalizes a sequence of framed payloads · List-of-naturals canonicalizer as a host component · List canonicalizer normalizes one element · List canonicalizer reaches the decoding outcome with canonical output · Embedded list canonicalizer preserves outside stacks · List canonicalizer fails on malformed input · List canonicalizer runs in linear time on decodable input · Program of the raw-input SUBSET-SUM to PARTITION machine · Program of the raw-input PARTITION membership machine · Quadratic run of the raw-input SUBSET-SUM to PARTITION machine · Raw-input PARTITION membership machine runs in quadratic time

DefinitionWorkspace layout of the list-of-naturals canonicalizer#✓fully proved

Workspace layout for the composition invariant.

def st (x acc out : List Bool) (s : NormalizeMachine.K → List Bool) :
    K → List Bool
  | .input => x
  | .acc => acc
  | .output => out
  | .nat k => s k

Uses 2 · Used by 8

Statement usesStacks of the payload normalizer machine · Stacks of the list-of-naturals canonicalizer

Used byList canonicalizer normalizes a sequence of framed payloads · List canonicalizer normalizes one element · List canonicalizer reaches the decoding outcome with canonical output · Embedded list canonicalizer preserves outside stacks · List canonicalizer fails on malformed input · List canonicalizer runs in linear time on decodable input · Quadratic run of the raw-input SUBSET-SUM to PARTITION machine · Raw-input PARTITION membership machine runs in quadratic time

TheoremList canonicalizer normalizes one element#✓fully proved

One list element is normalized and appended to the reverse accumulator; every scratch stack is ready for the next call.

theorem element_run (p x acc out : List Bool) (v : Bool) :
    RunLe prog (8 * (delimit p).length)
      ⟨some .loop, v, st (delimit p ++ x) acc out
        (NormalizeMachine.st [] [] [])⟩
      ⟨some .loop, false, st x
        ((delimit (normalizeNat p)).reverse ++ acc) out
        (NormalizeMachine.st [] [] [])⟩

Uses 27 · Used by 2

Statement usesStacks of the payload normalizer machine · Stack contents for the payload normalizer invariant · Normalization of a raw binary natural-number payload · Stacks of the list-of-naturals canonicalizer · Control labels of the list-of-naturals canonicalizer · Program of the list-of-naturals canonicalizer · Workspace layout of the list-of-naturals canonicalizer · Self-delimiting form of a bitstring · Runs within a step budget

Proof usesReading a complete framed block · Control labels of the payload normalizer machine · Program of the payload normalizer machine · Payload normalization adds at most one bit · Stack embedding of the number normalizer in the list canonicalizer · Label embedding of the number normalizer in the list canonicalizer · Frame emitter takes one step per payload bit plus one · 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 · Flag bit of a machine state · Exact-length runs of a TM2 machine · A single step executes the statement at the current label · Running the bit-moving loop

Used byList canonicalizer normalizes a sequence of framed payloads · List canonicalizer fails on malformed input

TheoremList canonicalizer normalizes a sequence of framed payloads#✓fully proved

Normalize any finite sequence of framed Nat payloads. The payloads need not be canonical, and previous accumulator/output suffixes survive.

theorem blocks_run (bs : List (List Bool)) :
    ∀ (acc out : List Bool) (v : Bool),
    RunLe prog (8 * ((bs.map delimit).flatten).length + 1)
      ⟨some .loop, v, st ((bs.map delimit).flatten) acc out
        (NormalizeMachine.st [] [] [])⟩
      ⟨some .finish, false, st []
        (((bs.map (fun p => delimit (normalizeNat p))).flatten).reverse ++ acc)
        out (NormalizeMachine.st [] [] [])⟩

Uses 12 · Used by 1

Statement usesStacks of the payload normalizer machine · Stack contents for the payload normalizer invariant · Normalization of a raw binary natural-number payload · Stacks of the list-of-naturals canonicalizer · Control labels of the list-of-naturals canonicalizer · Program of the list-of-naturals canonicalizer · Workspace layout of the list-of-naturals canonicalizer · Self-delimiting form of a bitstring · Runs within a step budget

Proof usesList canonicalizer normalizes one element · Exact-length runs of a TM2 machine · A single step executes the statement at the current label

Used byList canonicalizer runs in linear time on decodable input

TheoremList canonicalizer runs in linear time on decodable input#✓fully proved

Successful raw List Nat decoding is implemented in linear time, with canonical output and all private scratch stacks empty.

theorem run_some {x : List Bool} {as : List Nat}
    (h : bitDecode x = some as) (out : List Bool) (v : Bool) :
    ∃ v', RunLe prog (11 * x.length + 2)
      ⟨some .loop, v, st x [] out (NormalizeMachine.st [] [] [])⟩
      ⟨some .good, v', st [] [] (bitEncode as ++ out)
        (NormalizeMachine.st [] [] [])⟩

Uses 24 · Used by 1

Statement usesStacks of the payload normalizer machine · Stack contents for the payload normalizer invariant · Stacks of the list-of-naturals canonicalizer · Control labels of the list-of-naturals canonicalizer · Program of the list-of-naturals canonicalizer · Workspace layout of the list-of-naturals canonicalizer · 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 usesNormalization of a raw binary natural-number payload · List canonicalizer normalizes a sequence of framed payloads · Successful block parsing reconstructs the input · Decoding a list of naturals is block parsing then number decoding · Re-encoding decoded payloads normalizes each one · Normalizing framed number payloads at most triples the length · Flag bit of a machine state · Exact-length runs of a TM2 machine · Running the bit-moving loop

Used byList canonicalizer reaches the decoding outcome with canonical output

TheoremList canonicalizer fails on malformed input#✓fully proved

Every malformed raw List Nat input reaches the failure endpoint. The accumulator and Nat output may contain partial data; clear the workspace before reuse. No output claim is made for a failed parse.

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

Uses 22 · Used by 1

Statement usesStacks of the payload normalizer machine · Stack contents for the payload normalizer invariant · Stacks of the list-of-naturals canonicalizer · Control labels of the list-of-naturals canonicalizer · Program of the list-of-naturals canonicalizer · Workspace layout of the list-of-naturals canonicalizer · 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 · Normalization of a raw binary natural-number payload · List canonicalizer normalizes one element · 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 byList canonicalizer reaches the decoding outcome with canonical output

AbbreviationList-of-naturals canonicalizer as a host component#✓fully proved

The List Nat canonicalizer uses the existing finite Host interface.

abbrev component : Host.Comp where
  K := K
  Γ := fun _ => Bool
  L := Lab
  prog := prog
  ks := [.input, .acc, .output, .nat .input, .nat .buffer, .nat .output]
  ks_nodup := by decide
  mem_ks k := by
    cases k with
    | input | acc | output => decide
    | nat k => cases k <;> decide

Uses 6

Statement usesStacks of the payload normalizer machine · Control labels of the payload normalizer machine · Component machine · Stacks of the list-of-naturals canonicalizer · Control labels of the list-of-naturals canonicalizer · Program of the list-of-naturals canonicalizer

TheoremList canonicalizer reaches the decoding outcome with canonical output#✓fully proved

A total success/failure contract at the two actual halt labels. Success has canonical output; failure exposes no partial-output promise.

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

Uses 18 · Used by 1

Statement usesStacks of the payload normalizer machine · Stack contents for the payload normalizer invariant · Stacks of the list-of-naturals canonicalizer · Control labels of the list-of-naturals canonicalizer · Program of the list-of-naturals canonicalizer · Workspace layout of the list-of-naturals canonicalizer · 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 usesList canonicalizer fails on malformed input · List canonicalizer runs in linear time on decodable input · Exact-length runs of a TM2 machine

Used byEmbedded list canonicalizer preserves outside stacks

TheoremEmbedded list canonicalizer preserves outside stacks#✓fully proved

Embed the concrete normalizer in a caller, preserving every stack outside its workspace on both success and failure. Entry requires clean scratch and output stacks. After bad, clear partial workspace data before another invocation.

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 [] [] (NormalizeMachine.st [] [] [])) S) :
    ∃ v' T, RunLe M (11 * x.length + 2)
      ⟨some (φ .loop), v, S⟩
      ⟨some (φ (if (bitDecode (α := List Nat) x).isSome
        then .good else .bad)), v', T⟩ ∧ Frame E S T ∧
      ∀ as : List Nat, bitDecode x = some as →
        Agree E (st [] [] (bitEncode as) (NormalizeMachine.st [] [] [])) T

Uses 21 · Used by 2

Statement usesStack contents for the payload normalizer invariant · Stacks of the list-of-naturals canonicalizer · Control labels of the list-of-naturals canonicalizer · Program of the list-of-naturals canonicalizer · Workspace layout of the list-of-naturals canonicalizer · 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 payload normalizer machine · List canonicalizer reaches the decoding outcome with canonical output · Run embedding for bounded runs

Used byQuadratic run of the raw-input SUBSET-SUM to PARTITION machine · Raw-input PARTITION membership machine runs in quadratic time

13 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.