Hoare specification for the Tseitin reduction front end

reductionFrontEndTM first initializes the fresh-variable register to one more than the source bit length and then validates the source encoding. This module composes the two framed contracts. The sequence boundary is an exact no-op on the parked input, unary registers, and empty output accumulator.

The resulting postcondition records all state needed by the branch assembly:

• the input head is on the first trailing blank at |z| + 1;
• freshReg contains |z| + 1 and every other work register is zero;
• all work registers are preserved by validation; and
• output cell one contains validEncoding z, with the output head at one and a blank tail.

Main results

• reductionFrontEndTM_hoareTime_internal -- structural bound 5|z| + 13
• reductionFrontEndTM_linear_hoareTime_internal -- rounded bound 13(|z| + 1)

def Complexity.SAT.ThreeSAT.Machine.frontEndWork (z : List Bool) : Fin workTapeCount → Tape

Work-register family established by seedFreshTM: the fresh register contains the source bit length plus one and the remaining five registers are zero.

Equations

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

theorem Complexity.SAT.ThreeSAT.Machine.frontEndWork_parked (z : List Bool) (i : Fin workTapeCount) : TM.Parked (frontEndWork z i)

Every initialized front-end register is parked.

theorem Complexity.SAT.ThreeSAT.Machine.reductionFrontEndTime_le_linear_internal (n : ℕ) : 5 * n + 13 ≤ 13 * (n + 1)

The structural front-end budget is bounded by a convenient linear polynomial with one coefficient.

theorem Complexity.SAT.ThreeSAT.Machine.reductionFrontEndTM_hoareTime_internal (z : List Bool) : reductionFrontEndTM.HoareTime (fun (inp : Tape) (work : Fin workTapeCount → Tape) (out : Tape) => inp = Tape.init (List.map Γ.ofBool z) ∧ (∀ (i : Fin workTapeCount), work i = Tape.init []) ∧ out = Tape.init []) (validationFramedPost z (frontEndWork z)) (5 * z.length + 13)

Framed front-end execution. Starting from the ordinary initial tape layout, initialize all six registers and validate z. Validation preserves the initialized register family exactly and leaves its Boolean verdict at output cell one.

theorem Complexity.SAT.ThreeSAT.Machine.reductionFrontEndTM_linear_hoareTime_internal (z : List Bool) : reductionFrontEndTM.HoareTime (fun (inp : Tape) (work : Fin workTapeCount → Tape) (out : Tape) => inp = Tape.init (List.map Γ.ofBool z) ∧ (∀ (i : Fin workTapeCount), work i = Tape.init []) ∧ out = Tape.init []) (validationFramedPost z (frontEndWork z)) (13 * (z.length + 1))

Rounded linear-time form of the front-end contract, ready for later polynomial assembly.