FinalCorrectness.lean

/-
This is the final correctenss theorem, stated in terms of the autogenerated constraints.

The statements of theorems only depend on the data and constraints specified in
`constraints_autogenerated.lean` and the machine semantics in `cpu.lean`.
-/
import Verification.Semantics.AirEncoding.Correctness
import Verification.Semantics.AirEncoding.Glue

noncomputable section

open scoped Classical BigOperators

variable {F : Type} [Field F] [Fintype F]

/-
These are the constraints that the verifier has to check against the public data.
-/
structure PublicConstraints (inp : InputData F) (pd : PublicData F) : Prop where
  h_mem_star :
    let z := pd.memoryMultiColumnPermPermInteractionElm
    let alpha := pd.memoryMultiColumnPermHashInteractionElm0
    let p := pd.memoryMultiColumnPermPermPublicMemoryProd
    let dom_m_star := { x // Option.isSome (inp.mStar x) }
    (p * ∏ a : dom_m_star, (z - (a.val + alpha * memVal a))) = z ^ Fintype.card dom_m_star
  h_card_dom : 8 * Fintype.card { x // Option.isSome (inp.mStar x) } + 2 ≤ inp.traceLength
  public_memory_prod_eq_one : pd.rc16PermPublicMemoryProd = 1
  rcMax_lt : pd.rcMax < 2 ^ 16
  rcMin_le : pd.rcMin ≤ pd.rcMax
  traceLength_le_char : inp.traceLength ≤ ringChar F

/-
The main correctness theorem.
-/
theorem final_correctness (char_ge : ringChar F ≥ 2 ^ 63)
    -- public data
    (inp : InputData F)
    (pd : PublicData F) (pc : PublicConstraints inp pd)
    (c : Columns F) :
    -- sets to avoid
    ∃ bad1 bad2 bad3 : Finset F,
      bad1.card ≤ (inp.traceLength / 2) ^ 2 ∧
        bad2.card ≤ inp.traceLength / 2 ∧
          bad3.card ≤ inp.traceLength ∧
            -- autogenerated constraints
            ∀ ci : ColumnsInter F,
            -- probabilistic constraints
              CpuDecode c ∧ CpuOperands c ∧ CpuUpdateRegisters inp c ∧
              CpuOpcodes c ∧ Memory inp pd c ci ∧ Rc16 inp pd c ci ∧
              PublicMemory c ∧ RcBuiltin inp pd c ∧ ToplevelConstraints inp c ∧
              pd.memoryMultiColumnPermHashInteractionElm0 ∉ bad1 ∧
              pd.memoryMultiColumnPermPermInteractionElm ∉ bad2 ∧
              pd.memoryMultiColumnPermPermInteractionElm ≠ 0 ∧
              pd.rc16PermInteractionElm ∉ bad3 →
              -- number of execution steps
                let T := inp.traceLength / 16 - 1
              -- memory elements checked by range check builtin
                let rc_len := inp.traceLength / 128
                -- the conclusion
                ∃ mem : F → F,
                  Option.FnExtends mem inp.mStar ∧
                    (∀ i < rc_len, ∃ (n : ℕ), n < 2 ^ 128 ∧ mem (pd.initialRcAddr + i) = ↑n) ∧
                      ∃ exec : Fin (T + 1) → RegisterState F,
                        (exec 0).pc = inp.initialPc ∧
                          (exec 0).ap = inp.initialAp ∧
                            (exec 0).fp = inp.initialAp ∧
                              (exec (Fin.last T)).pc = inp.finalPc ∧
                                (exec (Fin.last T)).ap = inp.finalAp ∧
                                  ∀ i : Fin T, NextState mem (exec i.castSucc) (exec i.succ) := by
  use bad1 pc.h_card_dom c.column19 c.column20
  use bad2 pd pc.h_card_dom c.column19 c.column20
  use bad3 inp c.column0 c.column2
  use bad1_bound pc.h_card_dom _ _
  use bad2_bound pd pc.h_card_dom _ _
  use bad3_bound pc.h_card_dom _ _
  intro ci
  rintro ⟨cd, ops, upd, opcodes, m, rc, pm, rcb, iandf, prob1, prob2, prob3, prob4⟩
  dsimp
  exact
    execution_exists char_ge (inp.toInputDataAux pd pc.rcMax_lt pc.rcMin_le)
      (toConstraints cd ops upd opcodes m rc pm rcb iandf pc.h_mem_star pc.h_card_dom
        pc.public_memory_prod_eq_one pc.rcMax_lt pc.rcMin_le pc.traceLength_le_char)
      { hprob₁ := prob1
        hprob₂ := prob2
        hprob₃ := prob3
        hprob₄ := prob4 }