Reusable unary-count to canonical binary Nat conversion

InductiveControl labels of the unary-to-binary converter#✓fully proved

Existing emitter labels and the cleanup/unframing continuation.

inductive Lab | emit (l : EmitSS.Lab) | clean | read | back | done
  deriving DecidableEq

Uses 1 · Used by 6

Statement usesLabels of the subset-sum emitter

Used byUnary-to-binary converter as a host component · Label map from the emitter halt to scratch cleanup · Label enumeration of the unary-to-binary converter · Program of the unary-to-binary converter · Converter turns a unary count into a canonical binary frame · Converter turns a unary count into a raw canonical binary payload

DefinitionLabel enumeration of the unary-to-binary converter#✓fully proved

The finite label enumeration uses the existing emitter enumeration and two Boolean choices, without a noncomputable list conversion.

Cslib.Complexity.PolynomialEncoding.UnaryNat.labEquiv · 18 lines

def labEquiv : Lab ≃ EmitSS.Lab ⊕ Bool ⊕ Bool where
  toFun
    | .emit l => .inl l
    | .clean => .inr (.inl false)
    | .read => .inr (.inl true)
    | .back => .inr (.inr false)
    | .done => .inr (.inr true)
  invFun
    | .inl l => .emit l
    | .inr (.inl false) => .clean
    | .inr (.inl true) => .read
    | .inr (.inr false) => .back
    | .inr (.inr true) => .done
  left_inv l := by cases l <;> rfl
  right_inv l := by
    rcases l with l | b | b
    · rfl
    all_goals cases b <;> rfl

Uses 2 · Used by 1

Statement usesLabels of the subset-sum emitter · Control labels of the unary-to-binary converter

Used byUnary-to-binary converter as a host component

DefinitionEmitter stack embedding in the unary-to-binary converter#✓fully proved

The component retains the existing emitter's heterogeneous alphabets.

def embedding : SEmb EmitSS.Γ EmitSS.Γ :=
  ⟨id, injective_id, fun _ => Equiv.refl _⟩

Uses 3 · Used by 3

Statement usesStacks of the SUBSET-SUM reduction machine · Stack alphabets of the subset-sum emitter · Stack embedding

Used byProgram of the unary-to-binary converter · Converter turns a unary count into a canonical binary frame · Converter turns a unary count into a raw canonical binary payload

DefinitionLabel map from the emitter halt to scratch cleanup#✓fully proved

The actual emitter halt is followed by charged scratch cleanup.

def emitLabel (l : EmitSS.Lab) : Lab :=
  if l = .done then .clean else .emit l

Uses 2 · Used by 3

Statement usesLabels of the subset-sum emitter · Control labels of the unary-to-binary converter

Used byProgram of the unary-to-binary converter · Converter turns a unary count into a canonical binary frame · Converter turns a unary count into a raw canonical binary payload

DefinitionProgram of the unary-to-binary converter#✓fully proved

framed = true keeps the new frame; otherwise only that frame is removed, preserving any earlier output below it.

def prog (framed : Bool) : Lab → TM2.Stmt EmitSS.Γ Lab Bool
  | .emit l => mapS embedding emitLabel (EmitSS.prog l)
  | .clean => cleanS [.A, .H, .T] .clean (if framed then .done else .read)
  | .read => FramedCNF.Block.read .O .X some Sym.bit .read .back .done
  | .back => moveB .X .O Sym.bit? id .back .done
  | .done => .halt

Uses 14 · Used by 3

Statement usesMachine step reading one framed payload pair · Stacks of the SUBSET-SUM reduction machine · Labels of the subset-sum emitter · The subset-sum emitter machine · Stack alphabets of the subset-sum emitter · Control labels of the unary-to-binary converter · Emitter stack embedding in the unary-to-binary converter · Label map from the emitter halt to scratch cleanup · Stack alphabet of the SAT verifier · Reading a symbol as a name bit · Translating a statement along a stack embedding · Flag bit of a machine state · Cleanup round · Bit-moving loop

Used byUnary-to-binary converter as a host component · Converter turns a unary count into a canonical binary frame · Converter turns a unary count into a raw canonical binary payload

TheoremConverter turns a unary count into a canonical binary frame#✓fully proved

Emit one canonical Nat frame above any earlier output and restore all conversion scratch. The old counter is consumed; unrelated stacks, including X, are preserved. Cleanup is part of the charged run.

