tmp

Author: chung-thai-nguyen

ArkLib/OracleReduction/Completeness.lean

@@ -626,7 +626,6 @@ theorem unroll_n_message_reduction_perfectCompleteness
 
 end GenericProtocol
 
-
 section OneMessageProtocol
 
 variable {oSpec : OracleSpec ι} [oSpec.FiniteRange] {StmtIn WitIn StmtOut WitOut : Type}

ArkLib/OracleReduction/OracleInterface.lean

@@ -207,6 +207,40 @@ def simOracle2 {ι : Type u} (oSpec : OracleSpec ι)
       | .inl i => answer (t₁ i)
       | .inr i => answer (t₂ i))
 
+/-- simOracle never fails because it is a deterministic transcript lookup. -/
+theorem neverFails_simOracle {ι : Type u} (oSpec : OracleSpec ι)
+    {ι' : Type v} {T : ι' → Type w} [∀ i, OracleInterface (T i)]
+    (t : ∀ i, T i) :
+    ∀ {β} (q : (oSpec ++ₒ [T]ₒ).OracleQuery β),
+    ((simOracle oSpec t).impl q).neverFails := by
+  intro β q
+  unfold simOracle
+  dsimp [SimOracle.append, fnOracle, idOracle]
+  cases q with
+  | query i t' =>
+    cases i with
+    | inl i => exact OracleComp.neverFails_query _
+    | inr i => exact OracleComp.neverFails_pure _
+
+/-- simOracle2 never fails because it is a deterministic transcript lookup. -/
+theorem neverFails_simOracle2 {ι : Type u} (oSpec : OracleSpec ι)
+    {ι₁ : Type v} {T₁ : ι₁ → Type w} [∀ i, OracleInterface (T₁ i)]
+    {ι₂ : Type v} {T₂ : ι₂ → Type w} [∀ i, OracleInterface (T₂ i)]
+    (t₁ : ∀ i, T₁ i) (t₂ : ∀ i, T₂ i) :
+    ∀ {β} (q : (oSpec ++ₒ ([T₁]ₒ ++ₒ [T₂]ₒ)).OracleQuery β),
+    ((simOracle2 oSpec t₁ t₂).impl q).neverFails := by
+  intro β q
+  unfold simOracle2
+  dsimp [SimOracle.append, fnOracle, idOracle]
+  cases q with
+  | query i t =>
+    cases i with
+    | inl i => exact OracleComp.neverFails_query _
+    | inr i =>
+      cases i with
+      | inl i => exact OracleComp.neverFails_pure _
+      | inr i => exact OracleComp.neverFails_pure _
+
 open Finset in
 /-- A message type together with a `OracleInterface` instance is said to have **oracle distance**
   (at most) `d` if for any two distinct messages, there is at most `d` queries that distinguish

ArkLib/ProofSystem/Binius/BinaryBasefold/Basic.lean

@@ -355,9 +355,9 @@ def mkLastOracleIndex (i : Fin (ℓ + 1)) : Fin (toOutCodewordsCount ℓ ϑ i) :
     ⟩
 
 lemma mkLastOracleIndex_last : mkLastOracleIndex ℓ ϑ (Fin.last ℓ) = ℓ / ϑ - 1 := by
-  dsimp only [mkLastOracleIndex, Fin.val_last, lt_self_iff_false, Lean.Elab.WF.paramLet,
-    eq_mpr_eq_cast, cast_eq]
+  dsimp only [mkLastOracleIndex, Fin.val_last, lt_self_iff_false, Lean.Elab.WF.paramLet]
   simp only [lt_self_iff_false, ↓reduceDIte]
+  rfl
 
 end OracleStatementIndex
 
@@ -773,7 +773,6 @@ lemma take_snoc_oracle_eq_oStmtIn (i : Fin ℓ)
     (newOracleFn : OracleFunction 𝔽q β (h_ℓ_add_R_rate := h_ℓ_add_R_rate) i.succ) :
     (take_snoc_oracle 𝔽q β i oStmtIn newOracleFn) = oStmtIn := by
   unfold take_snoc_oracle snoc_oracle
