A linear-time machine for total binary-payload normalization

InductiveStacks of the payload normalizer machine#✓fully proved

Input, reverse buffer, and output.

inductive K | input | buffer | output
  deriving DecidableEq

Used by 27

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 · Stacks of the list-of-naturals 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 · Payload normalizer as a host component · Payload normalization is polynomial-time · Program of the payload normalizer machine · Read phase of the payload normalizer consumes each bit once · Linear step bound for the payload normalizer machine · Stack contents for the payload normalizer invariant · Number normalizer restores its work stacks and prepends its answer · Field-normalizer stack embedding in the number-pair projector · Program of the number-pair projector · Number-pair projector normalizes both fields of a raw pair frame · Raw-input SUBSET-SUM to PARTITION machine as a host component · Raw-input PARTITION membership machine as a host component · SUBSET-SUM to PARTITION map is polynomial-time · PARTITION to SUBSET-SUM map is polynomial-time · Quadratic run of the raw-input SUBSET-SUM to PARTITION machine · Raw-input PARTITION membership machine runs in quadratic time

InductiveControl labels of the payload normalizer machine#✓fully proved

The reader records the last payload bit; none means empty input.

inductive Lab | read (last : Option Bool) | copy | done
  deriving DecidableEq

Used by 31

Used byList-of-naturals canonicalizer as a host component · List canonicalizer normalizes one element · Control labels of the list-of-naturals canonicalizer · Label embedding of the number normalizer in the list canonicalizer · Program of the list-of-naturals canonicalizer · Payload normalizer as a host component · Payload normalization is polynomial-time · Program of the payload normalizer machine · Read phase of the payload normalizer consumes each bit once · Linear step bound for the payload normalizer machine · Pair-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 · Pair-list projector fails on malformed input in linear time · Four-output pair-list decoder as a host component · Label map from final pair halts to the decoder outcomes · Four-output decoder fails on malformed input · Four-output decoder emits four canonical outputs on success · Number normalizer restores its work stacks and prepends its answer · Number-pair projector as a host component · Control labels of the number-pair projector · 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 normalizes both fields of a raw pair frame · Raw-input SUBSET-SUM to PARTITION machine as a host component · Raw-input PARTITION membership machine as a host component · 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

DefinitionProgram of the payload normalizer machine#✓fully proved

Normalization using only Boolean stack symbols and finite control.

def prog : Lab → TM2.Stmt (fun _ : K => Bool) Lab Bool
  | .read last =>
    .peek .input (fun _ o => o.isSome) <| .branch id
      (.pop .input (fun _ o => o.getD false) <|
        .push .buffer id <| .goto fun b => .read (some b))
      (if last = some false then
        .push .buffer (fun _ => true) (.goto fun _ => .copy)
       else .goto fun _ => .copy)
  | .copy => moveB .buffer .output some id .copy .done
  | .done => .halt

Uses 4 · Used by 11

Statement usesStacks of the payload normalizer machine · Control labels of the payload normalizer machine · Flag bit of a machine state · Bit-moving loop

Used byList canonicalizer normalizes one element · Program of the list-of-naturals canonicalizer · Payload normalizer as a host component · Payload normalization is polynomial-time · Read phase of the payload normalizer consumes each bit once · Linear step bound for the payload normalizer machine · Number normalizer restores its work stacks and prepends its answer · Program of the number-pair projector · Number-pair projector normalizes both fields of a raw pair frame · Quadratic run of the raw-input SUBSET-SUM to PARTITION machine · Raw-input PARTITION membership machine runs in quadratic time

DefinitionStack contents for the payload normalizer invariant#✓fully proved

The three stack contents used in the run invariant.

def st (input buffer output : List Bool) : K → List Bool
  | .input => input
  | .buffer => buffer
  | .output => output

Uses 1 · Used by 13

Statement usesStacks of the payload normalizer machine

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 · Payload normalization is polynomial-time · Read phase of the payload normalizer consumes each bit once · Linear step bound for the payload normalizer machine · Number normalizer restores its work stacks and prepends its answer · Number-pair projector normalizes both fields of a raw pair frame · Quadratic run of the raw-input SUBSET-SUM to PARTITION machine · Raw-input PARTITION membership machine runs in quadratic time

TheoremRead phase of the payload normalizer consumes each bit once#✓fully proved

The read phase consumes each input bit once and optionally adds the implicit terminal one. The prefix records already-consumed input.

theorem read_run (xs : List Bool) : ∀ (pre out : List Bool) (v : Bool),
    Run prog (xs.length + 1)
      ⟨some (.read pre.getLast?), v, st xs pre.reverse out⟩
      ⟨some .copy, false, st [] (normalizeNat (pre ++ xs)).reverse out⟩

Uses 7 · Used by 2

Statement 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 · Normalization of a raw binary natural-number payload · Exact-length runs of a TM2 machine

Proof usesA single step executes the statement at the current label

Used byLinear step bound for the payload normalizer machine · Number normalizer restores its work stacks and prepends its answer

TheoremLinear step bound for the payload normalizer machine#✓fully proved

The whole component runs in at most 2 |x| + 3 steps.

theorem run (x : List Bool) :
    ∃ v S, RunLe prog (2 * x.length + 3)
      ⟨some (.read none), false, st x [] []⟩
      ⟨some .done, v, S⟩ ∧ S .output = normalizeNat x

Uses 11 · Used by 1

Statement 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 · Normalization of a raw binary natural-number payload · Runs within a step budget

Proof usesRead phase of the payload normalizer consumes each bit once · Payload normalization adds at most one bit · Flag bit of a machine state · Exact-length runs of a TM2 machine · Running the bit-moving loop

Used byPayload normalization is polynomial-time

AbbreviationPayload normalizer as a host component#✓fully proved

The normalizer in the canonical component interface.

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

Uses 4 · Used by 1

Statement usesStacks of the payload normalizer machine · Control labels of the payload normalizer machine · Program of the payload normalizer machine · Component machine

Used byPayload normalization is polynomial-time

TheoremPayload normalization is polynomial-time#✓fully proved

Total binary-payload normalization is polynomial-time in the canonical encoded machine model.

theorem isPolyTime_normalizeNat :
    MetaMathlibExt.ComplexityTheory.IsPolyTime normalizeNat

Uses 19

Statement usesNormalization of a raw binary natural-number payload · 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 · Polynomial-time computable functions

Proof usesStacks of the payload normalizer machine · Control labels of the payload normalizer machine · Payload normalizer as a host component · Program of the payload normalizer machine · Linear step bound for the payload normalizer machine · Stack contents for the payload normalizer invariant · Component machine · Reduction host, canonical form · Runs within a step budget

8 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.