Skip to content

feat: Update to 4.26 and fix breaking changes in VCV #286

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
dtumad wants to merge 3 commits into
base: main
Choose a base branch
from
Open

feat: Update to 4.26 and fix breaking changes in VCV #286

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
ac7ba3f
merge recent main
dtumad Jan 7, 2026
73305b9
Main 4-26 update and VCV breaking changes
dtumad Jan 7, 2026
f04465d
4.26 update and VCV breaking changes
dtumad Jan 7, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
70 changes: 35 additions & 35 deletions ArkLib.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -123,18 +123,18 @@ import ArkLib.OracleReduction.Composition.Sequential.Append
import ArkLib.OracleReduction.Composition.Sequential.General
import ArkLib.OracleReduction.Equiv
import ArkLib.OracleReduction.Execution
import ArkLib.OracleReduction.FiatShamir.Basic
import ArkLib.OracleReduction.FiatShamir.DuplexSponge.Defs
import ArkLib.OracleReduction.FiatShamir.DuplexSponge.Security.AbortAnalysis
import ArkLib.OracleReduction.FiatShamir.DuplexSponge.Security.Backtrack
import ArkLib.OracleReduction.FiatShamir.DuplexSponge.Security.BadEvents
import ArkLib.OracleReduction.FiatShamir.DuplexSponge.Security.Completeness
import ArkLib.OracleReduction.FiatShamir.DuplexSponge.Security.KeyLemma
import ArkLib.OracleReduction.FiatShamir.DuplexSponge.Security.Lookahead
import ArkLib.OracleReduction.FiatShamir.DuplexSponge.Security.ProverTransform
import ArkLib.OracleReduction.FiatShamir.DuplexSponge.Security.Soundness
import ArkLib.OracleReduction.FiatShamir.DuplexSponge.Security.TraceTransform
import ArkLib.OracleReduction.FiatShamir.DuplexSponge.State
-- import ArkLib.OracleReduction.FiatShamir.Basic
-- import ArkLib.OracleReduction.FiatShamir.DuplexSponge.Defs
-- import ArkLib.OracleReduction.FiatShamir.DuplexSponge.Security.AbortAnalysis
-- import ArkLib.OracleReduction.FiatShamir.DuplexSponge.Security.Backtrack
-- import ArkLib.OracleReduction.FiatShamir.DuplexSponge.Security.BadEvents
-- import ArkLib.OracleReduction.FiatShamir.DuplexSponge.Security.Completeness
-- import ArkLib.OracleReduction.FiatShamir.DuplexSponge.Security.KeyLemma
-- import ArkLib.OracleReduction.FiatShamir.DuplexSponge.Security.Lookahead
-- import ArkLib.OracleReduction.FiatShamir.DuplexSponge.Security.ProverTransform
-- import ArkLib.OracleReduction.FiatShamir.DuplexSponge.Security.Soundness
-- import ArkLib.OracleReduction.FiatShamir.DuplexSponge.Security.TraceTransform
-- import ArkLib.OracleReduction.FiatShamir.DuplexSponge.State
import ArkLib.OracleReduction.LiftContext.Lens
import ArkLib.OracleReduction.LiftContext.OracleReduction
import ArkLib.OracleReduction.LiftContext.Reduction
Expand All @@ -145,29 +145,29 @@ import ArkLib.OracleReduction.ProtocolSpec.Cast
import ArkLib.OracleReduction.ProtocolSpec.SeqCompose
import ArkLib.OracleReduction.Salt
import ArkLib.OracleReduction.Security.Basic
import ArkLib.OracleReduction.Security.Implications
import ArkLib.OracleReduction.Security.Rewinding
-- import ArkLib.OracleReduction.Security.Implications
-- import ArkLib.OracleReduction.Security.Rewinding
import ArkLib.OracleReduction.Security.RoundByRound
import ArkLib.OracleReduction.Security.SpecialSoundness
import ArkLib.OracleReduction.Security.StateRestoration
-- import ArkLib.OracleReduction.Security.SpecialSoundness
-- import ArkLib.OracleReduction.Security.StateRestoration
import ArkLib.OracleReduction.VectorIOR
import ArkLib.ProofSystem.BatchedFri.Spec.General
import ArkLib.ProofSystem.BatchedFri.Spec.SingleRound
import ArkLib.ProofSystem.Binius.BinaryBasefold.Basic
import ArkLib.ProofSystem.Binius.BinaryBasefold.CoreInteractionPhase
import ArkLib.ProofSystem.Binius.BinaryBasefold.General
import ArkLib.ProofSystem.Binius.BinaryBasefold.Prelude
import ArkLib.ProofSystem.Binius.BinaryBasefold.QueryPhase
import ArkLib.ProofSystem.Binius.BinaryBasefold.Spec
import ArkLib.ProofSystem.Binius.BinaryBasefold.Steps
import ArkLib.ProofSystem.Binius.FRIBinius.CoreInteractionPhase
import ArkLib.ProofSystem.Binius.FRIBinius.General
import ArkLib.ProofSystem.Binius.FRIBinius.Prelude
import ArkLib.ProofSystem.Binius.RingSwitching.BatchingPhase
import ArkLib.ProofSystem.Binius.RingSwitching.General
import ArkLib.ProofSystem.Binius.RingSwitching.Prelude
import ArkLib.ProofSystem.Binius.RingSwitching.Spec
import ArkLib.ProofSystem.Binius.RingSwitching.SumcheckPhase
-- import ArkLib.ProofSystem.BatchedFri.Spec.General
-- import ArkLib.ProofSystem.BatchedFri.Spec.SingleRound
-- import ArkLib.ProofSystem.Binius.BinaryBasefold.Basic
-- import ArkLib.ProofSystem.Binius.BinaryBasefold.CoreInteractionPhase
-- import ArkLib.ProofSystem.Binius.BinaryBasefold.General
-- import ArkLib.ProofSystem.Binius.BinaryBasefold.Prelude
-- import ArkLib.ProofSystem.Binius.BinaryBasefold.QueryPhase
-- import ArkLib.ProofSystem.Binius.BinaryBasefold.Spec
-- import ArkLib.ProofSystem.Binius.BinaryBasefold.Steps
-- import ArkLib.ProofSystem.Binius.FRIBinius.CoreInteractionPhase
-- import ArkLib.ProofSystem.Binius.FRIBinius.General
-- import ArkLib.ProofSystem.Binius.FRIBinius.Prelude
-- import ArkLib.ProofSystem.Binius.RingSwitching.BatchingPhase
-- import ArkLib.ProofSystem.Binius.RingSwitching.General
-- import ArkLib.ProofSystem.Binius.RingSwitching.Prelude
-- import ArkLib.ProofSystem.Binius.RingSwitching.Spec
-- import ArkLib.ProofSystem.Binius.RingSwitching.SumcheckPhase
import ArkLib.ProofSystem.Component.CheckClaim
import ArkLib.ProofSystem.Component.DoNothing
import ArkLib.ProofSystem.Component.NoInteraction
Expand All @@ -182,8 +182,8 @@ import ArkLib.ProofSystem.ConstraintSystem.R1CS
import ArkLib.ProofSystem.DSL
import ArkLib.ProofSystem.Fri.Domain
import ArkLib.ProofSystem.Fri.RoundConsistency
import ArkLib.ProofSystem.Fri.Spec.General
import ArkLib.ProofSystem.Fri.Spec.SingleRound
-- import ArkLib.ProofSystem.Fri.Spec.General
-- import ArkLib.ProofSystem.Fri.Spec.SingleRound
import ArkLib.ProofSystem.Plonk.Basic
import ArkLib.ProofSystem.Spartan.Basic
import ArkLib.ProofSystem.Stir
Expand Down
34 changes: 17 additions & 17 deletions ArkLib/AGM/Basic.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -49,31 +49,31 @@ variable (ι : Type) (p : ℕ)
/-- The group operation oracle allows an adversary to perform the group operation on group elements
stored at the indices `i` and `j` (if they are both defined), storing the result at index `k`. -/
@[reducible]
def GroupOpOracle : OracleSpec Unit := fun _ => (ι × ι × ι, Unit)
def GroupOpOracle : OracleSpec (ι × ι × ι) := fun _ => Unit

