Mixed-radix variable loading and literal emission

The Cook–Levin tableau's flat variable indices are mixed-radix numerals (((tag·A + a)·B + b)·C + c)·D + d. loadFlatVarTM computes one such index into the scratch register tmp by a setConstTM followed by four Horner layers, where each digit comes either from a register (a loop counter) or a hardwired constant, and each radix comes from a register. emitVarLitTM then appends the encoded literal for that variable to the output accumulator.

These two machines are the per-literal unit of every clause-family emitter: a clause is a bigSeqTM of emitVarLitTMs followed by the clause separator.

@[reducible, inline]

abbrev Complexity.TM.DigitSrc (n : ℕ) : Type

A digit source for the mixed-radix loader: a register index or a hardwired constant.

Equations

• Complexity.TM.DigitSrc n = (Fin n ⊕ ℕ)

def Complexity.TM.DigitSrcSpec {n : ℕ} (work₀ : Fin n → Tape) (tmp tmp2 : Fin n) : DigitSrc n → ℕ → Prop

The source s supplies the value w: either a register (disjoint from the scratches) currently holding w, or the constant w itself.

Equations

• Complexity.TM.DigitSrcSpec work₀ tmp tmp2 (Sum.inl r) x✝ = (work₀ r = Complexity.TM.regTape x✝ ∧ r ≠ tmp ∧ r ≠ tmp2)
• Complexity.TM.DigitSrcSpec work₀ tmp tmp2 (Sum.inr c) x✝ = (c = x✝)

def Complexity.TM.hornerStepTM {n : ℕ} (X tmp tmp2 : Fin n) : DigitSrc n → TM n

One mixed-radix step: tmp := tmp · X + (digit from s).

Equations

• Complexity.TM.hornerStepTM X tmp tmp2 (Sum.inl r) = Complexity.TM.hornerLayerRegTM X r tmp tmp2
• Complexity.TM.hornerStepTM X tmp tmp2 (Sum.inr c) = Complexity.TM.hornerLayerConstTM X tmp tmp2 c

theorem Complexity.TM.hornerStepTM_hoareTime {n : ℕ} {X tmp tmp2 : Fin n} (s : DigitSrc n) (hXt : X ≠ tmp) (hXt2 : X ≠ tmp2) (htt2 : tmp ≠ tmp2) (M x v w u : ℕ) (hx : x ≤ M) (hv : v ≤ M) (hu : u ≤ M) (hres : v * x + w ≤ M) (inp₀ : Tape) (work₀ : Fin n → Tape) (ys : List Bool) (hinp₀ : Parked inp₀) (hwork₀ : ∀ (i : Fin n), Parked (work₀ i)) (hX : work₀ X = regTape x) (hs : DigitSrcSpec work₀ tmp tmp2 s w) (ht : work₀ tmp = regTape v) (ht2 : work₀ tmp2 = regTape u) : (hornerStepTM X tmp tmp2 s).HoareTime (EmitPred inp₀ work₀ ys) (EmitPred inp₀ (Function.update (Function.update work₀ tmp2 (regTape (v * x + w))) tmp (regTape (v * x + w))) ys) (layerBudget M)

hornerStepTM Hoare specification (raw form, arbitrary scratch values).

def Complexity.TM.scratch {n : ℕ} (work₀ : Fin n → Tape) (tmp tmp2 : Fin n) (z : ℕ) : Fin n → Tape

The canonical scratch state after a mixed-radix stage: both scratches hold z, everything else is work₀.

Equations

• Complexity.TM.scratch work₀ tmp tmp2 z = Function.update (Function.update work₀ tmp2 (Complexity.TM.regTape z)) tmp (Complexity.TM.regTape z)

theorem Complexity.TM.scratch_parked {n : ℕ} {work₀ : Fin n → Tape} {tmp tmp2 : Fin n} (z : ℕ) (hwork₀ : ∀ (i : Fin n), Parked (work₀ i)) (i : Fin n) : Parked (scratch work₀ tmp tmp2 z i)

A scratch state built from a parked register family is parked on every tape.

theorem Complexity.TM.scratch_apply_ne {n : ℕ} {work₀ : Fin n → Tape} {tmp tmp2 : Fin n} {z : ℕ} {i : Fin n} (hit : i ≠ tmp) (hit2 : i ≠ tmp2) : scratch work₀ tmp tmp2 z i = work₀ i

scratch leaves every register other than the two scratches unchanged.