theorem run_framed (n : Nat) (out : List Bool) (v : Bool)
    (S : ∀ k, List (EmitSS.Γ k)) (hA : S .A = cnt EmitSS.U n)
    (hH : S .H = []) (hT : S .T = []) (hO : S .O = out) :
    ∃ U, RunLe (prog true) (708 * n + 304)
      ⟨some (.emit .hv), v, S⟩ ⟨some .done, false, U⟩ ∧
      U .O = delimit (Computability.encodeNat n) ++ out ∧
      U .A = [] ∧ U .H = [] ∧ U .T = [] ∧
      ∀ k, k ≠ .A → k ≠ .H → k ≠ .T → k ≠ .O → U k = S k

Uses 37

Statement usesStacks of the SUBSET-SUM reduction machine · Labels of the subset-sum emitter · Counter unit of the subset-sum emitter · Stack alphabets of the subset-sum emitter · Control labels of the unary-to-binary converter · Program of the unary-to-binary converter · Stack alphabet of the SAT verifier · Self-delimiting form of a bitstring · Runs within a step budget · Unary counter

Proof usesMachine step reading one framed payload pair · Binary code of the value of a bit list · Binary conversion (SUBSET-SUM reduction machine) · The subset-sum emitter machine · Run of the target-output phase of the subset-sum emitter · Emitter stack embedding in the unary-to-binary converter · Label map from the emitter halt to scratch cleanup · Reading a symbol as a name bit · Push bound of a finite multi-stack Turing machine · Number of push instructions in a TM2 statement · 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 · Cleanup round · Cleanup empties its stacks · Pushing a constant list · A halted run stays halted · Bit-moving loop · Pushing a list of symbols onto one stack · Value of a little-endian bit list · Binary encoding, least significant bit first

TheoremConverter turns a unary count into a raw canonical binary payload#✓fully proved

Convert a unary count to the canonical unframed Nat payload, preserving an earlier output suffix and clearing every used work stack.

theorem run_raw (n : Nat) (out : List Bool) (v : Bool)
    (S : ∀ k, List (EmitSS.Γ k)) (hA : S .A = cnt EmitSS.U n)
    (hH : S .H = []) (hT : S .T = []) (hO : S .O = out)
    (hX : S .X = []) :
    ∃ w U, RunLe (prog false) (710 * n + 306)
      ⟨some (.emit .hv), v, S⟩ ⟨some .done, w, U⟩ ∧
      U .O = Computability.encodeNat n ++ out ∧
      U .A = [] ∧ U .H = [] ∧ U .T = [] ∧ U .X = [] ∧
      ∀ k, k ≠ .A → k ≠ .H → k ≠ .T → k ≠ .O → k ≠ .X →
        U k = S k

Uses 39

Statement usesStacks of the SUBSET-SUM reduction machine · Labels of the subset-sum emitter · Counter unit of the subset-sum emitter · Stack alphabets of the subset-sum emitter · Control labels of the unary-to-binary converter · Program of the unary-to-binary converter · Stack alphabet of the SAT verifier · Runs within a step budget · Unary counter

Proof usesMachine step reading one framed payload pair · Reading a complete framed block · Binary code of the value of a bit list · Binary conversion (SUBSET-SUM reduction machine) · The subset-sum emitter machine · Run of the target-output phase of the subset-sum emitter · Emitter stack embedding in the unary-to-binary converter · Label map from the emitter halt to scratch cleanup · Reading a symbol as a name bit · Self-delimiting form of a bitstring · Push bound of a finite multi-stack Turing machine · Number of push instructions in a TM2 statement · 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 · Cleanup round · Cleanup empties its stacks · Pushing a constant list · A halted run stays halted · Bit-moving loop · Running the bit-moving loop · Pushing a list of symbols onto one stack · Value of a little-endian bit list · Binary encoding, least significant bit first

AbbreviationUnary-to-binary converter as a host component#✓fully proved

The adapter is a finite component of the existing Host. Its input counter has n physical symbols; the bound is linear in that length, not in the bit length of an arbitrary binary-encoded numeric input.

abbrev component (framed : Bool) : Host.Comp where
  K := EmitSS.K
  Γ := EmitSS.Γ
  finΓ k := by cases k <;> infer_instance
  L := Lab
  prog := prog framed
  ks := [.X, .O, .A, .H, .N, .M, .C, .S1, .S2, .Y, .Z, .T, .L, .R, .Rt]
  ks_nodup := by decide
  mem_ks k := by cases k <;> simp

Uses 8

Statement usesComponent machine · Stacks of the SUBSET-SUM reduction machine · Labels of the subset-sum emitter · Stack alphabets of the subset-sum emitter · Control labels of the unary-to-binary converter · Label enumeration of the unary-to-binary converter · Program of the unary-to-binary converter · Stack alphabet of the SAT verifier

8 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.