fix typo in u128s_from_felt252

lindy-labs · Jun 21, 2024 · 6318bf0 · 6318bf0
1 parent a6d1f64
commit 6318bf0
Show file tree

Hide file tree

Showing 2 changed files with 3 additions and 8 deletions.
diff --git a/Aegis/Libfuncs/UInt128.lean b/Aegis/Libfuncs/UInt128.lean
@@ -44,7 +44,7 @@ def u128s_from_felt252 : FuncData where
                    q(($a).val < U128_MOD ∧ $ρ = ($a).cast) },
                { outputTypes := [RangeCheck, U128, U128]
                  condition := fun _ (a : Q(F)) _ (ρ_high ρ_low : Q(UInt128)) =>
-                   q(U128_MOD ≤ ($a).val ∧ $ρ_high = $(a).val % U128_MOD
+                   q(U128_MOD ≤ ($a).val ∧ $ρ_high = $(a).val / U128_MOD
                      ∧ $ρ_low = $(a).cast) }]
 
 def u128_safe_divmod : FuncData where

diff --git a/Aegis/Tests/Libfuncs/U128/U128sFromFelt252.lean b/Aegis/Tests/Libfuncs/U128/U128sFromFelt252.lean
@@ -7,16 +7,11 @@ aegis_load_file "../../e2e_libfuncs/u128_aegis/u128s_from_felt252.sierra"
 aegis_spec "test::foo" :=
   fun _ _ a _ ρ =>
   a.val < U128_MOD ∧ ρ = .inl a.cast
-  ∨ U128_MOD ≤ a.val ∧ ρ = .inr ((a.val % U128_MOD : UInt128), a.cast)
+  ∨ U128_MOD ≤ a.val ∧ ρ = .inr ((a.val / U128_MOD : UInt128), a.cast)
 
 aegis_prove "test::foo" :=
   fun _ _ a _ ρ => by
   unfold «spec_test::foo»
-  rename_i x x_1 x_2
-  intro h_auto
-  simp_all only [ZMod.nat_cast_mod]
-  unhygienic aesop_cases h_auto
-  · simp_all only [and_self, true_or]
-  · simp_all only [and_self, or_true]
+  aesop
 
 aegis_complete