-  simp only [eq_mpr_eq_cast, id_eq]
   if hi: isCommitmentRound ℓ ϑ i then
     simp only [Fin.is_lt, ↓reduceDIte, Fin.eta]
   else
@@ -1047,9 +1046,9 @@ lemma oracleWitnessConsistency_relay_preserved
     (stmt : Statement (L := L) Context i.succ)
     (wit : Witness (L := L) 𝔽q β (h_ℓ_add_R_rate := h_ℓ_add_R_rate) i.succ)
     (oStmt : ∀ j, OracleStatement 𝔽q β (h_ℓ_add_R_rate := h_ℓ_add_R_rate) ϑ i.castSucc j) :
-    oracleWitnessConsistency (mp := mp) (𝓑 := 𝓑) 𝔽q β i.succ i.castSucc
+    oracleWitnessConsistency (mp := mp) 𝔽q β i.succ i.castSucc
       (le_succ ↑i.castSucc) stmt wit oStmt =
-    oracleWitnessConsistency (mp := mp) (𝓑 := 𝓑) 𝔽q β i.succ i.succ (by rfl) stmt wit
+    oracleWitnessConsistency (mp := mp) 𝔽q β i.succ i.succ (by rfl) stmt wit
       (mapOStmtOutRelayStep 𝔽q β i hNCR oStmt) := by
   unfold oracleWitnessConsistency
   -- All four components (witnessStructuralInvariant, sumCheckConsistency,
@@ -1109,13 +1108,12 @@ def masterKStateProp (stmtIdx : Fin (ℓ + 1))
     (wit : Witness (L := L) 𝔽q β (h_ℓ_add_R_rate := h_ℓ_add_R_rate) stmtIdx)
     (oStmt : ∀ j, (OracleStatement 𝔽q β (h_ℓ_add_R_rate := h_ℓ_add_R_rate) ϑ (i := oracleIdx) j))
     (localChecks : Prop := True) : Prop :=
-  let oracleWitnessConsistency: Prop := oracleWitnessConsistency (mp := mp) (𝓑 := 𝓑) 𝔽q β
+  let oracleWitnessConsistency: Prop := oracleWitnessConsistency (mp := mp) 𝔽q β
     stmtIdx oracleIdx h_le stmt wit oStmt
   let badEventExists := badEventExistsProp (ϑ := ϑ) 𝔽q β oracleIdx
     (challenges := Fin.take (m := oracleIdx) (v := stmt.challenges) (h := by omega))
     (oStmt := oStmt)
-  let sumCheckConsistency: Prop := sumcheckConsistencyProp (𝓑 := 𝓑) stmt.sumcheck_target wit.H
-  localChecks ∧ sumCheckConsistency ∧ (badEventExists ∨ oracleWitnessConsistency)
+  localChecks ∧ (badEventExists ∨ oracleWitnessConsistency)
 
 def roundRelationProp (i : Fin (ℓ + 1))
     (input : (Statement (L := L) Context i ×
@@ -1124,8 +1122,10 @@ def roundRelationProp (i : Fin (ℓ + 1))
   let stmt := input.1.1
   let oStmt := input.1.2
   let wit := input.2
-  masterKStateProp (mp := mp) (𝓑 := 𝓑) 𝔽q β
-    (stmtIdx := i) (oracleIdx := i) (h_le := le_refl i) stmt wit oStmt (localChecks := True)
+  let sumCheckConsistency: Prop := sumcheckConsistencyProp (𝓑 := 𝓑) stmt.sumcheck_target wit.H
+  masterKStateProp 𝔽q β (mp := mp)
+    (stmtIdx := i) (oracleIdx := i) (h_le := le_refl i) stmt wit oStmt
+    (localChecks := sumCheckConsistency)
 
 /-- A modified version of roundRelationProp (i+1) -/
 def foldStepRelOutProp (i : Fin ℓ)
@@ -1135,12 +1135,15 @@ def foldStepRelOutProp (i : Fin ℓ)
   let stmt := input.1.1
   let oStmt := input.1.2
   let wit := input.2
-  masterKStateProp (mp := mp) (𝓑 := 𝓑) 𝔽q β
+  let sumCheckConsistency: Prop := sumcheckConsistencyProp (𝓑 := 𝓑) stmt.sumcheck_target wit.H
+  masterKStateProp 𝔽q β (mp := mp)
     (stmtIdx := i.succ) (oracleIdx := i.castSucc)
-    (h_le := Nat.le_of_lt (Fin.castSucc_lt_succ i)) stmt wit oStmt (localChecks := True)
+    (h_le := Nat.le_of_lt (Fin.castSucc_lt_succ i)) stmt wit oStmt
+      (localChecks := sumCheckConsistency)
 
 /-- This is a special case of nonDoomedFoldingProp for `i = ℓ`, where we support
-the consistency between the last oracle `ℓ - ϑ` and the final constant `c` -/
+the consistency between the last oracle `ℓ - ϑ` and the final constant `c`.
+This definition has form similar to masterKState where there is no localChecks. -/
 def finalNonDoomedFoldingProp {h_le : ϑ ≤ ℓ}
     (input : (FinalSumcheckStatementOut (L := L) (ℓ := ℓ) ×
       (∀ j, OracleStatement 𝔽q β (h_ℓ_add_R_rate := h_ℓ_add_R_rate) ϑ (Fin.last ℓ) j))) :
@@ -1152,8 +1155,8 @@ def finalNonDoomedFoldingProp {h_le : ϑ ≤ ℓ}
   let k := j.val * ϑ
   have h_k: k = ℓ - ϑ := by
     dsimp only [mkLastOracleIndex, Fin.val_last, lt_self_iff_false, Lean.Elab.WF.paramLet,
-      eq_mpr_eq_cast, cast_eq, k, j]
-    simp only [lt_self_iff_false, ↓reduceDIte]
+      k, j]
+    simp only [lt_self_iff_false, ↓reduceDIte, eq_mpr_eq_cast, cast_eq]
     rw [Nat.sub_mul, Nat.one_mul]
     rw [Nat.div_mul_cancel (hdiv.out)]
   let f_k := oStmt j
@@ -1193,7 +1196,7 @@ def foldStepRelOut (i : Fin ℓ) :
     Set ((Statement (L := L) Context i.succ ×
       (∀ j, OracleStatement 𝔽q β (h_ℓ_add_R_rate := h_ℓ_add_R_rate) ϑ i.castSucc j)) ×
       Witness (L := L) 𝔽q β (h_ℓ_add_R_rate := h_ℓ_add_R_rate) i.succ) :=
-  { input | foldStepRelOutProp (mp := mp) (𝓑 := 𝓑) 𝔽q β i input}
+  { input | foldStepRelOutProp 𝔽q β (𝓑 := 𝓑) (mp := mp) i input}
 
 /-- Relation at step `i` of the CoreInteraction. `∀ i < ℓ, R_i` must hold at the
 beginning of ITERATION `i`. `R_ℓ` must hold after the last iteration and before sending
@@ -1202,7 +1205,7 @@ def roundRelation (i : Fin (ℓ + 1)) :
     Set ((Statement (L := L) Context i ×
       (∀ j, OracleStatement 𝔽q β (h_ℓ_add_R_rate := h_ℓ_add_R_rate) ϑ i j)) ×
       Witness (L := L) 𝔽q β (h_ℓ_add_R_rate := h_ℓ_add_R_rate) i) :=
-  { input | roundRelationProp (mp := mp) (𝓑 := 𝓑) 𝔽q β i input}
+  { input | roundRelationProp 𝔽q β (𝓑 := 𝓑) (mp := mp) i input}
 
 /-- Relation for final sumcheck step -/
 def finalSumcheckRelOutProp

ArkLib/ProofSystem/Binius/BinaryBasefold/Steps.lean

@@ -200,7 +200,7 @@ For fold step: sumcheck condition must hold. -/
 def foldVerifierCheck (i : Fin ℓ)
     (stmtIn : Statement (L := L) Context i.castSucc)
     (msg0 : Message (pSpecFold (L := L)) ⟨0, rfl⟩) : Prop :=
-  msg0.val.eval 0 + msg0.val.eval 1 = stmtIn.sumcheck_target
+  msg0.val.eval (𝓑 0) + msg0.val.eval (𝓑 1) = stmtIn.sumcheck_target
 
 /-- Pure verifier output computation extracted from foldOracleVerifier.verify (lines 180-184).
 What verifier returns after checks pass. -/
@@ -240,7 +240,7 @@ def foldStepLogic (i : Fin ℓ) :
 
   -- 2. Verifier Logic (Using extracted kernels)
   verifierCheck := fun s t =>
-    foldVerifierCheck i s (t.messages ⟨0, rfl⟩)
+    foldVerifierCheck i s (𝓑 := 𝓑) (t.messages ⟨0, rfl⟩)
 
   verifierOut := fun s t =>
     foldVerifierStmtOut i s (t ⟨0, by omega⟩) (t ⟨1, by omega⟩)
@@ -490,7 +490,7 @@ lemma foldStep_is_logic_complete (i : Fin ℓ) :
       -- verifierStmtOut.sumcheck_target = msg0.val.eval chal1 (by definition of foldVerifierStmtOut)
       -- proverWitOut.H = projectToNextSumcheckPoly witIn.H chal1 (by definition of getFoldProverFinalOutput)
       unfold sumcheckConsistencyProp
-      rw [verifierStmtOut, proverWitOut, proverOutput]
+      dsimp only [verifierStmtOut, proverWitOut, proverOutput]
       simp only [step, foldStepLogic, foldVerifierStmtOut, getFoldProverFinalOutput, transcript]
       -- Now we need: msg0.val.eval chal1 = ∑ x, projectedH.val.eval x
       -- This follows from projectToNextSumcheckPoly_sum_eq

ArkLib/ToVCVio/Execution.lean

@@ -12,6 +12,7 @@ import VCVio.OracleComp.SimSemantics.SimulateQ
 import Mathlib.Data.ENNReal.Basic
 import VCVio.OracleComp.DistSemantics.EvalDist
 import ArkLib.OracleReduction.OracleInterface
+import ArkLib.ToVCVio.StateTLemmas
 
 /-!
 ## Monad-to-Logic Bridge Lemmas

ArkLib/ToVCVio/StateTLemmas.lean

@@ -0,0 +1,44 @@
+/-
+Copyright (c) 2025 ArkLib Contributors. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: ArkLib Contributors
+-/
+
+import VCVio.OracleComp.OracleComp
+
+/-!
+# StateT Helper Lemmas
+
+This file contains simple helper lemmas for `StateT` operations that simplify
+reasoning about `run`, `run'`, and monadic operations in the probability monad.
+
+These lemmas are used throughout the execution semantics to unfold stateful
+computations into their underlying probability distributions.
+-/
+
+universe u v w
+
+namespace StateT
+
+variable {m : Type u → Type v} {σ α β : Type u}
+
+/-- Unfolding lemma for `run'` on `pure`. -/
+@[simp]
+theorem run'_pure_lib [Monad m] [LawfulMonad m] (x : α) (s : σ) :
+    (pure x : StateT σ m α).run' s = (pure x : m α) := by
+  simp only [run', pure, StateT.pure, map_pure]
+
+/-- Unfolding lemma for `run'` on `bind`. -/
+@[simp]
+theorem run'_bind_lib [Monad m] [LawfulMonad m] (ma : StateT σ m α) (f : α → StateT σ m β) (s : σ) :
+    (ma >>= f).run' s = ((ma.run s) >>= fun (a, s') => (f a).run' s') := by
+  simp only [run', bind, StateT.bind, map_bind, run]
+
+/-- Unfolding lemma for `run` on `liftM`. -/
+@[simp]
+theorem run_liftM_lib [Monad m] [LawfulMonad m] (ma : m α) (s : σ) :
+    (liftM ma : StateT σ m α).run s = (ma >>= fun a => pure (a, s)) := by
+  simp only [run, liftM, bind_pure_comp]
+  rw [map_eq_pure_bind]; rfl
+
+end StateT