Documentation

Complexitylib.SAT.Verifier

SAT verifier specification #

This file defines an executable verifier for pairLang Witness:

  1. split pair(z, α) back into (z, α) via unpair?,
  2. decode z as a CNF in SAT's concrete bit encoding,
  3. check the witness length bound |α| ≤ |z| + 1,
  4. evaluate the decoded formula under α.

The deterministic implementation verifyPairTM in SAT/VerifierTM.lean computes this specification and proves pairLang Witness ∈ P; this file is the small executable/semantic audit surface for that machine proof.

source
inductive Complexity.SAT.EncToken :
Type

The four two-bit tokens used by SAT's concrete encoding.

  • bit (b : Bool) : EncToken

    A doubled data bit: false is encoded as 00, true as 11.

  • litSep : EncToken

    The literal separator |, encoded as 01.

  • clauseSep : EncToken

    The clause separator #, encoded as 10.

Instances For
    source
    def Complexity.SAT.instDecidableEqEncToken.decEq (x✝ x✝¹ : EncToken) :
    Decidable (x✝ = x✝¹)
    Equations
    Instances For
      source
      @[implicit_reducible]
      instance Complexity.SAT.instDecidableEqEncToken :
      DecidableEq EncToken
      Equations
      source
      @[implicit_reducible]
      instance Complexity.SAT.instReprEncToken :
      Repr EncToken
      Equations
      source
      def Complexity.SAT.instReprEncToken.repr :
      EncToken → ℕ → Std.Format
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        def Complexity.SAT.EncToken.encode :
        EncToken → List Bool

        Concrete two-bit representation of one SAT encoding token.

        Equations
        Instances For
          source
          def Complexity.SAT.encodeTokens (toks : List EncToken) :
          List Bool

          Flatten a token stream back into concrete bits.

          Equations
          Instances For
            source
            def Complexity.SAT.tokenize? :
            List Bool → Option (List EncToken)

            Split a bitstring into SAT encoding tokens. Odd-length strings are invalid.

            Equations
            Instances For
              source
              @[simp]
              theorem Complexity.SAT.encodeTokens_nil :
              encodeTokens [] = []

              The empty token stream encodes to the empty bitstring.

              source
              @[simp]
              theorem Complexity.SAT.encodeTokens_cons (tok : EncToken) (toks : List EncToken) :
              encodeTokens (tok :: toks) = tok.encode ++ encodeTokens toks

              encodeTokens unfolds on cons: the head token's bits precede the tail's encoding.

              source
              @[simp]
              theorem Complexity.SAT.encodeTokens_append (xs ys : List EncToken) :
              encodeTokens (xs ++ ys) = encodeTokens xs ++ encodeTokens ys

              encodeTokens is a monoid homomorphism: it distributes over list append.

              source
              @[simp]
              theorem Complexity.SAT.tokenize?_encodeTokens (toks : List EncToken) :
              tokenize? (encodeTokens toks) = some toks

              Round trip: tokenizing an encoded token stream recovers the original tokens.

              source
              theorem Complexity.SAT.tokenize?_sound {z : List Bool} {toks : List EncToken} (h : tokenize? z = some toks) :
              z = encodeTokens toks

              Soundness of tokenize?: any successfully tokenized bitstring is the encoding of the resulting token stream.

              source
              theorem Complexity.SAT.tokenize?_sound.hsound (z : List Bool) (toks : List EncToken) :
              tokenize? z = some toks → z = encodeTokens toks
              source
              @[simp]
              theorem Complexity.SAT.encodeTokens_map_bit (bs : List Bool) :
              encodeTokens (List.map EncToken.bit bs) = doubleBits bs

              Encoding a stream of bit tokens doubles each underlying bit.

              source
              def Complexity.SAT.Lit.decodeRaw? :
              List Bool → Option Lit

              Decode a raw literal bitstring [sign] ++ replicate var true.

              Equations
              Instances For
                source
                @[simp]
                theorem Complexity.SAT.Lit.decodeRaw?_encodeRaw (ℓ : Lit) :
                decodeRaw? ℓ.encodeRaw = some ℓ

                Round trip: decoding a literal's raw encoding recovers the literal.

                source
                theorem Complexity.SAT.Lit.decodeRaw?_sound {bs : List Bool} {ℓ : Lit} (h : decodeRaw? bs = some ℓ) :
                bs = ℓ.encodeRaw

                Soundness of decodeRaw?: any successfully decoded bitstring is the raw encoding of the resulting literal.

                source
                def Complexity.SAT.Lit.rawTokens (ℓ : Lit) :
                List EncToken

                Token-level raw literal encoding.

                Equations
                Instances For
                  source
                  @[simp]
                  theorem Complexity.SAT.Lit.encodeTokens_rawTokens (ℓ : Lit) :
                  encodeTokens ℓ.rawTokens = doubleBits ℓ.encodeRaw

                  A literal's token-level encoding flattens to its raw bits, doubled.

                  source
                  def Complexity.SAT.Clause.tokens :
                  Clause → List EncToken

                  Token-level clause encoding: doubled raw literal bits, each terminated by |.

                  Equations
                  Instances For
                    source
                    @[simp]
                    theorem Complexity.SAT.Clause.encodeTokens_tokens (c : Clause) :
                    encodeTokens c.tokens = c.encode

                    A clause's token-level encoding flattens to its concrete bit encoding.

                    source
                    @[simp]
                    theorem Complexity.SAT.Clause.tokens_append (c₁ c₂ : Clause) :
                    (c₁ ++ c₂).tokens = c₁.tokens ++ c₂.tokens

                    Clause.tokens distributes over list append.

                    source
                    def Complexity.SAT.CNF.tokens :
                    CNF → List EncToken

                    Token-level CNF encoding: each clause is terminated by #.

                    Equations
                    Instances For
                      source
                      @[simp]
                      theorem Complexity.SAT.CNF.encodeTokens_tokens (φ : CNF) :
                      encodeTokens φ.tokens = φ.encode

                      A CNF's token-level encoding flattens to its concrete bit encoding.

                      source
                      @[simp]
                      theorem Complexity.SAT.CNF.tokens_append (φ ψ : CNF) :
                      (φ ++ ψ).tokens = φ.tokens ++ ψ.tokens

                      CNF.tokens distributes over list append.

                      source
                      def Complexity.SAT.parseTokensAux :
                      List EncToken → List Bool → Clause → CNF → Option CNF

                      Core parser state: rawRev is the reversed current raw literal, clauseRev the reversed current clause, and cnfRev the reversed list of completed clauses.

                      Equations
                      Instances For
                        source
                        def Complexity.SAT.CNF.decode? (z : List Bool) :
                        Option CNF

                        Decode a concrete SAT-encoded bitstring as a CNF.

                        Equations
                        Instances For
                          source
                          @[simp]
                          theorem Complexity.SAT.CNF.decode?_encode (φ : CNF) :
                          decode? φ.encode = some φ

                          Round trip: decoding an encoded CNF recovers the formula.

                          source
                          theorem Complexity.SAT.CNF.decode?_sound {z : List Bool} {φ : CNF} (h : decode? z = some φ) :
                          z = φ.encode

                          Soundness of CNF.decode?: any successfully decoded bitstring is the encoding of the resulting CNF.

                          source
                          def Complexity.SAT.verifyPair (w : List Bool) :
                          Bool

                          Boolean verifier for SAT's witness relation on paired inputs.

                          Equations
                          • One or more equations did not get rendered due to their size.
                          Instances For
                            source
                            @[simp]
                            theorem Complexity.SAT.verifyPair_pair_encode (φ : CNF) (α : Assignment) :
                            verifyPair (pair φ.encode α) = (decide (List.length α ≤ φ.encode.length + 1) && CNF.eval α φ)

                            On a well-formed pair pair(φ.encode, α), verifyPair reduces to the witness length check conjoined with evaluating φ under α.

                            source
                            theorem Complexity.SAT.verifyPair_true_of_witness {z α : List Bool} (hR : Witness z α) :
                            verifyPair (pair z α) = true

                            Completeness: verifyPair accepts the pairing of any witnessed instance.

                            source
                            theorem Complexity.SAT.verifyPair_eq_true_iff_mem_pairLang (w : List Bool) :
                            verifyPair w = true ↔ w ∈ pairLang Witness

                            Correctness of the verifier: verifyPair accepts exactly the members of pairLang Witness.

                            source
                            theorem Complexity.SAT.mem_pairLang_iff_verifyPair (w : List Bool) :
                            w ∈ pairLang Witness ↔ verifyPair w = true

                            verifyPair_eq_true_iff_mem_pairLang with the biconditional flipped.

                            source
                            theorem Complexity.SAT.pairLang_witness_eq_verifyPairLang :
                            pairLang Witness = {w : List Bool | verifyPair w = true}

                            pairLang Witness equals the language decided by verifyPair, as sets.