add remaining u8 libfunc tests

lindy-labs · Apr 9, 2024 · 65a37fe · 65a37fe
1 parent 6d9f2ae
commit 65a37fe
Show file tree

Hide file tree

Showing 2 changed files with 40 additions and 0 deletions.
diff --git a/Aegis/Tests/Libfuncs/U8/U8TryFromFelt252.lean b/Aegis/Tests/Libfuncs/U8/U8TryFromFelt252.lean
@@ -0,0 +1,21 @@
+import Aegis.Commands
+
+open Sierra
+
+aegis_load_file "../../e2e_libfuncs/u8_aegis/u8_try_from_felt252.sierra"
+
+aegis_spec "test::foo" :=
+  fun _ _ a _ ρ =>
+  a.val < U8_MOD ∧ ρ = .inl a.cast
+  ∨ U8_MOD ≤ a.val ∧ ρ = .inr ()
+
+aegis_prove "test::foo" :=
+  fun _ _ a _ ρ => by
+  unfold «spec_test::foo»
+  rename_i x x_1 x_2
+  intro h_auto
+  unhygienic aesop_cases h_auto
+  · simp_all only [and_self, true_or]
+  · simp_all only [and_self, or_true]
+
+aegis_complete
diff --git a/Aegis/Tests/Libfuncs/U8/U8WideMul.lean b/Aegis/Tests/Libfuncs/U8/U8WideMul.lean
@@ -0,0 +1,19 @@
+import Aegis.Commands
+
+open Sierra
+
+aegis_load_file "../../e2e_libfuncs/u8_aegis/u8_wide_mul.sierra"
+
+aegis_spec "test::foo" :=
+  fun _ a b ρ =>
+  ρ = a.cast * b.cast
+
+aegis_prove "test::foo" :=
+  fun _ a b ρ => by
+  unfold «spec_test::foo»
+  rename_i x
+  intro h_auto
+  aesop_subst h_auto
+  simp_all only
+
+aegis_complete