Sound checking of the RUP fragment of LRAT certificates

rupCheck checks reverse unit propagation along supplied clause indices. checkStepsWith checks a sequence of such additions and requires an empty clause. unsat_of_checkSteps proves that acceptance implies unsatisfiability of the input CNF. External solvers supply certificates; their correctness is unnecessary for this theorem.

ClauseDB abstracts lookup, append and initialization together with the membership laws consumed by soundness. Both the array and balanced-tree implementations prove those laws. The theorem covers RUP additions, not general RAT additions. Concrete certificate data and upstream performance experiments are outside this import.

@[reducible, inline]

abbrev QECCertificates.LRAT.Lit : Type

A zero-based variable index and its polarity.

Equations

• QECCertificates.LRAT.Lit = (ℕ × Bool)

@[reducible, inline]

abbrev QECCertificates.LRAT.Clause : Type

A disjunction of literals.

Equations

• QECCertificates.LRAT.Clause = List QECCertificates.LRAT.Lit

@[reducible, inline]

abbrev QECCertificates.LRAT.CNF : Type

A conjunction of clauses.

Equations

• QECCertificates.LRAT.CNF = List QECCertificates.LRAT.Clause

@[reducible, inline]

abbrev QECCertificates.LRAT.Assign : Type

A total Boolean assignment.

Equations

• QECCertificates.LRAT.Assign = (ℕ → Bool)

@[reducible, inline]

abbrev QECCertificates.LRAT.PAssign : Type

Literals asserted true by a partial assignment.

Equations

• QECCertificates.LRAT.PAssign = List QECCertificates.LRAT.Lit

def QECCertificates.LRAT.litNeg (l : Lit) : Lit

Negation changes only the polarity.

Equations

• QECCertificates.LRAT.litNeg l = (l.fst, !l.snd)

def QECCertificates.LRAT.SatClause (σ : Assign) (C : Clause) : Prop

A clause is satisfied by an assignment.

Equations

• QECCertificates.LRAT.SatClause σ C = ∃ (l : QECCertificates.LRAT.Lit), l ∈ C ∧ σ l.fst = l.snd

def QECCertificates.LRAT.SatFormula (σ : Assign) (F : CNF) : Prop

A CNF is satisfied by an assignment.

Equations

• QECCertificates.LRAT.SatFormula σ F = ∀ (C : QECCertificates.LRAT.Clause), C ∈ F → QECCertificates.LRAT.SatClause σ C

def QECCertificates.LRAT.Satisfiable (F : CNF) : Prop

The CNF is satisfiable.

Equations

• QECCertificates.LRAT.Satisfiable F = ∃ (σ : QECCertificates.LRAT.Assign), QECCertificates.LRAT.SatFormula σ F

def QECCertificates.LRAT.agrees (σ : Assign) (a : PAssign) : Prop

The partial assignment a agrees with the total assignment σ.

Equations

• QECCertificates.LRAT.agrees σ a = ∀ (l : QECCertificates.LRAT.Lit), l ∈ a → σ l.fst = l.snd

def QECCertificates.LRAT.litFree (a : PAssign) (l : Lit) : Bool

The literal is not known false: its negation is absent from the partial assignment.

Equations

• QECCertificates.LRAT.litFree a l = !decide (QECCertificates.LRAT.litNeg l ∈ a)

1. Scanning a clause

def QECCertificates.LRAT.scanAux (a : PAssign) (fr : List Lit) : Clause → List Lit

Collect literals not known false, accumulating them in reverse order.

Equations

• QECCertificates.LRAT.scanAux a fr [] = fr
• QECCertificates.LRAT.scanAux a fr (l :: rest) = if QECCertificates.LRAT.litFree a l = true then QECCertificates.LRAT.scanAux a (l :: fr) rest else QECCertificates.LRAT.scanAux a fr rest

def QECCertificates.LRAT.scan (a : PAssign) (D : Clause) : List Lit

