refinement.lean

-- Distributed under MIT License available at https://github.com/Verified-zkEVM/clean/blob/883ac93d22397edbdef3876623749e73425d571a/LICENSE
-- Copyright (c) 2025 zkSecurity, LLC

namespace High

  axiom ProverInput : Type
  axiom Witness : Type

  axiom compute : ProverInput → Option Witness

  -- None = UB
  -- Some true = satisfied
  -- Some false = unsatisfied
  axiom constrain : Witness → Option Bool

  axiom proverAssumption : ProverInput → Prop
  axiom completeness :
    ∀ input : ProverInput,
    proverAssumption input →
    ∃ w : Witness, compute input = some w ∧
      constrain w = some true

  axiom verifierAssumption : Witness → Prop
  axiom spec : Witness → Prop
  axiom soundness :
    ∀ w : Witness,
    verifierAssumption w →
    constrain w = some true →
    spec w

end High

namespace Low

  axiom ProverInput : Type
  axiom Witness : Type

  axiom compute : ProverInput → Option Witness

  -- None = UB
  -- Some true = satisfied
  -- Some false = unsatisfied
  axiom constrain : Witness → Option Bool

end Low

namespace Refinement

  axiom proverInputRel : High.ProverInput → Low.ProverInput → Prop
  axiom witnessRel : High.Witness → Low.Witness → Prop

  axiom constrainRelComplete : ∀ (witnessLow : Low.Witness) (witnessHigh : High.Witness) inputHigh,
    /- additional assumptions available in Lean -/
    High.proverAssumption inputHigh →
    High.compute inputHigh = some witnessHigh →
    /- usual things follow below -/
    Refinement.witnessRel witnessHigh witnessLow →
    High.constrain witnessHigh = some true →
    Low.constrain witnessLow = some true

  axiom constrainRelSound : ∀ (witnessLow : Low.Witness) (witnessHigh : High.Witness),
    /- additional assumption available in Lean -/
    High.verifierAssumption witnessHigh →
    /- usual things follow below -/
    Refinement.witnessRel witnessHigh witnessLow →
    Low.constrain witnessLow = some true → -- Low is implying high
    High.constrain witnessHigh = some true

  axiom computeRel : ∀ (inputLow : Low.ProverInput) (inputHigh : High.ProverInput),
    Refinement.proverInputRel inputHigh inputLow →
    ∀ witnessHigh, High.compute inputHigh = some witnessHigh →
    ∃ witnessLow, Low.compute inputLow = some witnessLow ∧
      Refinement.witnessRel witnessHigh witnessLow

  -- If Clean is used as backend, low must imply high for compute

end Refinement

namespace Low
  def proverAssumption (input : ProverInput) :=
    ∃ inputHigh, Refinement.proverInputRel inputHigh input ∧
      High.proverAssumption inputHigh
  def verifierAssumption (w : Witness) :=
    ∃ witnessHigh, Refinement.witnessRel witnessHigh w ∧
      High.verifierAssumption witnessHigh
  def spec (w : Witness) :=
    ∃ witnessHigh, Refinement.witnessRel witnessHigh w ∧
      High.spec witnessHigh
end Low

theorem completeness :
    ∀ input : Low.ProverInput,
    Low.proverAssumption input →
    ∃ w : Low.Witness, Low.compute input = some w ∧
      Low.constrain w = some true := by
  intro inputLow inputLow_h
  obtain ⟨ inputHigh, input_rel, inputHigh_h ⟩ := inputLow_h
  obtain ⟨ witnessHigh, high_compute, high_constrain ⟩ := High.completeness inputHigh inputHigh_h
  obtain ⟨ witnessLow, witnessLow_h ⟩ := Refinement.computeRel inputLow inputHigh input_rel witnessHigh high_compute
  exists witnessLow
  and_intros
  · simp_all
  apply Refinement.constrainRelComplete witnessLow witnessHigh inputHigh <;> simp_all

theorem soundness :
    ∀ w : Low.Witness,
    Low.verifierAssumption w →
    Low.constrain w = some true →
    Low.spec w := by
  intros w w_h w_c
  obtain ⟨ witnessHigh, w_rel, high_assumptino ⟩ := w_h
  unfold Low.spec
  exists witnessHigh
  and_intros
  · assumption
  apply High.soundness
  · assumption
  apply Refinement.constrainRelSound <;> assumption