feat(bounded-ints): add AddAssign and SubAssign

cryspen · Jun 20, 2024 · 3a70732 · 3a70732
1 parent 33f9705
commit 3a70732
Show file tree

Hide file tree

Showing 2 changed files with 63 additions and 0 deletions.
diff --git a/proof-libs/fstar/core/Core.Num.fsti b/proof-libs/fstar/core/Core.Num.fsti
@@ -45,3 +45,53 @@ val impl__u8__from_str_radix: string -> u32 -> Core.Result.t_Result u8 Core.Num.
 val impl__usize__ilog2: i32 -> u32 
 val impl__usize__leading_zeros: usize -> u32
 
+open Core.Ops.Arith
+unfold instance add_assign_num_refined_refined t ($phi1 $phi2: int_t t -> bool)
+  : t_AddAssign (x: int_t t {phi1 x}) (y: int_t t {phi2 y}) = {
+    f_add_assign_pre = (fun (x: int_t t {phi1 x}) (y: int_t t {phi2 y}) -> phi1 (x +. y));
+    f_add_assign_post = (fun x y r -> x +. y = r);
+    f_add_assign = (fun x y -> x +. y);
+  }
+unfold instance add_assign_num_lhs_refined t ($phi1: int_t t -> bool)
+  : t_AddAssign (x: int_t t {phi1 x}) (y: int_t t) = {
+    f_add_assign_pre = (fun (x: int_t t {phi1 x}) (y: int_t t) -> phi1 (x +. y));
+    f_add_assign_post = (fun x y r -> x +. y = r);
+    f_add_assign = (fun x y -> x +. y);
+  }
+unfold instance add_assign_num_rhs_refined t ($phi1: int_t t -> bool)
+  : t_AddAssign (x: int_t t) (y: int_t t {phi1 y}) = {
+    f_add_assign_pre = (fun (x: int_t t) (y: int_t t {phi1 y}) -> true);
+    f_add_assign_post = (fun x y r -> x +. y = r);
+    f_add_assign = (fun x y -> x +. y);
+  }
+unfold instance add_assign_num t
+  : t_AddAssign (x: int_t t) (y: int_t t) = {
+    f_add_assign_pre = (fun (x: int_t t) (y: int_t t) -> true);
+    f_add_assign_post = (fun x y r -> x +. y = r);
+    f_add_assign = (fun x y -> x +. y);
+  }
+
+unfold instance sub_assign_num_refined_refined t ($phi1 $phi2: int_t t -> bool)
+  : t_SubAssign (x: int_t t {phi1 x}) (y: int_t t {phi2 y}) = {
+    f_sub_assign_pre = (fun (x: int_t t {phi1 x}) (y: int_t t {phi2 y}) -> phi1 (x -. y));
+    f_sub_assign_post = (fun x y r -> x -. y = r);
+    f_sub_assign = (fun x y -> x -. y);
+  }
+unfold instance sub_assign_num_lhs_refined t ($phi1: int_t t -> bool)
+  : t_SubAssign (x: int_t t {phi1 x}) (y: int_t t) = {
+    f_sub_assign_pre = (fun (x: int_t t {phi1 x}) (y: int_t t) -> phi1 (x -. y));
+    f_sub_assign_post = (fun x y r -> x -. y = r);
+    f_sub_assign = (fun x y -> x -. y);
+  }
+unfold instance sub_assign_num_rhs_refined t ($phi1: int_t t -> bool)
+  : t_SubAssign (x: int_t t) (y: int_t t {phi1 y}) = {
+    f_sub_assign_pre = (fun (x: int_t t) (y: int_t t {phi1 y}) -> true);
+    f_sub_assign_post = (fun x y r -> x -. y = r);
+    f_sub_assign = (fun x y -> x -. y);
+  }
+unfold instance sub_assign_num t
+  : t_SubAssign (x: int_t t) (y: int_t t) = {
+    f_sub_assign_pre = (fun (x: int_t t) (y: int_t t) -> true);
+    f_sub_assign_post = (fun x y r -> x -. y = r);
+    f_sub_assign = (fun x y -> x -. y);
+  }
diff --git a/proof-libs/fstar/core/Core.Ops.Arith.fsti b/proof-libs/fstar/core/Core.Ops.Arith.fsti
@@ -33,3 +33,16 @@ class t_Div self rhs = {
    f_div_post: self -> rhs -> f_Output -> bool;
    f_div: x:self -> y:rhs -> Pure f_Output (f_div_pre x y) (fun r -> f_div_post x y r);
 }
+
+class t_AddAssign self rhs = {
+  f_add_assign_pre: self -> rhs -> bool;
+  f_add_assign_post: self -> rhs -> self -> bool;
+  f_add_assign: x:self -> y:rhs -> Pure self (f_add_assign_pre x y) (fun r -> f_add_assign_post x y r);
+}
+
+class t_SubAssign self rhs = {
+  f_sub_assign_pre: self -> rhs -> bool;
+  f_sub_assign_post: self -> rhs -> self -> bool;
+  f_sub_assign: x:self -> y:rhs -> Pure self (f_sub_assign_pre x y) (fun r -> f_sub_assign_post x y r);
+}
+