Documentation

Complexitylib.SAT.Tseitin.Machine.Internal.ValidationFramed

Framed execution of the Tseitin syntax validator #

The reduction front end invokes validationTM after seedFreshTM: the input and output heads are already parked at cell one, and the six work tapes contain initialized unary registers that must be preserved exactly. This module owns the canonical scan induction for that framed execution. From the started input, the validator consumes one input bit per step and one final step writes its Boolean verdict, for a total of |z| + 1 steps.

Main results #

Framed postcondition #

source
def Complexity.SAT.ThreeSAT.Machine.validationFramedPost {n : ℕ} (z : List Bool) (work₀ : Fin n → Tape) :
TapePred n

Tape-level result of validation with an arbitrary fixed work-register frame. The input has been scanned to its first trailing blank, the work tapes are unchanged, and the output contains exactly the Boolean validation verdict at cell one with a blank tail.

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

    One-step rules #

    Started scan #

    Exact started execution and Hoare interface #

    source
    theorem Complexity.SAT.ThreeSAT.Machine.validationTM_started_framed_reachesIn_internal {n : ℕ} (z : List Bool) (work₀ : Fin n → Tape) (out₀ : Tape) (hwork₀ : ∀ (i : Fin n), TM.Parked (work₀ i)) (hout₀ : TM.OutAcc [] out₀) :
    ∃ (c' : Cfg n validationTM.Q), validationTM.reachesIn (z.length + 1) { state := validationTM.qstart, input := { head := 1, cells := (Tape.init (List.map Γ.ofBool z)).cells }, work := work₀, output := out₀ } c' ∧ validationTM.halted c' ∧ validationFramedPost z work₀ c'.input c'.work c'.output

    Exact started, framed validation. From a started input and empty started output accumulator, validation reaches its framed postcondition in exactly |z| + 1 steps while preserving arbitrary parked work tapes.

    source
    theorem Complexity.SAT.ThreeSAT.Machine.validationTM_started_framed_hoareTime_internal {n : ℕ} (z : List Bool) (work₀ : Fin n → Tape) (hwork₀ : ∀ (i : Fin n), TM.Parked (work₀ i)) :
    validationTM.HoareTime (TM.EmitPred { head := 1, cells := (Tape.init (List.map Γ.ofBool z)).cells } work₀ []) (validationFramedPost z work₀) (z.length + 1)

    Started, framed validation. This is the interface needed directly after seedFreshTM: the input and output are parked at cell one, every work register is preserved exactly, and the verdict is produced in |z| + 1 steps.