/-- The group exponent oracle allows an adversary to compute the group element at the index `i`
raised to the power `a`, storing the result at index `j`.

Technically, this oracle can be implemented with just the group operation oracle, but we allow
this for faster implementation. -/
@[reducible]
def GroupExpOracle : OracleSpec Unit := fun _ => (ι × ZMod p × ι, Unit)
def GroupExpOracle : OracleSpec (ι × ZMod p × ι) := fun _ => Unit

/-- The group equality oracle allows an adversary to check if the group elements stored at the
indices `i` and `j` are equal. -/
@[reducible]
def GroupEqOracle : OracleSpec Unit := fun _ => (ι × ι, Bool)
def GroupEqOracle : OracleSpec (ι × ι) := fun _ => Bool

variable (bitLength : ℕ)

/-- The group encoding oracle allows an adversary to get the bit encoding of a group element. -/
@[reducible]
def GroupEncodeOracle : OracleSpec Unit := fun _ => (ι, BitVec bitLength)
def GroupEncodeOracle : OracleSpec ι := fun _ => BitVec bitLength

/-- The group decoding oracle allows an adversary to insert a group element corresponding to a
bit encoding into the table, if the bit encoding is valid. -/
@[reducible]
def GroupDecodeOracle : OracleSpec Unit := fun _ => (BitVec bitLength × ι, Unit)
def GroupDecodeOracle : OracleSpec (BitVec bitLength × ι) := fun _ => Unit

