Verified structured RAM exact-3-CNF syntax scanner #
The generic typed-scanner compiler supplies the entire implementation proof and
resource analysis for the existing 27-state SAT.ThreeSAT.Syntax automaton.
theorem
Complexity.RAM.Structured.ThreeSATSyntax.program_performance
(bits : List Bool)
:
∃ (final : Store) (cost : ℕ) (space : ℕ),
Exec program (inputStore bits) final (stepCount bits.length) cost space ∧ cost ≤ timeBound bits.length ∧ space ≤ spaceBound bits.length ∧ final verdictReg = Input.bitValue
(SAT.ThreeSAT.Syntax.accept (List.foldl SAT.ThreeSAT.Syntax.bitStep SAT.ThreeSAT.Syntax.bitStart bits))
Source correctness and explicit resource bounds for syntax recognition.
theorem
Complexity.RAM.Structured.ThreeSATSyntax.compiled_performance
(bits : List Bool)
:
∃ (final : Store) (cost : ℕ) (space : ℕ),
Exec program (inputStore bits) final (stepCount bits.length) cost space ∧ run compiled (stepCount bits.length) { pc := 0, regs := inputStore bits } = { pc := program.codeSize, regs := final } ∧ Halted compiled (run compiled (stepCount bits.length) { pc := 0, regs := inputStore bits }) ∧ logTimeUpto compiled (stepCount bits.length) { pc := 0, regs := inputStore bits } ≤ timeBound bits.length ∧ spaceUpto compiled (stepCount bits.length) { pc := 0, regs := inputStore bits } ≤ spaceBound bits.length ∧ ((run compiled (stepCount bits.length) { pc := 0, regs := inputStore bits }).regs verdictReg = 1 ↔ bits ∈ SAT.ThreeSAT.Syntax.language)
End-to-end compiled performance and syntax-language correctness.
The explicit logarithmic-time budget is quasilinear.
The explicit peak-space budget is quasilinear.