theorem Complexity.TM.scratch_apply_tmp {n : ℕ} {work₀ : Fin n → Tape} {tmp tmp2 : Fin n} {z : ℕ} : scratch work₀ tmp tmp2 z tmp = regTape z

In the scratch state at z, the register tmp holds z.

theorem Complexity.TM.scratch_apply_tmp2 {n : ℕ} {work₀ : Fin n → Tape} {tmp tmp2 : Fin n} {z : ℕ} (htt2 : tmp ≠ tmp2) : scratch work₀ tmp tmp2 z tmp2 = regTape z

In the scratch state at z, the register tmp2 holds z (when the scratches differ).

theorem Complexity.TM.parked_update {n : ℕ} {W : Fin n → Tape} (hW : ∀ (i : Fin n), Parked (W i)) {j : Fin n} {t : Tape} (ht : Parked t) (i : Fin n) : Parked (Function.update W j t i)

Updating a parked family with a parked tape stays parked.

theorem Complexity.TM.scratch_update_comm {n : ℕ} {work₀ : Fin n → Tape} {tmp tmp2 i : Fin n} (hit : i ≠ tmp) (hit2 : i ≠ tmp2) (z : ℕ) (t : Tape) : Function.update (scratch work₀ tmp tmp2 z) i t = scratch (Function.update work₀ i t) tmp tmp2 z

Updates at other registers slide past the scratch pair.