end OracleSpec

Expand All @@ -84,26 +84,26 @@ variable {ι : Type} [DecidableEq ι] {G : Type} [Group G] {p : ℕ}
/-- Implementation of the group operation oracle, which changes some underlying table of group
elements, using the group operation `op`. If the indices `i` and `j` does not contain group
elements yet, the oracle will fail. -/
def implGroupOpOracle : QueryImpl (GroupOpOracle ι) (StateT (GroupValTable ι G) Option) where
impl | query _ ⟨i, j, k⟩ => fun table =>
def implGroupOpOracle : QueryImpl (GroupOpOracle ι) (StateT (GroupValTable ι G) Option) :=
fun | ⟨i, j, k⟩ => fun table =>
match table i, table j with
| some g₁, some g₂ => some ((), table.update k (some (g₁ * g₂)))
| _, _ => none

/-- Implementation of the group exponent oracle, which computes the group element at the index `i`
raised to the power `a`, storing the result at index `j`. This will fail if the index `i` does
not contain a group element yet. -/
def implGroupExpOracle : QueryImpl (GroupExpOracle ι p) (StateT (GroupValTable ι G) Option) where
impl | query _ ⟨i, a, j⟩ => fun table =>
def implGroupExpOracle : QueryImpl (GroupExpOracle ι p) (StateT (GroupValTable ι G) Option) :=
fun | ⟨i, a, j⟩ => fun table =>
match table i with
| some g => some ((), table.update j (some (g ^ a.val)))
| none => none

/-- Implementation of the group equality oracle, which checks if the group elements at the indices
`i` and `j` are equal, and leave the table unchanged. -/
def implGroupEqOracle [BEq G] :
QueryImpl (GroupEqOracle ι) (StateT (GroupValTable ι G) Option) where
impl | query _ ⟨i, j⟩ => fun table =>
QueryImpl (GroupEqOracle ι) (StateT (GroupValTable ι G) Option) :=
fun | ⟨i, j⟩ => fun table =>
match table i, table j with
| some g₁, some g₂ => some (g₁ == g₂, table)
| _, _ => none
Expand All @@ -114,8 +114,8 @@ variable {bitLength : ℕ}
at the index `i`, leaving the table unchanged. This will fail if the index `i` does not contain
a group element yet. -/
def implGroupEncodeOracle [Serialize G (BitVec bitLength)] :
QueryImpl (GroupEncodeOracle ι bitLength) (StateT (GroupValTable ι G) Option) where
impl | query _ i => fun table =>
QueryImpl (GroupEncodeOracle ι bitLength) (StateT (GroupValTable ι G) Option) :=
fun | i => fun table =>
match table i with
| some g => some (serialize g, table)
| none => none
Expand All @@ -124,8 +124,8 @@ def implGroupEncodeOracle [Serialize G (BitVec bitLength)] :
bit encoding into the table, if the bit encoding is valid. This will fail if the bit encoding
is invalid. -/
def implGroupDecodeOracle [DeserializeOption G (BitVec bitLength)] :
QueryImpl (GroupDecodeOracle ι bitLength) (StateT (GroupValTable ι G) Option) where
impl | query _ (b, i) => fun table =>
QueryImpl (GroupDecodeOracle ι bitLength) (StateT (GroupValTable ι G) Option) :=
fun | (b, i) => fun table =>
match DeserializeOption.deserialize b with
| some g => some ((), table.update i (some g))
| none => none
Expand All @@ -148,8 +148,8 @@ TODO: need to be sure this definition is correct.
-/
def Adversary (ι : Type) (G : Type) (p : ℕ) (bitLength : ℕ) (α : Type) : Type _ :=
ReaderT (GroupValTable ι G)
(OracleComp (GroupOpOracle ι ++ₒ GroupExpOracle ι p ++ₒ
GroupEqOracle ι ++ₒ GroupEncodeOracle ι bitLength))
(OracleComp (GroupOpOracle ι + GroupExpOracle ι p +
GroupEqOracle ι + GroupEncodeOracle ι bitLength))
(List ι × α)

namespace Adversary
Expand Down
Loading
Loading