add libfunc tests for U8, fix u8_sqrt implementation

Aegis/Libfuncs/UInt8.lean

@@ -61,7 +61,6 @@ def u8_const (n : Q(UInt8)) : FuncData where
 
 def u8_eq : FuncData where
   inputTypes := [U8, U8]
-  -- TODO double check the order of branches
   branches := [{ condition := fun (a b : Q(UInt8)) => q($a ≠ $b) },
                { condition := fun (a b : Q(UInt8)) => q($a = $b) }]
 
@@ -91,7 +90,7 @@ def u8_sqrt : FuncData where
   inputTypes := [RangeCheck, U8]
   branches := [{ outputTypes := [RangeCheck, U8]
                  condition := fun _ (a : Q(UInt8)) _ (ρ : Q(UInt8)) =>
-                   q($ρ * $ρ = $a) }]
+                   q($(ρ).val = $(a).val.sqrt) }]
 
 def uint8Libfuncs : Identifier → Option FuncData
 | .name "u8_overflowing_add" [] .none      => u8_overflowing_add

Aegis/Tests/Libfuncs/U8/U8Eq.lean

@@ -0,0 +1,22 @@
+import Aegis.Commands
+
+open Sierra
+
+aegis_load_file "../../e2e_libfuncs/u8_aegis/u8_eq.sierra"
+
+aegis_spec "test::foo" :=
+  fun _ ρ =>
+  ρ = Bool.toSierraBool .false
+
+aegis_prove "test::foo" :=
+  fun _ ρ => by
+  unfold «spec_test::foo»
+  rintro (⟨-,rfl⟩|⟨h,rfl⟩)
+  · simp
+  · rw [← sub_eq_zero] at h
+    norm_num at h
+    letI : Fact (1 < U8_MOD) := ⟨by norm_num [U8_MOD]⟩
+    rw [← @ZMod.val_eq_zero, ZMod.val_one U8_MOD] at h
+    simp_all
+
+aegis_complete

Aegis/Tests/Libfuncs/U8/U8IsZero.lean

@@ -0,0 +1,18 @@
+import Aegis.Commands
+
+open Sierra
+
+aegis_load_file "../../e2e_libfuncs/u8_aegis/u8_is_zero.sierra"
+
+aegis_spec "test::foo" :=
+  fun _ a ρ =>
+  ρ =  if a = 0 then 123 else a
+
+aegis_prove "test::foo" :=
+  fun _ a ρ => by
+  unfold «spec_test::foo»
+  rintro (⟨rfl,rfl⟩|⟨h,rfl⟩)
+  · simp
+  · simp [h]
+
+aegis_complete

Aegis/Tests/Libfuncs/U8/U8OverflowingAdd.lean

@@ -0,0 +1,21 @@
+import Aegis.Commands
+
+open Sierra
+
+aegis_load_file "../../e2e_libfuncs/u8_aegis/u8_overflowing_add.sierra"
+
+aegis_spec "test::foo" :=
+  fun _ _ a b _ ρ =>
+  a.val + b.val < U8_MOD ∧ ρ = .inl (a + b)
+  ∨ U8_MOD ≤ a.val + b.val ∧ ρ = .inr (a + b)
+
+aegis_prove "test::foo" :=
+  fun _ _ a b _ ρ => 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

Aegis/Tests/Libfuncs/U8/U8OverflowingSub.lean

@@ -0,0 +1,21 @@
+import Aegis.Commands
+
+open Sierra
+
+aegis_load_file "../../e2e_libfuncs/u8_aegis/u8_overflowing_sub.sierra"
+
+aegis_spec "test::foo" :=
+  fun _ _ a b _ ρ =>
+  b.val ≤ a.val ∧ ρ = .inl (a - b)
+  ∨ a.val < b.val ∧ ρ = .inr (a - b)
+
+aegis_prove "test::foo" :=
+  fun _ _ a b _ ρ => 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

Aegis/Tests/Libfuncs/U8/U8SafeDivmod.lean

@@ -0,0 +1,19 @@
+import Aegis.Commands
+
+open Sierra
+
+aegis_load_file "../../e2e_libfuncs/u8_aegis/u8_safe_divmod.sierra"
+
+aegis_spec "test::foo" :=
+  fun _ _ a b _ ρ =>
+  ρ = (a.ndiv b, a.nmod b)
+
+aegis_prove "test::foo" :=
+  fun _ _ a b _ ρ => by
+  unfold «spec_test::foo»
+  rename_i x x_1 x_2
+  intro h_auto
+  aesop_subst h_auto
+  simp_all only
+
+aegis_complete

Aegis/Tests/Libfuncs/U8/U8Sqrt.lean

@@ -0,0 +1,18 @@
+import Aegis.Commands
+
+open Sierra
+
+aegis_load_file "../../e2e_libfuncs/u8_aegis/u8_sqrt.sierra"
+
+aegis_spec "test::foo" :=
+  fun _ _ a _ ρ =>
+  ρ.val = a.val.sqrt
+
+aegis_prove "test::foo" :=
+  fun _ _ a _ ρ => by
+  unfold «spec_test::foo»
+  rename_i x x_1 x_2
+  intro h_auto
+  simp_all only [exists_eq_right]
+
+aegis_complete