theorem Complexity.TM.scratch_idem {n : ℕ} {work₀ : Fin n → Tape} {tmp tmp2 : Fin n} (htt2 : tmp ≠ tmp2) (z z' : ℕ) : scratch (scratch work₀ tmp tmp2 z) tmp tmp2 z' = scratch work₀ tmp tmp2 z'

Scratching twice keeps only the second value.

theorem Complexity.TM.DigitSrcSpec.scratch {n : ℕ} {work₀ : Fin n → Tape} {tmp tmp2 : Fin n} {s : DigitSrc n} {w : ℕ} (hs : DigitSrcSpec work₀ tmp tmp2 s w) (z : ℕ) : DigitSrcSpec (TM.scratch work₀ tmp tmp2 z) tmp tmp2 s w

Source specifications survive scratching (sources avoid the scratches).

theorem Complexity.TM.hornerStepTM_hoareTime_scratch {n : ℕ} (X tmp tmp2 : Fin n) (s : DigitSrc n) (hXt : X ≠ tmp) (hXt2 : X ≠ tmp2) (htt2 : tmp ≠ tmp2) (M x v w : ℕ) (hx : x ≤ M) (hv : v ≤ M) (hres : v * x + w ≤ M) (inp₀ : Tape) (work₀ : Fin n → Tape) (ys : List Bool) (hinp₀ : Parked inp₀) (hwork₀ : ∀ (i : Fin n), Parked (work₀ i)) (hX : work₀ X = regTape x) (hs : DigitSrcSpec work₀ tmp tmp2 s w) : (hornerStepTM X tmp tmp2 s).HoareTime (EmitPred inp₀ (scratch work₀ tmp tmp2 v) ys) (EmitPred inp₀ (scratch work₀ tmp tmp2 (v * x + w)) ys) (layerBudget M)

hornerStepTM on canonical scratch states. The composable form: scratches at v in, scratches at v·x + w out.

def Complexity.TM.loadFlatVarTM {n : ℕ} (rA rB rC rD tmp tmp2 : Fin n) (tag : ℕ) (sa sb sc sd : DigitSrc n) : TM n

Load the mixed-radix numeral (((tag·A + a)·B + b)·C + c)·D + d into tmp (and tmp2), with radices read from registers rA rB rC rD and digits from the sources sa sb sc sd.

Equations

• One or more equations did not get rendered due to their size.

def Complexity.TM.loadBudget (M : ℕ) : ℕ

Time budget of loadFlatVarTM.

Equations

• Complexity.TM.loadBudget M = Complexity.TM.opBudget M + 4 * Complexity.TM.layerBudget M + 4

theorem Complexity.TM.loadFlatVarTM_hoareTime {n : ℕ} (rA rB rC rD tmp tmp2 : Fin n) (tag : ℕ) (sa sb sc sd : DigitSrc n) (hAt : rA ≠ tmp) (hAt2 : rA ≠ tmp2) (hBt : rB ≠ tmp) (hBt2 : rB ≠ tmp2) (hCt : rC ≠ tmp) (hCt2 : rC ≠ tmp2) (hDt : rD ≠ tmp) (hDt2 : rD ≠ tmp2) (htt2 : tmp ≠ tmp2) (M A B C D a b c d v u : ℕ) (hA : A ≤ M) (hB : B ≤ M) (hC : C ≤ M) (hD : D ≤ M) (htag : tag ≤ M) (hv : v ≤ M) (hu : u ≤ M) (h1 : tag * A + a ≤ M) (h2 : (tag * A + a) * B + b ≤ M) (h3 : ((tag * A + a) * B + b) * C + c ≤ M) (h4 : (((tag * A + a) * B + b) * C + c) * D + d ≤ M) (inp₀ : Tape) (work₀ : Fin n → Tape) (ys : List Bool) (hinp₀ : Parked inp₀) (hwork₀ : ∀ (i : Fin n), Parked (work₀ i)) (hrA : work₀ rA = regTape A) (hrB : work₀ rB = regTape B) (hrC : work₀ rC = regTape C) (hrD : work₀ rD = regTape D) (hsa : DigitSrcSpec work₀ tmp tmp2 sa a) (hsb : DigitSrcSpec work₀ tmp tmp2 sb b) (hsc : DigitSrcSpec work₀ tmp tmp2 sc c) (hsd : DigitSrcSpec work₀ tmp tmp2 sd d) (ht : work₀ tmp = regTape v) (ht2 : work₀ tmp2 = regTape u) : (loadFlatVarTM rA rB rC rD tmp tmp2 tag sa sb sc sd).HoareTime (EmitPred inp₀ work₀ ys) (EmitPred inp₀ (scratch work₀ tmp tmp2 ((((tag * A + a) * B + b) * C + c) * D + d)) ys) (loadBudget M)

loadFlatVarTM Hoare specification. All four radices from registers, all intermediate numeral values capped by M; ends on the canonical scratch state at the full numeral.

def Complexity.TM.emitVarLitTM {n : ℕ} (rA rB rC rD tmp tmp2 : Fin n) (sign : Bool) (tag : ℕ) (sa sb sc sd : DigitSrc n) : TM n

Emit one literal: load the mixed-radix variable index into tmp, then append the encoded literal with sign sign to the output.

Equations

• Complexity.TM.emitVarLitTM rA rB rC rD tmp tmp2 sign tag sa sb sc sd = (Complexity.TM.loadFlatVarTM rA rB rC rD tmp tmp2 tag sa sb sc sd).seqTM (Complexity.TM.emitLitTM sign tmp)

def Complexity.TM.emitVarBudget (M : ℕ) : ℕ

Time budget of emitVarLitTM.

Equations

• Complexity.TM.emitVarBudget M = Complexity.TM.loadBudget M + Complexity.TM.opBudget M + 1

theorem Complexity.TM.emitVarLitTM_hoareTime {n : ℕ} (rA rB rC rD tmp tmp2 : Fin n) (sign : Bool) (tag : ℕ) (sa sb sc sd : DigitSrc n) (hAt : rA ≠ tmp) (hAt2 : rA ≠ tmp2) (hBt : rB ≠ tmp) (hBt2 : rB ≠ tmp2) (hCt : rC ≠ tmp) (hCt2 : rC ≠ tmp2) (hDt : rD ≠ tmp) (hDt2 : rD ≠ tmp2) (htt2 : tmp ≠ tmp2) (M A B C D a b c d v u : ℕ) (hA : A ≤ M) (hB : B ≤ M) (hC : C ≤ M) (hD : D ≤ M) (htag : tag ≤ M) (hv : v ≤ M) (hu : u ≤ M) (h1 : tag * A + a ≤ M) (h2 : (tag * A + a) * B + b ≤ M) (h3 : ((tag * A + a) * B + b) * C + c ≤ M) (h4 : (((tag * A + a) * B + b) * C + c) * D + d ≤ M) (inp₀ : Tape) (work₀ : Fin n → Tape) (ys : List Bool) (hinp₀ : Parked inp₀) (hwork₀ : ∀ (i : Fin n), Parked (work₀ i)) (hrA : work₀ rA = regTape A) (hrB : work₀ rB = regTape B) (hrC : work₀ rC = regTape C) (hrD : work₀ rD = regTape D) (hsa : DigitSrcSpec work₀ tmp tmp2 sa a) (hsb : DigitSrcSpec work₀ tmp tmp2 sb b) (hsc : DigitSrcSpec work₀ tmp tmp2 sc c) (hsd : DigitSrcSpec work₀ tmp tmp2 sd d) (ht : work₀ tmp = regTape v) (ht2 : work₀ tmp2 = regTape u) : (emitVarLitTM rA rB rC rD tmp tmp2 sign tag sa sb sc sd).HoareTime (EmitPred inp₀ work₀ ys) (EmitPred inp₀ (scratch work₀ tmp tmp2 ((((tag * A + a) * B + b) * C + c) * D + d)) (ys ++ ([sign, sign] ++ List.replicate (2 * ((((tag * A + a) * B + b) * C + c) * D + d)) true ++ [false, true]))) (emitVarBudget M)

emitVarLitTM Hoare specification. Appends [sign, sign] ++ 2·var trues ++ [false, true] for the mixed-radix variable index var, leaving the scratches at var and everything else untouched.

theorem Complexity.TM.emitVarLitTM_hoareTime_scratch {n : ℕ} (rA rB rC rD tmp tmp2 : Fin n) (sign : Bool) (tag : ℕ) (sa sb sc sd : DigitSrc n) (hAt : rA ≠ tmp) (hAt2 : rA ≠ tmp2) (hBt : rB ≠ tmp) (hBt2 : rB ≠ tmp2) (hCt : rC ≠ tmp) (hCt2 : rC ≠ tmp2) (hDt : rD ≠ tmp) (hDt2 : rD ≠ tmp2) (htt2 : tmp ≠ tmp2) (M A B C D a b c d z : ℕ) (hA : A ≤ M) (hB : B ≤ M) (hC : C ≤ M) (hD : D ≤ M) (htag : tag ≤ M) (hz : z ≤ M) (h1 : tag * A + a ≤ M) (h2 : (tag * A + a) * B + b ≤ M) (h3 : ((tag * A + a) * B + b) * C + c ≤ M) (h4 : (((tag * A + a) * B + b) * C + c) * D + d ≤ M) (inp₀ : Tape) (work₀ : Fin n → Tape) (ys : List Bool) (hinp₀ : Parked inp₀) (hwork₀ : ∀ (i : Fin n), Parked (work₀ i)) (hrA : work₀ rA = regTape A) (hrB : work₀ rB = regTape B) (hrC : work₀ rC = regTape C) (hrD : work₀ rD = regTape D) (hsa : DigitSrcSpec work₀ tmp tmp2 sa a) (hsb : DigitSrcSpec work₀ tmp tmp2 sb b) (hsc : DigitSrcSpec work₀ tmp tmp2 sc c) (hsd : DigitSrcSpec work₀ tmp tmp2 sd d) : (emitVarLitTM rA rB rC rD tmp tmp2 sign tag sa sb sc sd).HoareTime (EmitPred inp₀ (scratch work₀ tmp tmp2 z) ys) (EmitPred inp₀ (scratch work₀ tmp tmp2 ((((tag * A + a) * B + b) * C + c) * D + d)) (ys ++ ([sign, sign] ++ List.replicate (2 * ((((tag * A + a) * B + b) * C + c) * D + d)) true ++ [false, true]))) (emitVarBudget M)

emitVarLitTM on canonical scratch states — the composable form used by the clause emitters: scratches at any z ≤ M in, scratches at the emitted variable out.

def Complexity.TM.resetScratchTM {n : ℕ} (tmp tmp2 : Fin n) : TM n

Zero both scratch registers (the fixed point of every clause emitter).

Equations

• Complexity.TM.resetScratchTM tmp tmp2 = (Complexity.TM.setConstTM tmp 0).seqTM (Complexity.TM.setConstTM tmp2 0)

theorem Complexity.TM.resetScratchTM_hoareTime {n : ℕ} (tmp tmp2 : Fin n) (htt2 : tmp ≠ tmp2) (M z : ℕ) (hz : z ≤ M) (inp₀ : Tape) (work₀ : Fin n → Tape) (ys : List Bool) (hinp₀ : Parked inp₀) (hwork₀ : ∀ (i : Fin n), Parked (work₀ i)) : (resetScratchTM tmp tmp2).HoareTime (EmitPred inp₀ (scratch work₀ tmp tmp2 z) ys) (EmitPred inp₀ (scratch work₀ tmp tmp2 0) ys) (2 * opBudget M + 1)

resetScratchTM Hoare specification: canonical scratches at z to canonical scratches at 0.