Scan a clause: return the list of its literals not known false under the current assignment. Emptiness means "all false", a conflict, and a singleton means "exactly one free literal", a unit step.

Equations

• QECCertificates.LRAT.scan a D = QECCertificates.LRAT.scanAux a [] D

theorem QECCertificates.LRAT.scanAux_spec (a : PAssign) (D : Clause) (fr : List Lit) : ∃ (tail : List Lit), scanAux a fr D = tail ++ fr ∧ (∀ (l : Lit), l ∈ tail → l ∈ D ∧ litFree a l = true) ∧ ∀ (l : Lit), l ∈ D → litFree a l = true → l ∈ tail

theorem QECCertificates.LRAT.scan_nil {a : PAssign} {D : Clause} (h : scan a D = []) (l : Lit) : l ∈ D → litFree a l = false

scan a D = [] implies that every literal of D is false under the current assignment.

theorem QECCertificates.LRAT.scan_singleton {a : PAssign} {D : Clause} {l : Lit} (h : scan a D = [l]) : l ∈ D ∧ ∀ (l' : Lit), l' ∈ D → l' ≠ l → litFree a l' = false

scan a D = [l] implies that l ∈ D and that every other literal of D is false.

theorem QECCertificates.LRAT.litFree_eq_false {a : PAssign} {l : Lit} (h : litFree a l = false) {σ : Assign} (hσ : agrees σ a) : σ l.fst = !l.snd

If a literal is not free under the current assignment, then its negation has been assigned.

2. The clause database interface

Kernel replay uses only four operations of the database, namely lookup, length, append and build, and three laws. Changing the representation, from Array to a balanced tree, is therefore an instantiation, not a re-proof of a load-bearing module.

The representation matters for kernel reduction: array accesses and appends can repeatedly traverse prior entries, whereas balanced trees avoid that pattern. Both implementations below satisfy the same soundness interface. Concrete replay datasets and upstream benchmarks are outside this import.

structure QECCertificates.LRAT.ClauseDB (Carrier : Type) : Type

The clause database interface: rupCheck and checkAux use only these four operations and three laws.

• get? : Carrier → ℕ → Option Clause

  Look up a clause at a zero-based index.

• size : Carrier → ℕ

  The index at which the next clause is appended.

• push : Carrier → Clause → Carrier

  Append a clause to the database.

• Mem : Carrier → Clause → Prop

  Semantic membership of a clause in the database.

• get?_mem {d : Carrier} {i : ℕ} {C : Clause} : self.get? d i = some C → self.Mem d C

  A clause that is looked up is certainly in the database.

• push_mem {d : Carrier} {C C' : Clause} : self.Mem (self.push d C) C' → C' = C ∨ self.Mem d C'

  After one append, every clause in the database is either the new one or was already there. Only the half that soundness needs is required: checkAux_sound consumes this direction only, while the missing converse, C' = C ∨ Mem d C' → Mem (push d C) C', is exactly where a balanced-tree instance needs the invariant "key < size". Stating the laws at the strength that is used keeps both instances clean.

• ofCNF : CNF → Carrier

  Build a database from a CNF.

• ofCNF_mem {F : CNF} {C : Clause} : self.Mem (self.ofCNF F) C → C ∈ F

  Every clause of the initial database comes from that CNF, again only the half that is used.

def QECCertificates.LRAT.ClauseDB.array : ClauseDB (Array Clause)

The clause database represented by an array.

Equations

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

def QECCertificates.LRAT.ClauseDB.treeMem (d : Std.TreeMap ℕ Clause compare) (C : Clause) : Prop

Membership for the tree database: C is the value at some key.

Factored out into a separate def: writing Mem inside the structure literal would resolve to the structure projection ClauseDB.Mem, which takes the structure itself as its first argument, so Mem d C would expect a ClauseDB as its first argument.

Equations

• QECCertificates.LRAT.ClauseDB.treeMem d C = ∃ (i : ℕ), d.get? i = some C

def QECCertificates.LRAT.ClauseDB.tree : ClauseDB (Std.TreeMap ℕ Clause compare)

The balanced-tree version: each lookup and insertion is $O(\log n)$ in the kernel, so the whole certificate accumulates logarithmically rather than quadratically as with Array. The key is the clause number minus one, 0-based, and push appends at size.

Equations

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

def QECCertificates.LRAT.rupAux {K : Type} (D : ClauseDB K) (d : K) (a : PAssign) : List ℕ → Bool

Unit propagation along the hint sequence. h is a 1-based clause number.

Equations

• One or more equations did not get rendered due to their size.
• QECCertificates.LRAT.rupAux D d a [] = false

def QECCertificates.LRAT.rupCheck {K : Type} (D : ClauseDB K) (d : K) (C : Clause) (hints : List ℕ) : Bool

The clause C is RUP with respect to the database d: negating C and propagating along hints reaches a conflict.

Equations

• QECCertificates.LRAT.rupCheck D d C hints = QECCertificates.LRAT.rupAux D d (List.map QECCertificates.LRAT.litNeg C) hints

theorem QECCertificates.LRAT.rupAux_sound {K : Type} (D : ClauseDB K) {σ : Assign} {d : K} (hints : List ℕ) (a : PAssign) : agrees σ a → (∀ (h : ℕ), h ∈ hints → ∀ (E : Clause), D.get? d (h - 1) = some E → SatClause σ E) → rupAux D d a hints = true → False

Soundness of RUP: if propagation along the hints reaches a conflict, then any assignment satisfying the clauses the hints point to satisfies C.

3. The certificate checking layer

structure QECCertificates.LRAT.LStep : Type

One LRAT step: id is the clause number given by LRAT, the original clauses being 1..m and the lemmas running consecutively from m+1.

• id : ℕ

  One-based number of the added clause.

• clause : Clause

  The clause justified by this step.

• hints : List ℕ

  One-based indices to follow during reverse unit propagation.

def QECCertificates.LRAT.checkAux {K : Type} (D : ClauseDB K) (d : K) : List LStep → Bool

Step-by-step checking: the clause numbers must be consecutive, namely D.size d + 1, and each clause must be RUP; deriving the empty clause means success.

Equations

• One or more equations did not get rendered due to their size.
• QECCertificates.LRAT.checkAux D d [] = false

def QECCertificates.LRAT.checkStepsWith {K : Type} (D : ClauseDB K) (F : CNF) (steps : List LStep) : Bool

Checking with a given representation: build the database from the CNF via D.ofCNF, then check the steps one by one.

Equations

• QECCertificates.LRAT.checkStepsWith D F steps = QECCertificates.LRAT.checkAux D (D.ofCNF F) steps

@[reducible, inline]

abbrev QECCertificates.LRAT.checkSteps (F : CNF) (steps : List LStep) : Bool

The entry point, with the verbatim signature from before the interface was opened: it uses the Array database, so the two downstream data modules are unaffected.

Equations

• QECCertificates.LRAT.checkSteps F steps = QECCertificates.LRAT.checkStepsWith QECCertificates.LRAT.ClauseDB.array F steps

theorem QECCertificates.LRAT.checkAux_sound {K : Type} (D : ClauseDB K) {σ : Assign} (d : K) (steps : List LStep) : (∀ (C : Clause), D.Mem d C → SatClause σ C) → checkAux D d steps = true → False

Soundness of the checker (the core): if checkAux returns true, then σ does not satisfy the database.

theorem QECCertificates.LRAT.checkSteps_sound {F : CNF} {steps : List LStep} (h : checkSteps F steps = true) : ¬Satisfiable F

The main theorem, entry point: a successful kernel check implies that the CNF is unsatisfiable.

theorem QECCertificates.LRAT.unsat_of_checkSteps {F : CNF} {steps : List LStep} (h : checkSteps F steps = true) : ¬Satisfiable F

The entry point used by the generator: the same content as checkSteps_sound, as a proof term.