build errors

dtumad · Mar 10, 2024 · 716f85a · 716f85a
1 parent dce6c36
commit 716f85a
Show file tree

Hide file tree

Showing 4 changed files with 3 additions and 3 deletions.
diff --git a/...tional_monads/asymptotics/negligable.lean → ...tional_monads/asymptotics/negligible.lean b/...tional_monads/asymptotics/negligable.lean → ...tional_monads/asymptotics/negligible.lean
diff --git a/src/crypto_foundations/hardness_assumptions/hard_homogeneous_space.lean b/src/crypto_foundations/hardness_assumptions/hard_homogeneous_space.lean
@@ -21,7 +21,7 @@ and further extend this with various assumptions about run times of computations
 -/
 
 open_locale big_operators ennreal
-open oracle_comp oracle_spec
+open oracle_comp oracle_spec asymptotics
 
 /-- An `algorithmic_homogenous_space` is a homogenous space where operations are all `poly_time`.
 Uses mathlib's definition of an `add_torsor`, which is a bijective group action.

diff --git a/src/crypto_foundations/primitives/asymm_enc.lean b/src/crypto_foundations/primitives/asymm_enc.lean
@@ -181,6 +181,6 @@ variables {spec : ℕ → oracle_spec} {M PK SK C : ℕ → Type}
 
 def ind_cpa_secure (enc_scheme : asymm_enc_scheme spec M PK SK C) : Prop :=
 ∀ (adv : Π (sp : ℕ), (enc_scheme sp).ind_cpa_adv),
-  negligible (λ sp, (ind_cpa_exp (adv sp)).advantage)
+  asymptotics.negligible (λ sp, (ind_cpa_exp (adv sp)).advantage)
 
 end asymm_enc_scheme
diff --git a/src/crypto_foundations/primitives/hash_function.lean b/src/crypto_foundations/primitives/hash_function.lean
@@ -48,6 +48,6 @@ variables {spec : ℕ → oracle_spec} {K I O : ℕ → Type}
   of winning the `collision_finding_experiment` as the security parameter increases -/
 def collision_resistant (hf : hash_scheme spec K I O) : Prop :=
 ∀ (adv : Π (sp : ℕ), (hf sp).collision_finding_adv),
-negligible (λ sp, (collision_finding_exp (adv sp)).advantage)
+  asymptotics.negligible (λ sp, (collision_finding_exp (adv sp)).advantage)
 
 end hash_scheme