Generated library for numbers

hacspec · Nov 26, 2024 · f709d7c · f709d7c
1 parent 01e7ecd
commit f709d7c
Show file tree

Hide file tree

Showing 39 changed files with 23,257 additions and 0 deletions.
diff --git a/proof-libs/fstar/generated_core/Core.Base.Binary.fst b/proof-libs/fstar/generated_core/Core.Base.Binary.fst
@@ -0,0 +1,168 @@
+module Core.Base.Binary
+#set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
+open Core
+open FStar.Mul
+
+let rec positive_cmp__cmp_binary_cont
+      (x y: Core.Base.Spec.Binary.Positive.t_Positive)
+      (r: Core.Cmp.t_Ordering)
+    : Core.Cmp.t_Ordering =
+  match Core.Base.Spec.Binary.Positive.match_positive x with
+  | Core.Base.Spec.Binary.Positive.POSITIVE_XH  ->
+    (match Core.Base.Spec.Binary.Positive.match_positive y with
+      | Core.Base.Spec.Binary.Positive.POSITIVE_XH  -> r
+      | Core.Base.Spec.Binary.Positive.POSITIVE_XO q
+      | Core.Base.Spec.Binary.Positive.POSITIVE_XI q ->
+        Core.Cmp.Ordering_Less <: Core.Cmp.t_Ordering)
+  | Core.Base.Spec.Binary.Positive.POSITIVE_XO p ->
+    (match Core.Base.Spec.Binary.Positive.match_positive y with
+      | Core.Base.Spec.Binary.Positive.POSITIVE_XH  ->
+        Core.Cmp.Ordering_Greater <: Core.Cmp.t_Ordering
+      | Core.Base.Spec.Binary.Positive.POSITIVE_XO q -> positive_cmp__cmp_binary_cont p q r
+      | Core.Base.Spec.Binary.Positive.POSITIVE_XI q ->
+        positive_cmp__cmp_binary_cont p q (Core.Cmp.Ordering_Less <: Core.Cmp.t_Ordering))
+  | Core.Base.Spec.Binary.Positive.POSITIVE_XI p ->
+    match Core.Base.Spec.Binary.Positive.match_positive y with
+    | Core.Base.Spec.Binary.Positive.POSITIVE_XH  ->
+      Core.Cmp.Ordering_Greater <: Core.Cmp.t_Ordering
+    | Core.Base.Spec.Binary.Positive.POSITIVE_XO q ->
+      positive_cmp__cmp_binary_cont p q (Core.Cmp.Ordering_Greater <: Core.Cmp.t_Ordering)
+    | Core.Base.Spec.Binary.Positive.POSITIVE_XI q -> positive_cmp__cmp_binary_cont p q r
+
+let positive_cmp (lhs rhs: Core.Base.Spec.Binary.Positive.t_Positive) : Core.Cmp.t_Ordering =
+  positive_cmp__cmp_binary_cont lhs rhs (Core.Cmp.Ordering_Equal <: Core.Cmp.t_Ordering)
+
+let positive_le (lhs rhs: Core.Base.Spec.Binary.Positive.t_Positive) : bool =
+  match
+    Core.Option.Option_Some (positive_cmp lhs rhs) <: Core.Option.t_Option Core.Cmp.t_Ordering
+  with
+  | Core.Option.Option_Some (Core.Cmp.Ordering_Less )
+  | Core.Option.Option_Some (Core.Cmp.Ordering_Equal ) -> true
+  | _ -> false
+
+let rec positive_pred_double (s: Core.Base.Spec.Binary.Positive.t_Positive)
+    : Core.Base.Spec.Binary.Positive.t_Positive =
+  match Core.Base.Spec.Binary.Positive.match_positive s with
+  | Core.Base.Spec.Binary.Positive.POSITIVE_XH  -> Core.Base.Spec.Binary.Positive.xH
+  | Core.Base.Spec.Binary.Positive.POSITIVE_XO p ->
+    Core.Base.Spec.Binary.Positive.xI (positive_pred_double p
+        <:
+        Core.Base.Spec.Binary.Positive.t_Positive)
+  | Core.Base.Spec.Binary.Positive.POSITIVE_XI p ->
+    Core.Base.Spec.Binary.Positive.xI (Core.Base.Spec.Binary.Positive.xO p
+        <:
+        Core.Base.Spec.Binary.Positive.t_Positive)
+
+let rec positive_succ (s: Core.Base.Spec.Binary.Positive.t_Positive)
+    : Core.Base.Spec.Binary.Positive.t_Positive =
+  match Core.Base.Spec.Binary.Positive.match_positive s with
+  | Core.Base.Spec.Binary.Positive.POSITIVE_XH  ->
+    Core.Base.Spec.Binary.Positive.xO Core.Base.Spec.Binary.Positive.xH
+  | Core.Base.Spec.Binary.Positive.POSITIVE_XO q -> Core.Base.Spec.Binary.Positive.xI q
+  | Core.Base.Spec.Binary.Positive.POSITIVE_XI q ->
+    Core.Base.Spec.Binary.Positive.xO (positive_succ q <: Core.Base.Spec.Binary.Positive.t_Positive)
+
+let positive_add (lhs rhs: Core.Base.Spec.Binary.Positive.t_Positive)
+    : Core.Base.Spec.Binary.Positive.t_Positive = positive_add__add lhs rhs
+
+let rec positive_mul (lhs rhs: Core.Base.Spec.Binary.Positive.t_Positive)
+    : Core.Base.Spec.Binary.Positive.t_Positive =
+  match Core.Base.Spec.Binary.Positive.match_positive lhs with
+  | Core.Base.Spec.Binary.Positive.POSITIVE_XH  -> rhs
+  | Core.Base.Spec.Binary.Positive.POSITIVE_XO p ->
+    Core.Base.Spec.Binary.Positive.xO (positive_mul p rhs
+        <:
+        Core.Base.Spec.Binary.Positive.t_Positive)
+  | Core.Base.Spec.Binary.Positive.POSITIVE_XI p ->
+    positive_add (Core.Clone.f_clone #Core.Base.Spec.Binary.Positive.t_Positive
+          #FStar.Tactics.Typeclasses.solve
+          rhs
+        <:
+        Core.Base.Spec.Binary.Positive.t_Positive)
+      (Core.Base.Spec.Binary.Positive.xO (positive_mul p rhs
+            <:
+            Core.Base.Spec.Binary.Positive.t_Positive)
+        <:
+        Core.Base.Spec.Binary.Positive.t_Positive)
+
+let rec positive_add__add (lhs rhs: Core.Base.Spec.Binary.Positive.t_Positive)
+    : Core.Base.Spec.Binary.Positive.t_Positive =
+  match Core.Base.Spec.Binary.Positive.match_positive lhs with
+  | Core.Base.Spec.Binary.Positive.POSITIVE_XH  ->
+    (match Core.Base.Spec.Binary.Positive.match_positive rhs with
+      | Core.Base.Spec.Binary.Positive.POSITIVE_XH  ->
+        Core.Base.Spec.Binary.Positive.xO Core.Base.Spec.Binary.Positive.xH
+      | Core.Base.Spec.Binary.Positive.POSITIVE_XO q -> Core.Base.Spec.Binary.Positive.xI q
+      | Core.Base.Spec.Binary.Positive.POSITIVE_XI q ->
+        Core.Base.Spec.Binary.Positive.xO (positive_succ q
+            <:
+            Core.Base.Spec.Binary.Positive.t_Positive))
+  | Core.Base.Spec.Binary.Positive.POSITIVE_XO p ->
+    (match Core.Base.Spec.Binary.Positive.match_positive rhs with
+      | Core.Base.Spec.Binary.Positive.POSITIVE_XH  -> Core.Base.Spec.Binary.Positive.xI p
+      | Core.Base.Spec.Binary.Positive.POSITIVE_XO q ->
+        Core.Base.Spec.Binary.Positive.xO (positive_add__add p q
+            <:
+            Core.Base.Spec.Binary.Positive.t_Positive)
+      | Core.Base.Spec.Binary.Positive.POSITIVE_XI q ->
+        Core.Base.Spec.Binary.Positive.xI (positive_add__add p q
+            <:
+            Core.Base.Spec.Binary.Positive.t_Positive))
+  | Core.Base.Spec.Binary.Positive.POSITIVE_XI p ->
+    match Core.Base.Spec.Binary.Positive.match_positive rhs with
+    | Core.Base.Spec.Binary.Positive.POSITIVE_XH  ->
+      Core.Base.Spec.Binary.Positive.xO (positive_succ p
+          <:
+          Core.Base.Spec.Binary.Positive.t_Positive)
+    | Core.Base.Spec.Binary.Positive.POSITIVE_XO q ->
+      Core.Base.Spec.Binary.Positive.xI (positive_add__add p q
+          <:
+          Core.Base.Spec.Binary.Positive.t_Positive)
+    | Core.Base.Spec.Binary.Positive.POSITIVE_XI q ->
+      Core.Base.Spec.Binary.Positive.xO (positive_add__add_carry p q
+          <:
+          Core.Base.Spec.Binary.Positive.t_Positive)
+
+and positive_add__add_carry (lhs rhs: Core.Base.Spec.Binary.Positive.t_Positive)
+    : Core.Base.Spec.Binary.Positive.t_Positive =
+  match Core.Base.Spec.Binary.Positive.match_positive lhs with
+  | Core.Base.Spec.Binary.Positive.POSITIVE_XH  ->
+    (match Core.Base.Spec.Binary.Positive.match_positive rhs with
+      | Core.Base.Spec.Binary.Positive.POSITIVE_XH  ->
+        Core.Base.Spec.Binary.Positive.xI Core.Base.Spec.Binary.Positive.xH
+      | Core.Base.Spec.Binary.Positive.POSITIVE_XO q ->
+        Core.Base.Spec.Binary.Positive.xO (positive_succ q
+            <:
+            Core.Base.Spec.Binary.Positive.t_Positive)
+      | Core.Base.Spec.Binary.Positive.POSITIVE_XI q ->
+        Core.Base.Spec.Binary.Positive.xI (positive_succ q
+            <:
+            Core.Base.Spec.Binary.Positive.t_Positive))
+  | Core.Base.Spec.Binary.Positive.POSITIVE_XO p ->
+    (match Core.Base.Spec.Binary.Positive.match_positive rhs with
+      | Core.Base.Spec.Binary.Positive.POSITIVE_XH  ->
+        Core.Base.Spec.Binary.Positive.xO (positive_succ p
+            <:
+            Core.Base.Spec.Binary.Positive.t_Positive)
+      | Core.Base.Spec.Binary.Positive.POSITIVE_XO q ->
+        Core.Base.Spec.Binary.Positive.xI (positive_add__add p q
+            <:
+            Core.Base.Spec.Binary.Positive.t_Positive)
+      | Core.Base.Spec.Binary.Positive.POSITIVE_XI q ->
+        Core.Base.Spec.Binary.Positive.xO (positive_add__add_carry p q
+            <:
+            Core.Base.Spec.Binary.Positive.t_Positive))
+  | Core.Base.Spec.Binary.Positive.POSITIVE_XI p ->
+    match Core.Base.Spec.Binary.Positive.match_positive rhs with
+    | Core.Base.Spec.Binary.Positive.POSITIVE_XH  ->
+      Core.Base.Spec.Binary.Positive.xI (positive_succ p
+          <:
+          Core.Base.Spec.Binary.Positive.t_Positive)
+    | Core.Base.Spec.Binary.Positive.POSITIVE_XO q ->
+      Core.Base.Spec.Binary.Positive.xO (positive_add__add_carry p q
+          <:
+          Core.Base.Spec.Binary.Positive.t_Positive)
+    | Core.Base.Spec.Binary.Positive.POSITIVE_XI q ->
+      Core.Base.Spec.Binary.Positive.xI (positive_add__add_carry p q
+          <:
+          Core.Base.Spec.Binary.Positive.t_Positive)
diff --git a/proof-libs/fstar/generated_core/Core.Base.Number_conversion.fst b/proof-libs/fstar/generated_core/Core.Base.Number_conversion.fst
@@ -0,0 +1,76 @@
+module Core.Base.Number_conversion
+#set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
+open Core
+open FStar.Mul
+
+include Core.Intrinsics.Rec_bundle_253787241 {from_u128_binary as impl_24__from_u128_binary}
+
+include Core.Intrinsics.Rec_bundle_253787241 {impl_8 as impl_8}
+
+include Core.Intrinsics.Rec_bundle_253787241 {impl_20 as impl_20}
+
+include Core.Intrinsics.Rec_bundle_253787241 {from_u16_binary as impl_24__from_u16_binary}
+
+include Core.Intrinsics.Rec_bundle_253787241 {impl_2 as impl_2}
+
+include Core.Intrinsics.Rec_bundle_253787241 {impl_14 as impl_14}
+
+include Core.Intrinsics.Rec_bundle_253787241 {from_u32_binary as impl_24__from_u32_binary}
+
+include Core.Intrinsics.Rec_bundle_253787241 {impl_4 as impl_4}
+
+include Core.Intrinsics.Rec_bundle_253787241 {impl_16 as impl_16}
+
+include Core.Intrinsics.Rec_bundle_253787241 {from_u64_binary as impl_24__from_u64_binary}
+
+include Core.Intrinsics.Rec_bundle_253787241 {impl_6 as impl_6}
+
+include Core.Intrinsics.Rec_bundle_253787241 {impl_18 as impl_18}
+
+include Core.Intrinsics.Rec_bundle_253787241 {from_u8_binary as impl_24__from_u8_binary}
+
+include Core.Intrinsics.Rec_bundle_253787241 {impl as impl}
+
+include Core.Intrinsics.Rec_bundle_253787241 {impl_12 as impl_12}
+
+include Core.Intrinsics.Rec_bundle_253787241 {from_usize_binary as impl_24__from_usize_binary}
+
+include Core.Intrinsics.Rec_bundle_253787241 {impl_10 as impl_10}
+
+include Core.Intrinsics.Rec_bundle_253787241 {impl_22 as impl_22}
+
+include Core.Intrinsics.Rec_bundle_253787241 {to_u128_binary as impl_24__to_u128_binary}
+
+include Core.Intrinsics.Rec_bundle_253787241 {impl_9 as impl_9}
+
+include Core.Intrinsics.Rec_bundle_253787241 {impl_21 as impl_21}
+
+include Core.Intrinsics.Rec_bundle_253787241 {to_u16_binary as impl_24__to_u16_binary}
+
+include Core.Intrinsics.Rec_bundle_253787241 {impl_3 as impl_3}
+
+include Core.Intrinsics.Rec_bundle_253787241 {impl_15 as impl_15}
+
+include Core.Intrinsics.Rec_bundle_253787241 {to_u32_binary as impl_24__to_u32_binary}
+
+include Core.Intrinsics.Rec_bundle_253787241 {impl_5 as impl_5}
+
+include Core.Intrinsics.Rec_bundle_253787241 {impl_17 as impl_17}
+
+include Core.Intrinsics.Rec_bundle_253787241 {to_u64_binary as impl_24__to_u64_binary}
+
+include Core.Intrinsics.Rec_bundle_253787241 {impl_7 as impl_7}
+
+include Core.Intrinsics.Rec_bundle_253787241 {impl_19 as impl_19}
+
+include Core.Intrinsics.Rec_bundle_253787241 {to_u8_binary as impl_24__to_u8_binary}
+
+include Core.Intrinsics.Rec_bundle_253787241 {impl_1 as impl_1}
+
+include Core.Intrinsics.Rec_bundle_253787241 {impl_13 as impl_13}
+
+include Core.Intrinsics.Rec_bundle_253787241 {to_usize_binary as impl_24__to_usize_binary}
+
+include Core.Intrinsics.Rec_bundle_253787241 {impl_11 as impl_11}
+
+include Core.Intrinsics.Rec_bundle_253787241 {impl_23 as impl_23}