From f3499685db0bcf55aa93610038992ae1ffb8e721 Mon Sep 17 00:00:00 2001 From: Lasse Letager Hansen Date: Tue, 29 Oct 2024 23:09:01 +0100 Subject: [PATCH] Add Coq Core Lib --- proof-libs/coq/coq/.gitignore | 7 + proof-libs/coq/coq/_CoqProject | 41 + proof-libs/coq/coq/src/Core_Array.v | 72 + proof-libs/coq/coq/src/Core_Base_Int.v | 30 + .../coq/coq/src/Core_Base_Int_Base_impl.v | 617 ++++++++ .../coq/coq/src/Core_Base_Int_Base_spec.v | 129 ++ .../coq/src/Core_Base_Int_Number_conversion.v | 80 + proof-libs/coq/coq/src/Core_Base_Seq.v | 30 + .../coq/coq/src/Core_Base_Seq_Base_impl.v | 142 ++ .../coq/coq/src/Core_Base_Seq_Base_spec.v | 20 + proof-libs/coq/coq/src/Core_Clone.v | 13 + proof-libs/coq/coq/src/Core_Cmp.v | 165 ++ proof-libs/coq/coq/src/Core_Coerce.v | 21 + proof-libs/coq/coq/src/Core_Convert.v | 32 + proof-libs/coq/coq/src/Core_Int.v | 1321 +++++++++++++++++ proof-libs/coq/coq/src/Core_Intrinsics.v | 119 ++ proof-libs/coq/coq/src/Core_Marker.v | 31 + proof-libs/coq/coq/src/Core_Num.v | 317 ++++ proof-libs/coq/coq/src/Core_Ops.v | 52 + proof-libs/coq/coq/src/Core_Ops_Arith.v | 59 + proof-libs/coq/coq/src/Core_Ops_Bit.v | 57 + proof-libs/coq/coq/src/Core_Option.v | 12 + proof-libs/coq/coq/src/Core_Panicking.v | 20 + proof-libs/coq/coq/src/Core_Primitive.v | 552 +++++++ 24 files changed, 3939 insertions(+) create mode 100644 proof-libs/coq/coq/.gitignore create mode 100644 proof-libs/coq/coq/_CoqProject create mode 100644 proof-libs/coq/coq/src/Core_Array.v create mode 100644 proof-libs/coq/coq/src/Core_Base_Int.v create mode 100644 proof-libs/coq/coq/src/Core_Base_Int_Base_impl.v create mode 100644 proof-libs/coq/coq/src/Core_Base_Int_Base_spec.v create mode 100644 proof-libs/coq/coq/src/Core_Base_Int_Number_conversion.v create mode 100644 proof-libs/coq/coq/src/Core_Base_Seq.v create mode 100644 proof-libs/coq/coq/src/Core_Base_Seq_Base_impl.v create mode 100644 proof-libs/coq/coq/src/Core_Base_Seq_Base_spec.v create mode 100644 proof-libs/coq/coq/src/Core_Clone.v create mode 100644 proof-libs/coq/coq/src/Core_Cmp.v create mode 100644 proof-libs/coq/coq/src/Core_Coerce.v create mode 100644 proof-libs/coq/coq/src/Core_Convert.v create mode 100644 proof-libs/coq/coq/src/Core_Int.v create mode 100644 proof-libs/coq/coq/src/Core_Intrinsics.v create mode 100644 proof-libs/coq/coq/src/Core_Marker.v create mode 100644 proof-libs/coq/coq/src/Core_Num.v create mode 100644 proof-libs/coq/coq/src/Core_Ops.v create mode 100644 proof-libs/coq/coq/src/Core_Ops_Arith.v create mode 100644 proof-libs/coq/coq/src/Core_Ops_Bit.v create mode 100644 proof-libs/coq/coq/src/Core_Option.v create mode 100644 proof-libs/coq/coq/src/Core_Panicking.v create mode 100644 proof-libs/coq/coq/src/Core_Primitive.v diff --git a/proof-libs/coq/coq/.gitignore b/proof-libs/coq/coq/.gitignore new file mode 100644 index 000000000..0b7287c5c --- /dev/null +++ b/proof-libs/coq/coq/.gitignore @@ -0,0 +1,7 @@ +*.vo* +*.aux +*.glob +*.cache +.Makefile.d +Makefile +Makefile.conf diff --git a/proof-libs/coq/coq/_CoqProject b/proof-libs/coq/coq/_CoqProject new file mode 100644 index 000000000..d24f4b58d --- /dev/null +++ b/proof-libs/coq/coq/_CoqProject @@ -0,0 +1,41 @@ +-R src/ Core +-arg -w +-arg all + +./src/Core_Clone.v + +./src/Core_Marker.v + +./src/Core_Option.v +./src/Core_Cmp.v + +./src/Core_Base_Int.v +./src/Core_Base_Int_Base_spec.v +./src/Core_Base_Int_Base_impl.v + +./src/Core_Coerce.v +./src/Core_Convert.v + +./src/Core_Ops_Arith.v +./src/Core_Ops_Bit.v + +./src/Core_Ops.v + +./src/Core_Int.v + +./src/Core_Base_Seq.v +./src/Core_Base_Seq_Base_spec.v + +./src/Core_Panicking.v + +./src/Core_Base_Seq_Base_impl.v + +./src/Core_Primitive.v + +./src/Core_Base_Int_Number_conversion.v + +./src/Core_Array.v + +./src/Core_Intrinsics.v + +./src/Core_Num.v diff --git a/proof-libs/coq/coq/src/Core_Array.v b/proof-libs/coq/coq/src/Core_Array.v new file mode 100644 index 000000000..99cc68b86 --- /dev/null +++ b/proof-libs/coq/coq/src/Core_Array.v @@ -0,0 +1,72 @@ +(* File automatically generated by Hacspec *) +From Coq Require Import ZArith. +Import List.ListNotations. +Open Scope Z_scope. +Open Scope bool_scope. +Require Import String. + + +From Core Require Import Core_Coerce (t_Abstraction). +Export Core_Coerce (t_Abstraction). + +From Core Require Import Core_Coerce (t_Concretization). +Export Core_Coerce (t_Concretization). + + +From Core Require Import Core_Base_Int_Number_conversion. +Export Core_Base_Int_Number_conversion. + +From Core Require Import Core_Base_Seq. +Export Core_Base_Seq. + +From Core Require Import Core_Int. +Export Core_Int. + + +From Core Require Import Core_Cmp. +Export Core_Cmp. + +From Core Require Import Core_Clone. +Export Core_Clone. + + +From Core Require Import Core_Primitive. +Export Core_Primitive. + +Instance t_Clone_427868774 `{v_T : Type} `{v_N : t_usize} `{t_Sized v_T} `{t_Clone v_T} : t_Clone (t_Array (v_T) (v_N)) := + { + t_Clone_f_clone := fun (self : t_Array (v_T) (v_N)) => + Build_t_Array (t_Clone_f_clone (t_Array_f_v self)); + }. + +Instance t_PartialEq_670168337 `{v_T : Type} `{v_N : t_usize} `{t_Sized v_T} `{t_Clone v_T} `{t_PartialEq v_T v_T} : t_PartialEq (t_Array (v_T) (v_N)) (t_Array (v_T) (v_N)) := + { + t_PartialEq_f_eq := fun (self : t_Array (v_T) (v_N)) (other : t_Array (v_T) (v_N)) => + t_PartialEq_f_eq (t_Clone_f_clone (t_Array_f_v self)) (t_Array_f_v other); + t_PartialEq_f_ne := fun (self : t_Array (v_T) (v_N)) (other : t_Array (v_T) (v_N)) => + negb (t_PartialEq_f_eq (t_Clone_f_clone (t_Array_f_v self)) (t_Array_f_v other)); + }. + +Definition impl_2__reverse `{v_T : Type} `{v_N : t_usize} `{t_Sized v_T} `{t_Clone v_T} (self : t_Array (v_T) (v_N)) : t_Array (v_T) (v_N) := + Build_t_Array (impl_2__rev (t_Array_f_v self)). + +Lemma lt_usize_implies_hax_int (x : t_usize) (y : t_usize) : + t_PartialOrd_f_lt (x) (y) = true -> + t_PartialOrd_f_lt (t_From_f_from (x)) (t_From_f_from (y)) = true. +Proof. Admitted. + +Lemma lift_usize_equality (x : t_HaxInt) (y : t_usize) : + t_PartialEq_f_eq (x) (t_From_f_from y) = true -> + t_PartialEq_f_eq (t_From_f_from (x)) (y) = true. +Proof. Admitted. + +Program Definition impl_2__index `{v_T : Type} `{v_N : t_usize} `{t_Sized v_T} `{t_Clone v_T} (self : t_Array (v_T) (v_N)) (i : t_usize) `{andb (t_PartialEq_f_eq (impl_2__len (t_Array_f_v self)) (t_From_f_from (v_N))) (t_PartialOrd_f_lt (i) (v_N)) = true} : v_T := + impl_2__get_index (H1 := _) (t_Array_f_v self) (t_From_f_from (i)). +Admit Obligations. + +Definition impl_2__new `{v_T : Type} `{v_N : t_usize} `{t_Sized v_T} `{t_Clone v_T} (x : v_T) : t_Array (v_T) (v_N) := + Build_t_Array (impl_2__repeat (t_From_f_from (v_N)) (x)). + +Program Definition impl_2__set_index `{v_T : Type} `{v_N : t_usize} `{t_Sized v_T} `{t_Clone v_T} (self : t_Array (v_T) (v_N)) (i : t_usize) (t : v_T) `{andb (t_PartialEq_f_eq (impl_2__len (t_Array_f_v self)) (t_From_f_from (v_N))) (t_PartialOrd_f_lt (i) (v_N)) = true} : t_Array (v_T) (v_N) := + Build_t_Array (impl_2__set_index (H1 := _) (t_Array_f_v self) (t_From_f_from (i)) (t)). +Admit Obligations. diff --git a/proof-libs/coq/coq/src/Core_Base_Int.v b/proof-libs/coq/coq/src/Core_Base_Int.v new file mode 100644 index 000000000..78d754524 --- /dev/null +++ b/proof-libs/coq/coq/src/Core_Base_Int.v @@ -0,0 +1,30 @@ +(* File automatically generated by Hacspec *) +From Coq Require Import ZArith. +Import List.ListNotations. +Open Scope Z_scope. +Open Scope bool_scope. +Require Import String. + +(* NotImplementedYet *) + +(* NotImplementedYet *) + +(* NotImplementedYet *) + +Definition t_HaxInt : Type := N. +Definition t_Positive : Type := positive. + +Notation "'t_POS'" := t_HaxInt. +Notation "'t_POS_POS_ZERO'" := N0. +Notation "'t_POS_POS_POS'" := Npos. + +Notation "'t_POSITIVE'" := t_Positive. +Notation "'t_POSITIVE_POSITIVE_XH'" := xH. +Notation "'t_POSITIVE_POSITIVE_XO'" := xO. +Notation "'t_POSITIVE_POSITIVE_XI'" := xI. + +Definition t_Unary : Type := nat. + +Notation "'t_UNARY'" := t_Unary. +Notation "'t_UNARY_UNARY_ZERO'" := O. +Notation "'t_UNARY_UNARY_SUCC'" := S. diff --git a/proof-libs/coq/coq/src/Core_Base_Int_Base_impl.v b/proof-libs/coq/coq/src/Core_Base_Int_Base_impl.v new file mode 100644 index 000000000..213d51628 --- /dev/null +++ b/proof-libs/coq/coq/src/Core_Base_Int_Base_impl.v @@ -0,0 +1,617 @@ +(* File automatically generated by Hacspec *) +From Coq Require Import ZArith. +Import List.ListNotations. +Open Scope Z_scope. +Open Scope bool_scope. +Require Import String. + +From Core Require Import Core_Base_Int. +Export Core_Base_Int. + + +From Core Require Import Core_Cmp. +Export Core_Cmp. + +From Core Require Import Core_Clone. +Export Core_Clone. + +From Core Require Import Core_Option. +Export Core_Option. + +From Core Require Import Core_Base_Int_Base_spec. +Export Core_Base_Int_Base_spec. + +Definition impl_7__sub__double_mask (lhs : t_HaxInt) : t_HaxInt := + match impl_9__match_pos (lhs) with + | t_POS_POS_ZERO => + impl_9__ZERO + | t_POS_POS_POS (p) => + impl_4__to_int (impl_8__xO (p)) + end. + +Definition impl_7__sub__succ_double_mask (lhs : t_HaxInt) : t_HaxInt := + match impl_9__match_pos (lhs) with + | t_POS_POS_ZERO => + impl_4__to_int (impl_8__xH) + | t_POS_POS_POS (p) => + impl_4__to_int (impl_8__xI (p)) + end. + +Definition impl_8__double (self : t_HaxInt) : t_HaxInt := + match impl_9__match_pos (self) with + | t_POS_POS_ZERO => + impl_9__ZERO + | t_POS_POS_POS (p) => + impl_4__to_int (impl_8__xO (p)) + end. + +Definition impl_8__half (self : t_HaxInt) : t_HaxInt := + match impl_9__match_pos (self) with + | t_POS_POS_ZERO => + impl_9__ZERO + | t_POS_POS_POS (n) => + match impl_8__match_positive (n) with + | t_POSITIVE_POSITIVE_XH => + impl_9__ZERO + | t_POSITIVE_POSITIVE_XO (p) => + impl_4__to_int (p) + | t_POSITIVE_POSITIVE_XI (p) => + impl_4__to_int (p) + end + end. + +Definition impl_8__succ_double (self : t_HaxInt) : t_Positive := + match impl_9__match_pos (self) with + | t_POS_POS_ZERO => + impl_8__xH + | t_POS_POS_POS (p) => + impl_8__xI (p) + end. + +Fixpoint impl__cmp__cmp_binary_cont (x : t_Positive) (y : t_Positive) (r : t_Ordering) : t_Ordering := + match impl_8__match_positive (x) with + | t_POSITIVE_POSITIVE_XH => + match impl_8__match_positive (y) with + | t_POSITIVE_POSITIVE_XH => + r + | t_POSITIVE_POSITIVE_XO (q) + | t_POSITIVE_POSITIVE_XI (q) => + t_Ordering_Ordering_Less + end + | t_POSITIVE_POSITIVE_XO (p) => + match impl_8__match_positive (y) with + | t_POSITIVE_POSITIVE_XH => + t_Ordering_Ordering_Greater + | t_POSITIVE_POSITIVE_XO (q) => + impl__cmp__cmp_binary_cont (p) (q) (r) + | t_POSITIVE_POSITIVE_XI (q) => + impl__cmp__cmp_binary_cont (p) (q) (t_Ordering_Ordering_Less) + end + | t_POSITIVE_POSITIVE_XI (p) => + match impl_8__match_positive (y) with + | t_POSITIVE_POSITIVE_XH => + t_Ordering_Ordering_Greater + | t_POSITIVE_POSITIVE_XO (q) => + impl__cmp__cmp_binary_cont (p) (q) (t_Ordering_Ordering_Greater) + | t_POSITIVE_POSITIVE_XI (q) => + impl__cmp__cmp_binary_cont (p) (q) (r) + end + end. + +Definition impl__cmp (lhs : t_Positive) (rhs : t_Positive) : t_Ordering := + impl__cmp__cmp_binary_cont (lhs) (rhs) (t_Ordering_Ordering_Equal). + +Instance t_PartialEq_427583131 : t_PartialEq (t_Positive) (t_Positive) := + { + t_PartialEq_f_eq := fun (self : t_Positive) (other : t_Positive) => + t_PartialEq_f_eq (impl__cmp (t_Clone_f_clone (self)) (t_Clone_f_clone (other))) (t_Ordering_Ordering_Equal); + t_PartialEq_f_ne := fun (self : t_Positive) (other : t_Positive) => + negb (t_PartialEq_f_eq (impl__cmp (t_Clone_f_clone (self)) (t_Clone_f_clone (other))) (t_Ordering_Ordering_Equal)); + }. + +Definition impl_2__cmp (lhs : t_HaxInt) (rhs : t_HaxInt) : t_Ordering := + match impl_9__match_pos (lhs) with + | t_POS_POS_ZERO => + match impl_9__match_pos (rhs) with + | t_POS_POS_ZERO => + t_Ordering_Ordering_Equal + | t_POS_POS_POS (q) => + t_Ordering_Ordering_Less + end + | t_POS_POS_POS (p) => + match impl_9__match_pos (rhs) with + | t_POS_POS_ZERO => + t_Ordering_Ordering_Greater + | t_POS_POS_POS (q) => + impl__cmp (p) (q) + end + end. + +Instance t_PartialEq_822848086 : t_PartialEq (t_HaxInt) (t_HaxInt) := + { + t_PartialEq_f_eq := fun (self : t_HaxInt) (other : t_HaxInt) => + t_PartialEq_f_eq (impl_2__cmp (t_Clone_f_clone (self)) (t_Clone_f_clone (other))) (t_Ordering_Ordering_Equal); + t_PartialEq_f_ne := fun (self : t_HaxInt) (other : t_HaxInt) => + negb (t_PartialEq_f_eq (impl_2__cmp (t_Clone_f_clone (self)) (t_Clone_f_clone (other))) (t_Ordering_Ordering_Equal)); + }. + +Fixpoint impl_4__succ (self : t_Positive) : t_Positive := + match impl_8__match_positive (self) with + | t_POSITIVE_POSITIVE_XH => + impl_8__xO (impl_8__xH) + | t_POSITIVE_POSITIVE_XO (q) => + impl_8__xI (q) + | t_POSITIVE_POSITIVE_XI (q) => + impl_8__xO (impl_4__succ (q)) + end. + +Fixpoint impl_7__sub__pred_double (lhs : t_Positive) : t_Positive := + match impl_8__match_positive (lhs) with + | t_POSITIVE_POSITIVE_XH => + impl_8__xH + | t_POSITIVE_POSITIVE_XO (p) => + impl_8__xI (impl_7__sub__pred_double (p)) + | t_POSITIVE_POSITIVE_XI (p) => + impl_8__xI (impl_8__xO (p)) + end. + +Definition impl_7__sub__double_pred_mask (lhs : t_Positive) : t_HaxInt := + match impl_8__match_positive (lhs) with + | t_POSITIVE_POSITIVE_XH => + impl_9__ZERO + | t_POSITIVE_POSITIVE_XO (p) => + impl_4__to_int (impl_8__xO (impl_7__sub__pred_double (p))) + | t_POSITIVE_POSITIVE_XI (p) => + impl_4__to_int (impl_8__xO (impl_8__xO (p))) + end. + +Fixpoint impl_9__power_of_two (self : t_Unary) : t_Positive := + match impl_6__match_unary (self) with + | t_UNARY_UNARY_ZERO => + impl_8__xH + | t_UNARY_UNARY_SUCC (x) => + impl_8__xO (impl_9__power_of_two (x)) + end. + +Fixpoint impl_12__shl__shl_helper (rhs : t_Unary) (lhs : t_HaxInt) : t_HaxInt := + if + impl_9__is_zero (t_Clone_f_clone (lhs)) + then + lhs + else + match impl_6__match_unary (rhs) with + | t_UNARY_UNARY_ZERO => + lhs + | t_UNARY_UNARY_SUCC (n) => + impl_12__shl__shl_helper (n) (impl_8__double (lhs)) + end. + +Definition impl_12__shl (self : t_HaxInt) (rhs : t_HaxInt) : t_HaxInt := + impl_12__shl__shl_helper (impl_5__from_int (rhs)) (self). + +Fixpoint impl_13__shr__shr_helper (rhs : t_Unary) (lhs : t_HaxInt) : t_HaxInt := + if + impl_9__is_zero (t_Clone_f_clone (lhs)) + then + lhs + else + match impl_6__match_unary (rhs) with + | t_UNARY_UNARY_ZERO => + lhs + | t_UNARY_UNARY_SUCC (n) => + impl_13__shr__shr_helper (n) (impl_8__half (lhs)) + end. + +Definition impl_13__shr (self : t_HaxInt) (rhs : t_HaxInt) : t_HaxInt := + impl_13__shr__shr_helper (impl_5__from_int (rhs)) (self). + +Fixpoint impl_14__bitxor__bitxor_binary (lhs : t_Positive) (rhs : t_Positive) : t_HaxInt := + match impl_8__match_positive (lhs) with + | t_POSITIVE_POSITIVE_XH => + match impl_8__match_positive (rhs) with + | t_POSITIVE_POSITIVE_XH => + impl_9__ZERO + | t_POSITIVE_POSITIVE_XO (q) => + impl_4__to_int (impl_8__xI (q)) + | t_POSITIVE_POSITIVE_XI (q) => + impl_4__to_int (impl_8__xO (q)) + end + | t_POSITIVE_POSITIVE_XO (p) => + match impl_8__match_positive (rhs) with + | t_POSITIVE_POSITIVE_XH => + impl_4__to_int (impl_8__xI (p)) + | t_POSITIVE_POSITIVE_XO (q) => + impl_8__double (impl_14__bitxor__bitxor_binary (p) (q)) + | t_POSITIVE_POSITIVE_XI (q) => + impl_4__to_int (impl_8__succ_double (impl_14__bitxor__bitxor_binary (p) (q))) + end + | t_POSITIVE_POSITIVE_XI (p) => + match impl_8__match_positive (rhs) with + | t_POSITIVE_POSITIVE_XH => + impl_4__to_int (impl_8__xO (p)) + | t_POSITIVE_POSITIVE_XO (q) => + impl_4__to_int (impl_8__succ_double (impl_14__bitxor__bitxor_binary (p) (q))) + | t_POSITIVE_POSITIVE_XI (q) => + impl_8__double (impl_14__bitxor__bitxor_binary (p) (q)) + end + end. + +Definition impl_14__bitxor (self : t_HaxInt) (rhs : t_HaxInt) : t_HaxInt := + match impl_9__match_pos (self) with + | t_POS_POS_ZERO => + rhs + | t_POS_POS_POS (p) => + match impl_9__match_pos (rhs) with + | t_POS_POS_ZERO => + impl_4__to_int (p) + | t_POS_POS_POS (q) => + impl_14__bitxor__bitxor_binary (p) (q) + end + end. + +Fixpoint impl_15__bitand__bitand_binary (lhs : t_Positive) (rhs : t_Positive) : t_HaxInt := + match impl_8__match_positive (lhs) with + | t_POSITIVE_POSITIVE_XH => + match impl_8__match_positive (rhs) with + | t_POSITIVE_POSITIVE_XO (q) => + impl_9__ZERO + | t_POSITIVE_POSITIVE_XI (_) + | t_POSITIVE_POSITIVE_XH => + impl_9__ONE + end + | t_POSITIVE_POSITIVE_XO (p) => + match impl_8__match_positive (rhs) with + | t_POSITIVE_POSITIVE_XH => + impl_9__ZERO + | t_POSITIVE_POSITIVE_XO (q) + | t_POSITIVE_POSITIVE_XI (q) => + impl_8__double (impl_15__bitand__bitand_binary (p) (q)) + end + | t_POSITIVE_POSITIVE_XI (p) => + match impl_8__match_positive (rhs) with + | t_POSITIVE_POSITIVE_XH => + impl_9__ONE + | t_POSITIVE_POSITIVE_XO (q) => + impl_8__double (impl_15__bitand__bitand_binary (p) (q)) + | t_POSITIVE_POSITIVE_XI (q) => + impl_4__to_int (impl_8__succ_double (impl_15__bitand__bitand_binary (p) (q))) + end + end. + +Definition impl_15__bitand (self : t_HaxInt) (rhs : t_HaxInt) : t_HaxInt := + match impl_9__match_pos (self) with + | t_POS_POS_ZERO => + impl_9__ZERO + | t_POS_POS_POS (p) => + match impl_9__match_pos (rhs) with + | t_POS_POS_ZERO => + impl_9__ZERO + | t_POS_POS_POS (q) => + impl_15__bitand__bitand_binary (p) (q) + end + end. + +Fixpoint impl_16__bitor__bitor_binary (lhs : t_Positive) (rhs : t_Positive) : t_Positive := + match impl_8__match_positive (lhs) with + | t_POSITIVE_POSITIVE_XH => + match impl_8__match_positive (rhs) with + | t_POSITIVE_POSITIVE_XO (q) => + impl_8__xI (q) + | t_POSITIVE_POSITIVE_XH => + impl_8__xH + | t_POSITIVE_POSITIVE_XI (q) => + impl_8__xI (q) + end + | t_POSITIVE_POSITIVE_XO (p) => + match impl_8__match_positive (rhs) with + | t_POSITIVE_POSITIVE_XH => + impl_8__xI (p) + | t_POSITIVE_POSITIVE_XO (q) => + impl_8__xO (impl_16__bitor__bitor_binary (p) (q)) + | t_POSITIVE_POSITIVE_XI (q) => + impl_8__xI (impl_16__bitor__bitor_binary (p) (q)) + end + | t_POSITIVE_POSITIVE_XI (p) => + match impl_8__match_positive (rhs) with + | t_POSITIVE_POSITIVE_XH => + impl_8__xI (p) + | t_POSITIVE_POSITIVE_XO (q) + | t_POSITIVE_POSITIVE_XI (q) => + impl_8__xI (impl_16__bitor__bitor_binary (p) (q)) + end + end. + +Definition impl_16__bitor (self : t_HaxInt) (rhs : t_HaxInt) : t_HaxInt := + match impl_9__match_pos (self) with + | t_POS_POS_ZERO => + rhs + | t_POS_POS_POS (p) => + match impl_9__match_pos (rhs) with + | t_POS_POS_ZERO => + impl_4__to_int (p) + | t_POS_POS_POS (q) => + impl_4__to_int (impl_16__bitor__bitor_binary (p) (q)) + end + end. + +Instance t_PartialOrd_895391065 : t_PartialOrd (t_Positive) (t_Positive) := + { + t_PartialOrd_f_partial_cmp := fun (self : t_Positive) (other : t_Positive) => + t_Option_Option_Some (impl__cmp (t_Clone_f_clone (self)) (t_Clone_f_clone (other))); + t_PartialOrd_f_lt := fun (self : t_Positive) (other : t_Positive) => + match t_Option_Option_Some (impl__cmp (t_Clone_f_clone (self)) (t_Clone_f_clone (other))) with + | t_Option_Option_Some (t_Ordering_Ordering_Less) => + true + | _ => + false + end; + t_PartialOrd_f_le := fun (self : t_Positive) (other : t_Positive) => + match t_Option_Option_Some (impl__cmp (t_Clone_f_clone (self)) (t_Clone_f_clone (other))) with + | t_Option_Option_Some (t_Ordering_Ordering_Less + | t_Ordering_Ordering_Equal) => + true + | _ => + false + end; + t_PartialOrd_f_gt := fun (self : t_Positive) (other : t_Positive) => + match t_Option_Option_Some (impl__cmp (t_Clone_f_clone (self)) (t_Clone_f_clone (other))) with + | t_Option_Option_Some (t_Ordering_Ordering_Greater) => + true + | _ => + false + end; + t_PartialOrd_f_ge := fun (self : t_Positive) (other : t_Positive) => + match t_Option_Option_Some (impl__cmp (t_Clone_f_clone (self)) (t_Clone_f_clone (other))) with + | t_Option_Option_Some (t_Ordering_Ordering_Greater + | t_Ordering_Ordering_Equal) => + true + | _ => + false + end; + }. + +Instance t_PartialOrd_414924529 : t_PartialOrd (t_HaxInt) (t_HaxInt) := + { + t_PartialOrd_f_partial_cmp := fun (self : t_HaxInt) (other : t_HaxInt) => + t_Option_Option_Some (impl_2__cmp (t_Clone_f_clone (self)) (t_Clone_f_clone (other))); + t_PartialOrd_f_lt := fun (self : t_HaxInt) (other : t_HaxInt) => + match t_Option_Option_Some (impl_2__cmp (t_Clone_f_clone (self)) (t_Clone_f_clone (other))) with + | t_Option_Option_Some (t_Ordering_Ordering_Less) => + true + | _ => + false + end; + t_PartialOrd_f_le := fun (self : t_HaxInt) (other : t_HaxInt) => + match t_Option_Option_Some (impl_2__cmp (t_Clone_f_clone (self)) (t_Clone_f_clone (other))) with + | t_Option_Option_Some (t_Ordering_Ordering_Less + | t_Ordering_Ordering_Equal) => + true + | _ => + false + end; + t_PartialOrd_f_gt := fun (self : t_HaxInt) (other : t_HaxInt) => + match t_Option_Option_Some (impl_2__cmp (t_Clone_f_clone (self)) (t_Clone_f_clone (other))) with + | t_Option_Option_Some (t_Ordering_Ordering_Greater) => + true + | _ => + false + end; + t_PartialOrd_f_ge := fun (self : t_HaxInt) (other : t_HaxInt) => + match t_Option_Option_Some (impl_2__cmp (t_Clone_f_clone (self)) (t_Clone_f_clone (other))) with + | t_Option_Option_Some (t_Ordering_Ordering_Greater + | t_Ordering_Ordering_Equal) => + true + | _ => + false + end; + }. + +Fixpoint impl_4__add (self : t_Positive) (rhs : t_Positive) : t_Positive := + match impl_8__match_positive (self) with + | t_POSITIVE_POSITIVE_XH => + match impl_8__match_positive (rhs) with + | t_POSITIVE_POSITIVE_XH => + impl_8__xO (impl_8__xH) + | t_POSITIVE_POSITIVE_XO (q) => + impl_8__xI (q) + | t_POSITIVE_POSITIVE_XI (q) => + impl_8__xO (impl_4__succ (q)) + end + | t_POSITIVE_POSITIVE_XO (p) => + match impl_8__match_positive (rhs) with + | t_POSITIVE_POSITIVE_XH => + impl_8__xI (p) + | t_POSITIVE_POSITIVE_XO (q) => + impl_8__xO (impl_4__add (p) (q)) + | t_POSITIVE_POSITIVE_XI (q) => + impl_8__xI (impl_4__add (p) (q)) + end + | t_POSITIVE_POSITIVE_XI (p) => + match impl_8__match_positive (rhs) with + | t_POSITIVE_POSITIVE_XH => + impl_8__xO (impl_4__succ (p)) + | t_POSITIVE_POSITIVE_XO (q) => + impl_8__xI (impl_4__add (p) (q)) + | t_POSITIVE_POSITIVE_XI (q) => + impl_8__xO (impl_4__add__add_carry (p) (q)) + end + end + +with impl_4__add__add_carry (lhs : t_Positive) (rhs : t_Positive) : t_Positive := + match impl_8__match_positive (lhs) with + | t_POSITIVE_POSITIVE_XH => + match impl_8__match_positive (rhs) with + | t_POSITIVE_POSITIVE_XH => + impl_8__xI (impl_8__xH) + | t_POSITIVE_POSITIVE_XO (q) => + impl_8__xO (impl_4__succ (q)) + | t_POSITIVE_POSITIVE_XI (q) => + impl_8__xI (impl_4__succ (q)) + end + | t_POSITIVE_POSITIVE_XO (p) => + match impl_8__match_positive (rhs) with + | t_POSITIVE_POSITIVE_XH => + impl_8__xO (impl_4__succ (p)) + | t_POSITIVE_POSITIVE_XO (q) => + impl_8__xI (impl_4__add (p) (q)) + | t_POSITIVE_POSITIVE_XI (q) => + impl_8__xO (impl_4__add__add_carry (p) (q)) + end + | t_POSITIVE_POSITIVE_XI (p) => + match impl_8__match_positive (rhs) with + | t_POSITIVE_POSITIVE_XH => + impl_8__xI (impl_4__succ (p)) + | t_POSITIVE_POSITIVE_XO (q) => + impl_8__xO (impl_4__add__add_carry (p) (q)) + | t_POSITIVE_POSITIVE_XI (q) => + impl_8__xI (impl_4__add__add_carry (p) (q)) + end + end. + +Definition impl_6__add (self : t_HaxInt) (rhs : t_HaxInt) : t_HaxInt := + match impl_9__match_pos (self) with + | t_POS_POS_ZERO => + rhs + | t_POS_POS_POS (p) => + match impl_9__match_pos (rhs) with + | t_POS_POS_ZERO => + impl_4__to_int (p) + | t_POS_POS_POS (q) => + impl_4__to_int (impl_4__add (p) (q)) + end + end. + +Fixpoint impl_7__sub__sub_binary (lhs : t_Positive) (rhs : t_Positive) : t_HaxInt := + match impl_8__match_positive (lhs) with + | t_POSITIVE_POSITIVE_XH => + impl_9__ZERO + | t_POSITIVE_POSITIVE_XO (p) => + match impl_8__match_positive (rhs) with + | t_POSITIVE_POSITIVE_XH => + impl_4__to_int (impl_7__sub__pred_double (p)) + | t_POSITIVE_POSITIVE_XO (q) => + impl_7__sub__double_mask (impl_7__sub__sub_binary (p) (q)) + | t_POSITIVE_POSITIVE_XI (q) => + impl_7__sub__succ_double_mask (impl_7__sub__sub_carry (p) (q)) + end + | t_POSITIVE_POSITIVE_XI (p) => + match impl_8__match_positive (rhs) with + | t_POSITIVE_POSITIVE_XH => + impl_4__to_int (impl_8__xO (p)) + | t_POSITIVE_POSITIVE_XO (q) => + impl_7__sub__succ_double_mask (impl_7__sub__sub_binary (p) (q)) + | t_POSITIVE_POSITIVE_XI (q) => + impl_7__sub__double_mask (impl_7__sub__sub_binary (p) (q)) + end + end + +with impl_7__sub__sub_carry (lhs : t_Positive) (rhs : t_Positive) : t_HaxInt := + match impl_8__match_positive (lhs) with + | t_POSITIVE_POSITIVE_XH => + impl_9__ZERO + | t_POSITIVE_POSITIVE_XO (p) => + match impl_8__match_positive (rhs) with + | t_POSITIVE_POSITIVE_XH => + impl_7__sub__double_pred_mask (p) + | t_POSITIVE_POSITIVE_XO (q) => + impl_7__sub__succ_double_mask (impl_7__sub__sub_carry (p) (q)) + | t_POSITIVE_POSITIVE_XI (q) => + impl_7__sub__double_mask (impl_7__sub__sub_carry (p) (q)) + end + | t_POSITIVE_POSITIVE_XI (p) => + match impl_8__match_positive (rhs) with + | t_POSITIVE_POSITIVE_XH => + impl_4__to_int (impl_7__sub__pred_double (p)) + | t_POSITIVE_POSITIVE_XO (q) => + impl_7__sub__double_mask (impl_7__sub__sub_binary (p) (q)) + | t_POSITIVE_POSITIVE_XI (q) => + impl_7__sub__succ_double_mask (impl_7__sub__sub_carry (p) (q)) + end + end. + +Definition impl_7__sub (self : t_HaxInt) (rhs : t_HaxInt) : t_HaxInt := + match impl_9__match_pos (self) with + | t_POS_POS_ZERO => + impl_9__ZERO + | t_POS_POS_POS (p) => + match impl_9__match_pos (rhs) with + | t_POS_POS_ZERO => + impl_4__to_int (p) + | t_POS_POS_POS (q) => + impl_7__sub__sub_binary (p) (q) + end + end. + +Fixpoint impl_5__mul (self : t_Positive) (rhs : t_Positive) : t_Positive := + match impl_8__match_positive (self) with + | t_POSITIVE_POSITIVE_XH => + rhs + | t_POSITIVE_POSITIVE_XO (p) => + impl_8__xO (impl_5__mul (p) (rhs)) + | t_POSITIVE_POSITIVE_XI (p) => + impl_4__add (t_Clone_f_clone (rhs)) (impl_8__xO (impl_5__mul (p) (rhs))) + end. + +Definition impl_11__mul (self : t_HaxInt) (rhs : t_HaxInt) : t_HaxInt := + match impl_9__match_pos (self) with + | t_POS_POS_ZERO => + impl_9__ZERO + | t_POS_POS_POS (p) => + match impl_9__match_pos (rhs) with + | t_POS_POS_ZERO => + impl_9__ZERO + | t_POS_POS_POS (q) => + impl_4__to_int (impl_5__mul (p) (q)) + end + end. + +Fixpoint impl_10__divmod__divmod_binary (a : t_Positive) (b : t_Positive) : (t_HaxInt*t_HaxInt) := + match impl_8__match_positive (a) with + | t_POSITIVE_POSITIVE_XH => + match impl_8__match_positive (b) with + | t_POSITIVE_POSITIVE_XH => + (impl_9__ONE,impl_9__ZERO) + | t_POSITIVE_POSITIVE_XO (q) + | t_POSITIVE_POSITIVE_XI (q) => + (impl_9__ZERO,impl_9__ONE) + end + | t_POSITIVE_POSITIVE_XO (a) => + let '(q,r) := impl_10__divmod__divmod_binary (a) (t_Clone_f_clone (b)) in + let r := impl_8__double (r) in + if + t_PartialOrd_f_le (impl_4__to_int (t_Clone_f_clone (b))) (t_Clone_f_clone (r)) + then + (impl_4__to_int (impl_8__succ_double (q)),impl_7__sub (r) (impl_4__to_int (b))) + else + (impl_8__double (q),r) + | t_POSITIVE_POSITIVE_XI (a) => + let '(q,r) := impl_10__divmod__divmod_binary (a) (t_Clone_f_clone (b)) in + let r := impl_4__to_int (impl_8__succ_double (r)) in + if + t_PartialOrd_f_le (impl_4__to_int (t_Clone_f_clone (b))) (t_Clone_f_clone (r)) + then + (impl_4__to_int (impl_8__succ_double (q)),impl_7__sub (r) (impl_4__to_int (b))) + else + (impl_8__double (q),r) + end. + +Definition impl_10__divmod (a : t_HaxInt) (b : t_HaxInt) : (t_HaxInt*t_HaxInt) := + match impl_9__match_pos (a) with + | t_POS_POS_ZERO => + (impl_9__ZERO,impl_9__ZERO) + | t_POS_POS_POS (p) => + match impl_9__match_pos (b) with + | t_POS_POS_ZERO => + (impl_9__ZERO,impl_4__to_int (p)) + | t_POS_POS_POS (q) => + impl_10__divmod__divmod_binary (p) (q) + end + end. + +Definition impl_10__div (self : t_HaxInt) (rhs : t_HaxInt) : t_HaxInt := + let '(q,r) := impl_10__divmod (self) (rhs) in + q. + +Definition impl_10__rem (self : t_HaxInt) (rhs : t_HaxInt) : t_HaxInt := + let '(q,r) := impl_10__divmod (self) (rhs) in + r. diff --git a/proof-libs/coq/coq/src/Core_Base_Int_Base_spec.v b/proof-libs/coq/coq/src/Core_Base_Int_Base_spec.v new file mode 100644 index 000000000..e8c46c4f8 --- /dev/null +++ b/proof-libs/coq/coq/src/Core_Base_Int_Base_spec.v @@ -0,0 +1,129 @@ +(* File automatically generated by Hacspec *) +From Coq Require Import ZArith. +Import List.ListNotations. +Open Scope Z_scope. +Open Scope bool_scope. +Require Import String. + +From Core Require Import Core_Base_Int. +Export Core_Base_Int. + +From Core Require Import Core_Clone (t_Clone). +Export Core_Clone (t_Clone). +(* File automatically generated by Hacspec *) +From Coq Require Import ZArith. +Import List.ListNotations. +Open Scope Z_scope. +Open Scope bool_scope. +Require Import String. + +From Core Require Import Core_Base_Int. +Export Core_Base_Int. + +From Core Require Import Core_Clone (t_Clone). +Export Core_Clone (t_Clone). + +Definition impl_9__ONE : t_HaxInt := 1%N. + +Definition impl_9__ZERO : t_HaxInt := 0%N. + +Definition v_BITS_128_ : t_HaxInt := 128%N. + +Definition v_BITS_16_ : t_HaxInt := 16%N. + +Definition v_BITS_32_ : t_HaxInt := 32%N. + +Definition v_BITS_64_ : t_HaxInt := 64%N. + +Definition v_BITS_8_ : t_HaxInt := 8%N. + +Definition v_WORDSIZE_128_ : t_HaxInt := N.pow 2 128. + +Definition v_WORDSIZE_128_SUB_1_ : t_HaxInt := (N.pow 2 128 - 1)%N. + +Definition v_WORDSIZE_16_ : t_HaxInt := N.pow 2 16. + +Definition v_WORDSIZE_16_SUB_1_ : t_HaxInt := (N.pow 2 16 - 1)%N. + +Definition v_WORDSIZE_32_ : t_HaxInt := N.pow 2 32. + +Definition v_WORDSIZE_32_SUB_1_ : t_HaxInt := (N.pow 2 32 - 1)%N. + +Definition v_WORDSIZE_64_ : t_HaxInt := N.pow 2 64. + +Definition v_WORDSIZE_64_SUB_1_ : t_HaxInt := (N.pow 2 64 - 1)%N. + +Definition v_WORDSIZE_8_ : t_HaxInt := N.pow 2 8. + +Definition v_WORDSIZE_8_SUB_1_ : t_HaxInt := (N.pow 2 8 - 1)%N. + +Instance t_Clone_599065907 : t_Clone (t_HaxInt) := + { + t_Clone_f_clone := fun (self : t_HaxInt) => self; + }. + +Definition impl_7__div2 (self : t_HaxInt) : t_HaxInt := N.div self 2. + +Definition impl_9__is_zero (self : t_HaxInt) : bool := match self with | N0 => true | _ => false end. + +Definition impl_9__pred (self : t_HaxInt) `{negb (impl_9__is_zero (self)) = true} : t_HaxInt := + N.pred self. + +Definition impl_9__succ (self : t_HaxInt) : t_HaxInt := + N.succ self. + +Instance t_Clone_793353639 : t_Clone (t_Positive) := + { + t_Clone_f_clone := fun (self : t_Positive) => + self; + }. + +Instance t_Clone_620939287 : t_Clone (t_Unary) := + { + t_Clone_f_clone := fun (self : t_Unary) => + self; + }. + +Definition impl_4__from_int (x : t_HaxInt) : t_Positive := + match x with | N0 => xH | Npos p => p end. + +Definition impl_4__to_int (self : t_Positive) : t_HaxInt := + Npos self. + +Definition impl_5__from_int (x : t_HaxInt) : t_Unary := + N.to_nat x. + +Definition impl_5__to_int (self : t_Unary) : t_HaxInt := + N.of_nat self. + +Definition impl_6__match_unary (self : t_Unary) : t_UNARY := + self. + +Definition impl_8__is_xH (self : t_Positive) : bool := + match self with xH => true | _ => false end. + +Definition impl_8__is_xI (self : t_Positive) : bool := + match self with xI _ => true | _ => false end. + +Definition impl_8__is_xO (self : t_Positive) : bool := + match self with xO _ => true | _ => false end. + +Definition impl_8__match_positive (self : t_Positive) : t_POSITIVE := + self. + +Definition impl_8__xH : t_Positive := + xH. + +Definition impl_8__xI (self : t_Positive) : t_Positive := + xI self. + +Definition impl_8__xO (self : t_Positive) : t_Positive := + xO self. + +Definition impl_9__match_pos (self : t_HaxInt) : t_POS := + if + impl_9__is_zero ((self)) + then + t_POS_POS_ZERO + else + t_POS_POS_POS (impl_4__from_int (self)). diff --git a/proof-libs/coq/coq/src/Core_Base_Int_Number_conversion.v b/proof-libs/coq/coq/src/Core_Base_Int_Number_conversion.v new file mode 100644 index 000000000..4f1df3ef3 --- /dev/null +++ b/proof-libs/coq/coq/src/Core_Base_Int_Number_conversion.v @@ -0,0 +1,80 @@ +(* File automatically generated by Hacspec *) +From Coq Require Import ZArith. +Import List.ListNotations. +Open Scope Z_scope. +Open Scope bool_scope. +Require Import String. + +From Core Require Import Core_Base_Int. +Export Core_Base_Int. + +From Core Require Import Core_Primitive. +Export Core_Primitive. + +From Core Require Import Core_Cmp. +Export Core_Cmp. + +From Core Require Import Core_Convert. +Export Core_Convert. + +(* NotImplementedYet *) + +Instance t_From_62544291 : t_From (t_HaxInt) (t_u8) := + { + t_From_f_from := fun (x : t_u8) => t_U8_f_v (t_u8_0 x); + }. + +Instance t_From_1006987144 : t_From (t_u8) (t_HaxInt) := + { + t_From_f_from := fun (x : t_HaxInt) => Build_t_u8 (Build_t_U8 x) + }. + +Instance t_From_1039663005 : t_From (t_HaxInt) (t_u16) := + { + t_From_f_from := fun (x : t_u16) => t_U16_f_v (t_u16_0 x); + }. + +Instance t_From_1052282100 : t_From (t_u16) (t_HaxInt) := + { + t_From_f_from := fun (x : t_HaxInt) => Build_t_u16 (Build_t_U16 x); + }. + +Instance t_From_529475850 : t_From (t_HaxInt) (t_u32) := + { + t_From_f_from := fun (x : t_u32) => t_U32_f_v (t_u32_0 x); + }. + +Instance t_From_447931916 : t_From (t_u32) (t_HaxInt) := + { + t_From_f_from := fun (x : t_HaxInt) => Build_t_u32 (Build_t_U32 x); + }. + +Instance t_From_616445870 : t_From (t_HaxInt) (t_u64) := + { + t_From_f_from := fun (x : t_u64) => t_U64_f_v (t_u64_0 x); + }. + +Instance t_From_70650389 : t_From (t_u64) (t_HaxInt) := + { + t_From_f_from := fun (x : t_HaxInt) => Build_t_u64 (Build_t_U64 x); + }. + +Instance t_From_184355489 : t_From (t_HaxInt) (t_u128) := + { + t_From_f_from := fun (x : t_u128) => t_U128_f_v (t_u128_0 x); + }. + +Instance t_From_844812452 : t_From (t_u128) (t_HaxInt) := + { + t_From_f_from := fun (x : t_HaxInt) => Build_t_u128 (Build_t_U128 x); + }. + +Instance t_From_946823391 : t_From (t_HaxInt) (t_usize) := + { + t_From_f_from := fun (x : t_usize) => t_U64_f_v (t_usize_0 x); + }. + +Instance t_From_655514338 : t_From (t_usize) (t_HaxInt) := + { + t_From_f_from := fun (x : t_HaxInt) => Build_t_usize (Build_t_U64 x); + }. diff --git a/proof-libs/coq/coq/src/Core_Base_Seq.v b/proof-libs/coq/coq/src/Core_Base_Seq.v new file mode 100644 index 000000000..a92c32d89 --- /dev/null +++ b/proof-libs/coq/coq/src/Core_Base_Seq.v @@ -0,0 +1,30 @@ +(* File automatically generated by Hacspec *) +From Coq Require Import ZArith. +Import List.ListNotations. +Open Scope Z_scope. +Open Scope bool_scope. +Require Import String. + +From Core Require Import Core_Clone (t_Clone). +Export Core_Clone (t_Clone). + +From Core Require Import Core_Cmp (t_PartialEq). +Export Core_Cmp (t_PartialEq). + +From Core Require Import Core_Marker (t_Sized). +Export Core_Marker (t_Sized). + +From Core Require Import Core_Base_Int. +Export Core_Base_Int. + +(* NotImplementedYet *) + +(* NotImplementedYet *) + +Definition t_Seq `{v_T : Type} `{t_Sized v_T} : Type := list v_T. +Arguments t_Seq:clear implicits. +Arguments t_Seq (_) {_}. + +Notation "'t_LIST'" := t_Seq. +Notation "'t_LIST_LIST_NIL'" := nil. +Notation "'t_LIST_LIST_CONS'" := cons. diff --git a/proof-libs/coq/coq/src/Core_Base_Seq_Base_impl.v b/proof-libs/coq/coq/src/Core_Base_Seq_Base_impl.v new file mode 100644 index 000000000..013f2e2e0 --- /dev/null +++ b/proof-libs/coq/coq/src/Core_Base_Seq_Base_impl.v @@ -0,0 +1,142 @@ +(* File automatically generated by Hacspec *) +From Coq Require Import ZArith. +Import List.ListNotations. +Open Scope Z_scope. +Open Scope bool_scope. +Require Import String. + + +From Core Require Import Core_Base_Seq. +Export Core_Base_Seq. + +From Core Require Import Core_Base_Seq_Base_spec. +Export Core_Base_Seq_Base_spec. + +From Core Require Import Core_Panicking. +Export Core_Panicking. + +From Core Require Import Core_Marker. +Export Core_Marker. + +From Core Require Import Core_Clone. +Export Core_Clone. + +From Core Require Import Core_Cmp. +Export Core_Cmp. + +From Core Require Import Core_Base_Int_Base_impl. +Export Core_Base_Int_Base_impl. + +Definition impl_2__is_empty `{v_T : Type} `{t_Sized v_T} `{t_Clone v_T} (self : t_Seq (v_T)) : bool := + match impl_1__match_list (self) with + | t_LIST_LIST_NIL => + true + | t_LIST_LIST_CONS (_) (_) => + false + end. + +Definition impl_2__tl `{v_T : Type} `{t_Sized v_T} `{t_Clone v_T} (self : t_Seq (v_T)) `{negb (impl_2__is_empty (self)) = true} : t_Seq (v_T) := + match impl_1__match_list (self) with + | t_LIST_LIST_NIL => + impl_1__NIL + | t_LIST_LIST_CONS (_) (tl) => + tl + end. + +Definition impl_2__hd__panic_cold_explicit (_ : unit) `{false = true} : t_Never := + panic_explicit (H := H) (tt). + +Definition impl_2__hd `{v_T : Type} `{t_Sized v_T} `{t_Clone v_T} (self : t_Seq (v_T)) `{negb (impl_2__is_empty (self)) = true} : v_T := + match impl_1__match_list (self) as k return negb (impl_2__is_empty k) = true -> _ with + | t_LIST_LIST_NIL => + fun F => + never_to_any (impl_2__hd__panic_cold_explicit (H := F) (tt)) + | t_LIST_LIST_CONS (hd) (_) => + fun _ => + hd + end H1. + +Definition impl_2__set_index__set_index_unary__panic_cold_explicit (_ : unit) `{false = true} : t_Never := + panic_explicit (H := H) (tt). + +Fixpoint impl__eq_inner `{v_T : Type} `{t_Sized v_T} `{t_Clone v_T} `{t_PartialEq v_T v_T} (self : t_Seq (v_T)) (other : t_Seq (v_T)) : bool := + match impl_1__match_list (t_Clone_f_clone (self)) with + | t_LIST_LIST_NIL => + impl_2__is_empty (t_Clone_f_clone (other)) + | t_LIST_LIST_CONS (x) (xs) => + match impl_1__match_list (t_Clone_f_clone (other)) with + | t_LIST_LIST_NIL => + false + | t_LIST_LIST_CONS (y) (ys) => + andb (t_PartialEq_f_eq (x) (y)) (impl__eq_inner (xs) (ys)) + end + end. + +Instance t_PartialEq_531240694 `{v_T : Type} `{t_Sized v_T} `{t_Clone v_T} `{t_PartialEq v_T v_T} : t_PartialEq (t_Seq (v_T)) (t_Seq (v_T)) := + { + t_PartialEq_f_eq := fun (self : t_Seq (v_T)) (other : t_Seq (v_T)) => + impl__eq_inner (self) (other); + t_PartialEq_f_ne := fun (self : t_Seq (v_T)) (other : t_Seq (v_T)) => + negb (impl__eq_inner (self) (other)); + }. + +Fixpoint impl_2__len `{v_T : Type} `{t_Sized v_T} `{t_Clone v_T} (self : t_Seq (v_T)) : t_HaxInt := + match impl_1__match_list (self) with + | t_LIST_LIST_NIL => + impl_9__ZERO + | t_LIST_LIST_CONS (_) (tl) => + impl_9__succ (impl_2__len (tl)) + end. + +Fixpoint impl_2__rev_accum `{v_T : Type} `{t_Sized v_T} `{t_Clone v_T} (self : t_Seq (v_T)) (accum : t_Seq (v_T)) : t_Seq (v_T) := + match impl_1__match_list (self) with + | t_LIST_LIST_NIL => + accum + | t_LIST_LIST_CONS (hd) (tl) => + impl_2__rev_accum (tl) (impl_1__cons (accum) (hd)) + end. + +Definition impl_2__rev `{v_T : Type} `{t_Sized v_T} `{t_Clone v_T} (self : t_Seq (v_T)) : t_Seq (v_T) := + impl_2__rev_accum (self) (impl_1__NIL). + +Program Fixpoint impl_2__get_index__get_index_unary `{v_T : Type} `{t_Sized v_T} `{t_Clone v_T} (l : t_Seq (v_T)) (i : t_Unary) `{t_PartialOrd_f_lt (impl_5__to_int i) ((impl_2__len (l))) = true} : v_T := + match impl_6__match_unary (i) with + | t_UNARY_UNARY_ZERO => + impl_2__hd (l) + | t_UNARY_UNARY_SUCC (n) => + impl_2__get_index__get_index_unary (impl_2__tl (l)) (n) + end. +Admit Obligations. + +Program Definition impl_2__get_index `{v_T : Type} `{t_Sized v_T} `{t_Clone v_T} (self : t_Seq (v_T)) (i : t_HaxInt) `{t_PartialOrd_f_lt (i) (impl_2__len (self)) = true} : v_T := + impl_2__get_index__get_index_unary (H1 := _) (self) (impl_5__from_int (i)). +Admit Obligations. + +Fixpoint impl_2__repeat__repeat_unary `{v_T : Type} `{t_Sized v_T} `{t_Clone v_T} (n : t_Unary) (v : v_T) : t_Seq (v_T) := + match impl_6__match_unary (n) with + | t_UNARY_UNARY_ZERO => + impl_1__NIL + | t_UNARY_UNARY_SUCC (m) => + impl_1__cons (impl_2__repeat__repeat_unary (m) (t_Clone_f_clone (v))) (v) + end. + +Definition impl_2__repeat `{v_T : Type} `{t_Sized v_T} `{t_Clone v_T} (n : t_HaxInt) (v : v_T) : t_Seq (v_T) := + impl_2__repeat__repeat_unary (impl_5__from_int (n)) (v). + +Program Fixpoint impl_2__set_index__set_index_unary `{v_T : Type} `{t_Sized v_T} `{t_Clone v_T} (x : t_Seq (v_T)) (i : t_Unary) (v : v_T) `{t_PartialOrd_f_lt (impl_5__to_int i) ((impl_2__len (x))) = true} : t_Seq (v_T) := + match impl_1__match_list (x) with + | t_LIST_LIST_NIL => + never_to_any (impl_2__set_index__set_index_unary__panic_cold_explicit (H := _) (tt)) + | t_LIST_LIST_CONS (hd) (tl) => + match impl_6__match_unary (i) with + | t_UNARY_UNARY_ZERO => + impl_1__cons (tl) (v) + | t_UNARY_UNARY_SUCC (n) => + impl_1__cons (impl_2__set_index__set_index_unary (tl) (n) (v)) (hd) + end + end. +Admit Obligations. + +Program Definition impl_2__set_index `{v_T : Type} `{t_Sized v_T} `{t_Clone v_T} (self : t_Seq (v_T)) (i : t_HaxInt) (v : v_T) `{t_PartialOrd_f_lt (i) (impl_2__len (self)) = true} : t_Seq (v_T) := + impl_2__set_index__set_index_unary (H1 := _) (self) (impl_5__from_int (i)) (v). +Admit Obligations. diff --git a/proof-libs/coq/coq/src/Core_Base_Seq_Base_spec.v b/proof-libs/coq/coq/src/Core_Base_Seq_Base_spec.v new file mode 100644 index 000000000..895d9f453 --- /dev/null +++ b/proof-libs/coq/coq/src/Core_Base_Seq_Base_spec.v @@ -0,0 +1,20 @@ +(* File automatically generated by Hacspec *) +From Coq Require Import ZArith. +Import List.ListNotations. +Open Scope Z_scope. +Open Scope bool_scope. +Require Import String. + +From Core Require Import Core_Base_Seq. +Export Core_Base_Seq. + +Instance t_Clone_528107485 `{v_T : Type} `{t_Sized v_T} `{t_Clone v_T} : t_Clone (t_Seq (v_T)) := + { + t_Clone_f_clone := fun (self : t_Seq (v_T)) => self; + }. + +Definition impl_1__NIL `{v_T : Type} `{t_Sized v_T} `{t_Clone v_T} : t_Seq (v_T) := nil. + +Definition impl_1__cons `{v_T : Type} `{t_Sized v_T} `{t_Clone v_T} (self : t_Seq (v_T)) (t : v_T) : t_Seq (v_T) := cons t self. + +Definition impl_1__match_list `{v_T : Type} `{t_Sized v_T} `{t_Clone v_T} (self : t_Seq (v_T)) : t_LIST (v_T) := self. diff --git a/proof-libs/coq/coq/src/Core_Clone.v b/proof-libs/coq/coq/src/Core_Clone.v new file mode 100644 index 000000000..020e2c3af --- /dev/null +++ b/proof-libs/coq/coq/src/Core_Clone.v @@ -0,0 +1,13 @@ +(* File automatically generated by Hacspec *) +From Coq Require Import ZArith. +Import List.ListNotations. +Open Scope Z_scope. +Open Scope bool_scope. +Require Import String. + +Class t_Clone `{v_Self : Type} : Type := + { + t_Clone_f_clone : v_Self -> v_Self; + }. +Arguments t_Clone:clear implicits. +Arguments t_Clone (_). diff --git a/proof-libs/coq/coq/src/Core_Cmp.v b/proof-libs/coq/coq/src/Core_Cmp.v new file mode 100644 index 000000000..a38506da5 --- /dev/null +++ b/proof-libs/coq/coq/src/Core_Cmp.v @@ -0,0 +1,165 @@ +(* File automatically generated by Hacspec *) +From Coq Require Import ZArith. +Import List.ListNotations. +Open Scope Z_scope. +Open Scope bool_scope. +Require Import String. + + +From Core Require Import Core_Option (t_Option). +Export Core_Option (t_Option). + +Definition discriminant_t_Ordering_Ordering_Equal := + 0%N. + +Definition discriminant_t_Ordering_Ordering_Greater := + 1%N. + +Inductive t_Ordering : Type := +| t_Ordering_Ordering_Less +| t_Ordering_Ordering_Equal +| t_Ordering_Ordering_Greater. +Arguments t_Ordering:clear implicits. +Arguments t_Ordering. + +Definition impl__Ordering__is_eq (self : t_Ordering) : bool := + match self with + | t_Ordering_Ordering_Equal => + true + | _ => + false + end. + +Definition impl__Ordering__is_gt (self : t_Ordering) : bool := + match self with + | t_Ordering_Ordering_Greater => + true + | _ => + false + end. + +Definition impl__Ordering__is_lt (self : t_Ordering) : bool := + match self with + | t_Ordering_Ordering_Less => + true + | _ => + false + end. + +Definition impl__Ordering__reverse (self : t_Ordering) : t_Ordering := + match self with + | t_Ordering_Ordering_Less => + t_Ordering_Ordering_Greater + | t_Ordering_Ordering_Equal => + t_Ordering_Ordering_Equal + | t_Ordering_Ordering_Greater => + t_Ordering_Ordering_Less + end. + +Definition discriminant_t_Ordering_Ordering_Less := + 1%N. + +Definition t_Ordering_cast_to_repr (x : t_Ordering) := + match x with + | t_Ordering_Ordering_Less => + discriminant_t_Ordering_Ordering_Less + | t_Ordering_Ordering_Equal => + discriminant_t_Ordering_Ordering_Equal + | t_Ordering_Ordering_Greater => + discriminant_t_Ordering_Ordering_Greater + end. + +Class t_PartialEq `{v_Self : Type} `{v_Rhs : Type} : Type := + { + t_PartialEq_f_eq : v_Self -> v_Rhs -> bool; + t_PartialEq_f_ne : v_Self -> v_Rhs -> bool; + }. +Arguments t_PartialEq:clear implicits. +Arguments t_PartialEq (_) (_). + +Definition impl__Ordering__is_ge (self : t_Ordering) : bool := + negb (match self with + | t_Ordering_Ordering_Less => + true + | _ => + false + end). + +Definition impl__Ordering__is_le (self : t_Ordering) : bool := + negb (match self with + | t_Ordering_Ordering_Greater => + true + | _ => + false + end). + +Definition impl__Ordering__is_ne (self : t_Ordering) : bool := + negb (match self with + | t_Ordering_Ordering_Equal => + true + | _ => + false + end). + +Instance t_PartialEq_322340293 : t_PartialEq (t_Ordering) (t_Ordering) := + { + t_PartialEq_f_eq := fun (self : t_Ordering) (other : t_Ordering) => + match self with + | t_Ordering_Ordering_Less => + match other with + | t_Ordering_Ordering_Less => + true + | _ => + false + end + | t_Ordering_Ordering_Equal => + match other with + | t_Ordering_Ordering_Equal => + true + | _ => + false + end + | t_Ordering_Ordering_Greater => + match other with + | t_Ordering_Ordering_Greater => + true + | _ => + false + end + end; + t_PartialEq_f_ne := fun (self : t_Ordering) (other : t_Ordering) => + negb (match self with + | t_Ordering_Ordering_Less => + match other with + | t_Ordering_Ordering_Less => + true + | _ => + false + end + | t_Ordering_Ordering_Equal => + match other with + | t_Ordering_Ordering_Equal => + true + | _ => + false + end + | t_Ordering_Ordering_Greater => + match other with + | t_Ordering_Ordering_Greater => + true + | _ => + false + end + end); + }. + +Class t_PartialOrd `{v_Self : Type} `{v_Rhs : Type} `{t_PartialEq v_Self v_Rhs} : Type := + { + t_PartialOrd_f_partial_cmp : v_Self -> v_Rhs -> t_Option (t_Ordering); + t_PartialOrd_f_lt : v_Self -> v_Rhs -> bool; + t_PartialOrd_f_le : v_Self -> v_Rhs -> bool; + t_PartialOrd_f_gt : v_Self -> v_Rhs -> bool; + t_PartialOrd_f_ge : v_Self -> v_Rhs -> bool; + }. +Arguments t_PartialOrd:clear implicits. +Arguments t_PartialOrd (_) (_) {_}. diff --git a/proof-libs/coq/coq/src/Core_Coerce.v b/proof-libs/coq/coq/src/Core_Coerce.v new file mode 100644 index 000000000..0c7d5730e --- /dev/null +++ b/proof-libs/coq/coq/src/Core_Coerce.v @@ -0,0 +1,21 @@ +(* File automatically generated by Hacspec *) +From Coq Require Import ZArith. +Import List.ListNotations. +Open Scope Z_scope. +Open Scope bool_scope. +Require Import String. + +Class t_Concretization `{v_Self : Type} `{v_T : Type} : Type := + { + t_Concretization_f_concretize : v_Self -> v_T; + }. +Arguments t_Concretization:clear implicits. +Arguments t_Concretization (_) (_). + +Class t_Abstraction `{v_Self : Type} : Type := + { + t_Abstraction_f_AbstractType : Type; + t_Abstraction_f_lift : v_Self -> t_Abstraction_f_AbstractType; + }. +Arguments t_Abstraction:clear implicits. +Arguments t_Abstraction (_). diff --git a/proof-libs/coq/coq/src/Core_Convert.v b/proof-libs/coq/coq/src/Core_Convert.v new file mode 100644 index 000000000..92e7f58d5 --- /dev/null +++ b/proof-libs/coq/coq/src/Core_Convert.v @@ -0,0 +1,32 @@ +(* File automatically generated by Hacspec *) +From Coq Require Import ZArith. +Import List.ListNotations. +Open Scope Z_scope. +Open Scope bool_scope. +Require Import String. + +Class t_From `{v_Self : Type} `{v_T : Type} : Type := + { + t_From_f_from : v_T -> v_Self; + }. +Arguments t_From:clear implicits. +Arguments t_From (_) (_). + +Instance t_From_888864539 `{v_T : Type} : t_From (v_T) (v_T) := + { + t_From_f_from := fun (t : v_T) => + t; + }. + +Class t_Into `{v_Self : Type} `{v_T : Type} : Type := + { + t_Into_f_into : v_Self -> v_T; + }. +Arguments t_Into:clear implicits. +Arguments t_Into (_) (_). + +Instance t_Into_28327994 `{v_T : Type} `{v_U : Type} `{t_From v_U v_T} : t_Into (v_T) (v_U) := + { + t_Into_f_into := fun (self : v_T) => + t_From_f_from (self); + }. diff --git a/proof-libs/coq/coq/src/Core_Int.v b/proof-libs/coq/coq/src/Core_Int.v new file mode 100644 index 000000000..1c9f74592 --- /dev/null +++ b/proof-libs/coq/coq/src/Core_Int.v @@ -0,0 +1,1321 @@ +(* File automatically generated by Hacspec *) +From Coq Require Import ZArith. +Import List.ListNotations. +Open Scope Z_scope. +Open Scope bool_scope. +Require Import String. + + +From Core Require Import Core_Marker. +Export Core_Marker. + +From Core Require Import Core_Ops_Arith. +Export Core_Ops_Arith. + +From Core Require Import Core_Ops_Bit. +Export Core_Ops_Bit. + + +From Core Require Import Core_Cmp. +Export Core_Cmp. + + +From Core Require Import Core_Base_Int_Base_spec. +Export Core_Base_Int_Base_spec. + +From Core Require Import Core_Base_Int_Base_impl. +Export Core_Base_Int_Base_impl. + + +From Core Require Import Core_Coerce. +Export Core_Coerce. + + +From Core Require Import Core_Option. +Export Core_Option. + +From Core Require Import Core_Clone. +Export Core_Clone. + +From Core Require Import Core_Convert. +Export Core_Convert. + +Class t_Constants `{v_Self : Type} : Type := + { + t_Constants_f_ZERO : v_Self; + t_Constants_f_ONE : v_Self; + t_Constants_f_MIN : v_Self; + t_Constants_f_MAX : v_Self; + }. +Arguments t_Constants:clear implicits. +Arguments t_Constants (_). + +(* NotImplementedYet *) + +(* NotImplementedYet *) + +(* NotImplementedYet *) + +(* NotImplementedYet *) + +(* NotImplementedYet *) + +(* NotImplementedYet *) + +(* NotImplementedYet *) + +(* NotImplementedYet *) + +(* NotImplementedYet *) + +(* NotImplementedYet *) + +(* NotImplementedYet *) + +(* NotImplementedYet *) + +(* NotImplementedYet *) + +(* NotImplementedYet *) + +(* NotImplementedYet *) + +Definition impl_21__WORDSIZE : t_HaxInt := + v_WORDSIZE_8_. + +Definition impl_48__WORDSIZE : t_HaxInt := + v_WORDSIZE_16_. + +Definition impl_75__WORDSIZE : t_HaxInt := + v_WORDSIZE_32_. + +Definition impl_102__WORDSIZE : t_HaxInt := + v_WORDSIZE_64_. + +Definition impl_129__WORDSIZE : t_HaxInt := + v_WORDSIZE_128_. + +Record t_U128 : Type := + { + t_U128_f_v : t_HaxInt + }. +Arguments t_U128:clear implicits. +Arguments t_U128. + +Instance t_Constants_262847618 : t_Constants (t_U128) := + { + t_Constants_f_ZERO := Build_t_U128 (impl_9__ZERO); + t_Constants_f_ONE := Build_t_U128 (impl_9__ONE); + t_Constants_f_MIN := Build_t_U128 (impl_9__ZERO); + t_Constants_f_MAX := Build_t_U128 (v_WORDSIZE_128_SUB_1_); + }. + +Instance t_Clone_864982688 : t_Clone (t_U128) := + { + t_Clone_f_clone := fun (self : t_U128) => + Build_t_U128 (t_Clone_f_clone (t_U128_f_v self)); + }. + +Record t_U16 : Type := + { + t_U16_f_v : t_HaxInt + }. +Arguments t_U16:clear implicits. +Arguments t_U16. + +Instance t_Constants_109024683 : t_Constants (t_U16) := + { + t_Constants_f_ZERO := Build_t_U16 (impl_9__ZERO); + t_Constants_f_ONE := Build_t_U16 (impl_9__ONE); + t_Constants_f_MIN := Build_t_U16 (impl_9__ZERO); + t_Constants_f_MAX := Build_t_U16 (v_WORDSIZE_16_SUB_1_); + }. + +Instance t_Clone_516308087 : t_Clone (t_U16) := + { + t_Clone_f_clone := fun (self : t_U16) => + Build_t_U16 (t_Clone_f_clone (t_U16_f_v self)); + }. + +Record t_U32 : Type := + { + t_U32_f_v : t_HaxInt + }. +Arguments t_U32:clear implicits. +Arguments t_U32. + +Definition impl_21__BITS : t_U32 := + Build_t_U32 (v_BITS_8_). + +Definition impl_48__BITS : t_U32 := + Build_t_U32 (v_BITS_16_). + +Instance t_Constants_516415142 : t_Constants (t_U32) := + { + t_Constants_f_ZERO := Build_t_U32 (impl_9__ZERO); + t_Constants_f_ONE := Build_t_U32 (impl_9__ONE); + t_Constants_f_MIN := Build_t_U32 (impl_9__ZERO); + t_Constants_f_MAX := Build_t_U32 (v_WORDSIZE_32_SUB_1_); + }. + +Definition impl_75__BITS : t_U32 := + Build_t_U32 (v_BITS_32_). + +Instance t_Clone_816356986 : t_Clone (t_U32) := + { + t_Clone_f_clone := fun (self : t_U32) => + Build_t_U32 (t_Clone_f_clone (t_U32_f_v self)); + }. + +Definition impl_102__BITS : t_U32 := + Build_t_U32 (v_BITS_64_). + +Definition impl_129__BITS : t_U32 := + Build_t_U32 (v_BITS_128_). + +Record t_U64 : Type := + { + t_U64_f_v : t_HaxInt + }. +Arguments t_U64:clear implicits. +Arguments t_U64. + +Instance t_Constants_576498638 : t_Constants (t_U64) := + { + t_Constants_f_ZERO := Build_t_U64 (impl_9__ZERO); + t_Constants_f_ONE := Build_t_U64 (impl_9__ONE); + t_Constants_f_MIN := Build_t_U64 (impl_9__ZERO); + t_Constants_f_MAX := Build_t_U64 (v_WORDSIZE_64_SUB_1_); + }. + +Instance t_Clone_899858620 : t_Clone (t_U64) := + { + t_Clone_f_clone := fun (self : t_U64) => + Build_t_U64 (t_Clone_f_clone (t_U64_f_v self)); + }. + +Record t_U8 : Type := + { + t_U8_f_v : t_HaxInt + }. +Arguments t_U8:clear implicits. +Arguments t_U8. + +Instance t_Constants_524257484 : t_Constants (t_U8) := + { + t_Constants_f_ZERO := Build_t_U8 (impl_9__ZERO); + t_Constants_f_ONE := Build_t_U8 (impl_9__ONE); + t_Constants_f_MIN := Build_t_U8 (impl_9__ZERO); + t_Constants_f_MAX := Build_t_U8 (v_WORDSIZE_8_SUB_1_); + }. + +Instance t_Clone_1016243736 : t_Clone (t_U8) := + { + t_Clone_f_clone := fun (self : t_U8) => + Build_t_U8 (t_Clone_f_clone (t_U8_f_v self)); + }. + +Instance t_Abstraction_566214702 : t_Abstraction (t_U8) := + { + t_Abstraction_f_AbstractType := t_HaxInt; + t_Abstraction_f_lift := fun (self : t_U8) => + t_U8_f_v self; + }. + +Instance t_PartialEq_118986006 : t_PartialEq (t_U8) (t_U8) := + { + t_PartialEq_f_eq := fun (self : t_U8) (rhs : t_U8) => + t_PartialEq_f_eq (t_PartialEq := t_PartialEq_822848086) (t_Abstraction_f_lift (t_Clone_f_clone (self))) (t_Abstraction_f_lift (t_Clone_f_clone (rhs))); + t_PartialEq_f_ne := fun (self : t_U8) (rhs : t_U8) => + negb (t_PartialEq_f_eq (t_PartialEq := t_PartialEq_822848086) (t_Abstraction_f_lift (t_Clone_f_clone (self))) (t_Abstraction_f_lift (t_Clone_f_clone (rhs)))); + }. + +Instance t_PartialOrd_672693761 : t_PartialOrd (t_U8) (t_U8) := + { + t_PartialOrd_f_partial_cmp := fun (self : t_U8) (rhs : t_U8) => + t_PartialOrd_f_partial_cmp (t_PartialOrd := t_PartialOrd_414924529) (t_Abstraction_f_lift (t_Clone_f_clone (self))) (t_Abstraction_f_lift (t_Clone_f_clone (rhs))); + t_PartialOrd_f_lt := fun (self : t_U8) (rhs : t_U8) => + match t_PartialOrd_f_partial_cmp (t_PartialOrd := t_PartialOrd_414924529) (t_Abstraction_f_lift (t_Clone_f_clone (self))) (t_Abstraction_f_lift (t_Clone_f_clone (rhs))) with + | t_Option_Option_Some (t_Ordering_Ordering_Less) => + true + | _ => + false + end; + t_PartialOrd_f_le := fun (self : t_U8) (rhs : t_U8) => + match t_PartialOrd_f_partial_cmp (t_PartialOrd := t_PartialOrd_414924529) (t_Abstraction_f_lift (t_Clone_f_clone (self))) (t_Abstraction_f_lift (t_Clone_f_clone (rhs))) with + | t_Option_Option_Some (t_Ordering_Ordering_Less + | t_Ordering_Ordering_Equal) => + true + | _ => + false + end; + t_PartialOrd_f_gt := fun (self : t_U8) (rhs : t_U8) => + match t_PartialOrd_f_partial_cmp (t_PartialOrd := t_PartialOrd_414924529) (t_Abstraction_f_lift (t_Clone_f_clone (self))) (t_Abstraction_f_lift (t_Clone_f_clone (rhs))) with + | t_Option_Option_Some (t_Ordering_Ordering_Greater) => + true + | _ => + false + end; + t_PartialOrd_f_ge := fun (self : t_U8) (rhs : t_U8) => + match t_PartialOrd_f_partial_cmp (t_PartialOrd := t_PartialOrd_414924529) (t_Abstraction_f_lift (t_Clone_f_clone (self))) (t_Abstraction_f_lift (t_Clone_f_clone (rhs))) with + | t_Option_Option_Some (t_Ordering_Ordering_Greater + | t_Ordering_Ordering_Equal) => + true + | _ => + false + end; + }. + +Instance t_Abstraction_134234872 : t_Abstraction (t_U16) := + { + t_Abstraction_f_AbstractType := t_HaxInt; + t_Abstraction_f_lift := fun (self : t_U16) => + t_U16_f_v self; + }. + +Instance t_PartialEq_712273567 : t_PartialEq (t_U16) (t_U16) := + { + t_PartialEq_f_eq := fun (self : t_U16) (rhs : t_U16) => + t_PartialEq_f_eq (t_PartialEq := t_PartialEq_822848086) (t_Abstraction_f_lift (t_Clone_f_clone (self))) (t_Abstraction_f_lift (t_Clone_f_clone (rhs))); + t_PartialEq_f_ne := fun (self : t_U16) (rhs : t_U16) => + negb (t_PartialEq_f_eq (t_PartialEq := t_PartialEq_822848086) (t_Abstraction_f_lift (t_Clone_f_clone (self))) (t_Abstraction_f_lift (t_Clone_f_clone (rhs)))); + }. + +Instance t_PartialOrd_17851967 : t_PartialOrd (t_U16) (t_U16) := + { + t_PartialOrd_f_partial_cmp := fun (self : t_U16) (rhs : t_U16) => + t_PartialOrd_f_partial_cmp (t_PartialOrd := t_PartialOrd_414924529) (t_Abstraction_f_lift (t_Clone_f_clone (self))) (t_Abstraction_f_lift (t_Clone_f_clone (rhs))); + t_PartialOrd_f_lt := fun (self : t_U16) (rhs : t_U16) => + match t_PartialOrd_f_partial_cmp (t_PartialOrd := t_PartialOrd_414924529) (t_Abstraction_f_lift (t_Clone_f_clone (self))) (t_Abstraction_f_lift (t_Clone_f_clone (rhs))) with + | t_Option_Option_Some (t_Ordering_Ordering_Less) => + true + | _ => + false + end; + t_PartialOrd_f_le := fun (self : t_U16) (rhs : t_U16) => + match t_PartialOrd_f_partial_cmp (t_PartialOrd := t_PartialOrd_414924529) (t_Abstraction_f_lift (t_Clone_f_clone (self))) (t_Abstraction_f_lift (t_Clone_f_clone (rhs))) with + | t_Option_Option_Some (t_Ordering_Ordering_Less + | t_Ordering_Ordering_Equal) => + true + | _ => + false + end; + t_PartialOrd_f_gt := fun (self : t_U16) (rhs : t_U16) => + match t_PartialOrd_f_partial_cmp (t_PartialOrd := t_PartialOrd_414924529) (t_Abstraction_f_lift (t_Clone_f_clone (self))) (t_Abstraction_f_lift (t_Clone_f_clone (rhs))) with + | t_Option_Option_Some (t_Ordering_Ordering_Greater) => + true + | _ => + false + end; + t_PartialOrd_f_ge := fun (self : t_U16) (rhs : t_U16) => + match t_PartialOrd_f_partial_cmp (t_PartialOrd := t_PartialOrd_414924529) (t_Abstraction_f_lift (t_Clone_f_clone (self))) (t_Abstraction_f_lift (t_Clone_f_clone (rhs))) with + | t_Option_Option_Some (t_Ordering_Ordering_Greater + | t_Ordering_Ordering_Equal) => + true + | _ => + false + end; + }. + +Instance t_Abstraction_699270934 : t_Abstraction (t_U32) := + { + t_Abstraction_f_AbstractType := t_HaxInt; + t_Abstraction_f_lift := fun (self : t_U32) => + t_U32_f_v self; + }. + +Instance t_PartialEq_334097439 : t_PartialEq (t_U32) (t_U32) := + { + t_PartialEq_f_eq := fun (self : t_U32) (rhs : t_U32) => + t_PartialEq_f_eq (t_PartialEq := t_PartialEq_822848086) (t_Abstraction_f_lift (t_Clone_f_clone (self))) (t_Abstraction_f_lift (t_Clone_f_clone (rhs))); + t_PartialEq_f_ne := fun (self : t_U32) (rhs : t_U32) => + negb (t_PartialEq_f_eq (t_PartialEq := t_PartialEq_822848086) (t_Abstraction_f_lift (t_Clone_f_clone (self))) (t_Abstraction_f_lift (t_Clone_f_clone (rhs)))); + }. + +Instance t_PartialOrd_768426650 : t_PartialOrd (t_U32) (t_U32) := + { + t_PartialOrd_f_partial_cmp := fun (self : t_U32) (rhs : t_U32) => + t_PartialOrd_f_partial_cmp (t_PartialOrd := t_PartialOrd_414924529) (t_Abstraction_f_lift (t_Clone_f_clone (self))) (t_Abstraction_f_lift (t_Clone_f_clone (rhs))); + t_PartialOrd_f_lt := fun (self : t_U32) (rhs : t_U32) => + match t_PartialOrd_f_partial_cmp (t_PartialOrd := t_PartialOrd_414924529) (t_Abstraction_f_lift (t_Clone_f_clone (self))) (t_Abstraction_f_lift (t_Clone_f_clone (rhs))) with + | t_Option_Option_Some (t_Ordering_Ordering_Less) => + true + | _ => + false + end; + t_PartialOrd_f_le := fun (self : t_U32) (rhs : t_U32) => + match t_PartialOrd_f_partial_cmp (t_PartialOrd := t_PartialOrd_414924529) (t_Abstraction_f_lift (t_Clone_f_clone (self))) (t_Abstraction_f_lift (t_Clone_f_clone (rhs))) with + | t_Option_Option_Some (t_Ordering_Ordering_Less + | t_Ordering_Ordering_Equal) => + true + | _ => + false + end; + t_PartialOrd_f_gt := fun (self : t_U32) (rhs : t_U32) => + match t_PartialOrd_f_partial_cmp (t_PartialOrd := t_PartialOrd_414924529) (t_Abstraction_f_lift (t_Clone_f_clone (self))) (t_Abstraction_f_lift (t_Clone_f_clone (rhs))) with + | t_Option_Option_Some (t_Ordering_Ordering_Greater) => + true + | _ => + false + end; + t_PartialOrd_f_ge := fun (self : t_U32) (rhs : t_U32) => + match t_PartialOrd_f_partial_cmp (t_PartialOrd := t_PartialOrd_414924529) (t_Abstraction_f_lift (t_Clone_f_clone (self))) (t_Abstraction_f_lift (t_Clone_f_clone (rhs))) with + | t_Option_Option_Some (t_Ordering_Ordering_Greater + | t_Ordering_Ordering_Equal) => + true + | _ => + false + end; + }. + +Instance t_Abstraction_374630185 : t_Abstraction (t_U64) := + { + t_Abstraction_f_AbstractType := t_HaxInt; + t_Abstraction_f_lift := fun (self : t_U64) => + t_U64_f_v self; + }. + +Instance t_PartialEq_164055385 : t_PartialEq (t_U64) (t_U64) := + { + t_PartialEq_f_eq := fun (self : t_U64) (rhs : t_U64) => + t_PartialEq_f_eq (t_PartialEq := t_PartialEq_822848086) (t_Abstraction_f_lift (t_Clone_f_clone (self))) (t_Abstraction_f_lift (t_Clone_f_clone (rhs))); + t_PartialEq_f_ne := fun (self : t_U64) (rhs : t_U64) => + negb (t_PartialEq_f_eq (t_PartialEq := t_PartialEq_822848086) (t_Abstraction_f_lift (t_Clone_f_clone (self))) (t_Abstraction_f_lift (t_Clone_f_clone (rhs)))); + }. + +Instance t_PartialOrd_565848459 : t_PartialOrd (t_U64) (t_U64) := + { + t_PartialOrd_f_partial_cmp := fun (self : t_U64) (rhs : t_U64) => + t_PartialOrd_f_partial_cmp (t_PartialOrd := t_PartialOrd_414924529) (t_Abstraction_f_lift (t_Clone_f_clone (self))) (t_Abstraction_f_lift (t_Clone_f_clone (rhs))); + t_PartialOrd_f_lt := fun (self : t_U64) (rhs : t_U64) => + match t_PartialOrd_f_partial_cmp (t_PartialOrd := t_PartialOrd_414924529) (t_Abstraction_f_lift (t_Clone_f_clone (self))) (t_Abstraction_f_lift (t_Clone_f_clone (rhs))) with + | t_Option_Option_Some (t_Ordering_Ordering_Less) => + true + | _ => + false + end; + t_PartialOrd_f_le := fun (self : t_U64) (rhs : t_U64) => + match t_PartialOrd_f_partial_cmp (t_PartialOrd := t_PartialOrd_414924529) (t_Abstraction_f_lift (t_Clone_f_clone (self))) (t_Abstraction_f_lift (t_Clone_f_clone (rhs))) with + | t_Option_Option_Some (t_Ordering_Ordering_Less + | t_Ordering_Ordering_Equal) => + true + | _ => + false + end; + t_PartialOrd_f_gt := fun (self : t_U64) (rhs : t_U64) => + match t_PartialOrd_f_partial_cmp (t_PartialOrd := t_PartialOrd_414924529) (t_Abstraction_f_lift (t_Clone_f_clone (self))) (t_Abstraction_f_lift (t_Clone_f_clone (rhs))) with + | t_Option_Option_Some (t_Ordering_Ordering_Greater) => + true + | _ => + false + end; + t_PartialOrd_f_ge := fun (self : t_U64) (rhs : t_U64) => + match t_PartialOrd_f_partial_cmp (t_PartialOrd := t_PartialOrd_414924529) (t_Abstraction_f_lift (t_Clone_f_clone (self))) (t_Abstraction_f_lift (t_Clone_f_clone (rhs))) with + | t_Option_Option_Some (t_Ordering_Ordering_Greater + | t_Ordering_Ordering_Equal) => + true + | _ => + false + end; + }. + +Instance t_Abstraction_462669591 : t_Abstraction (t_U128) := + { + t_Abstraction_f_AbstractType := t_HaxInt; + t_Abstraction_f_lift := fun (self : t_U128) => + t_U128_f_v self; + }. + +Instance t_PartialEq_1056014937 : t_PartialEq (t_U128) (t_U128) := + { + t_PartialEq_f_eq := fun (self : t_U128) (rhs : t_U128) => + t_PartialEq_f_eq (t_PartialEq := t_PartialEq_822848086) (t_Abstraction_f_lift (t_Clone_f_clone (self))) (t_Abstraction_f_lift (t_Clone_f_clone (rhs))); + t_PartialEq_f_ne := fun (self : t_U128) (rhs : t_U128) => + negb (t_PartialEq_f_eq (t_PartialEq := t_PartialEq_822848086) (t_Abstraction_f_lift (t_Clone_f_clone (self))) (t_Abstraction_f_lift (t_Clone_f_clone (rhs)))); + }. + +Instance t_PartialOrd_967097068 : t_PartialOrd (t_U128) (t_U128) := + { + t_PartialOrd_f_partial_cmp := fun (self : t_U128) (rhs : t_U128) => + t_PartialOrd_f_partial_cmp (t_PartialOrd := t_PartialOrd_414924529) (t_Abstraction_f_lift (t_Clone_f_clone (self))) (t_Abstraction_f_lift (t_Clone_f_clone (rhs))); + t_PartialOrd_f_lt := fun (self : t_U128) (rhs : t_U128) => + match t_PartialOrd_f_partial_cmp (t_PartialOrd := t_PartialOrd_414924529) (t_Abstraction_f_lift (t_Clone_f_clone (self))) (t_Abstraction_f_lift (t_Clone_f_clone (rhs))) with + | t_Option_Option_Some (t_Ordering_Ordering_Less) => + true + | _ => + false + end; + t_PartialOrd_f_le := fun (self : t_U128) (rhs : t_U128) => + match t_PartialOrd_f_partial_cmp (t_PartialOrd := t_PartialOrd_414924529) (t_Abstraction_f_lift (t_Clone_f_clone (self))) (t_Abstraction_f_lift (t_Clone_f_clone (rhs))) with + | t_Option_Option_Some (t_Ordering_Ordering_Less + | t_Ordering_Ordering_Equal) => + true + | _ => + false + end; + t_PartialOrd_f_gt := fun (self : t_U128) (rhs : t_U128) => + match t_PartialOrd_f_partial_cmp (t_PartialOrd := t_PartialOrd_414924529) (t_Abstraction_f_lift (t_Clone_f_clone (self))) (t_Abstraction_f_lift (t_Clone_f_clone (rhs))) with + | t_Option_Option_Some (t_Ordering_Ordering_Greater) => + true + | _ => + false + end; + t_PartialOrd_f_ge := fun (self : t_U128) (rhs : t_U128) => + match t_PartialOrd_f_partial_cmp (t_PartialOrd := t_PartialOrd_414924529) (t_Abstraction_f_lift (t_Clone_f_clone (self))) (t_Abstraction_f_lift (t_Clone_f_clone (rhs))) with + | t_Option_Option_Some (t_Ordering_Ordering_Greater + | t_Ordering_Ordering_Equal) => + true + | _ => + false + end; + }. + +Instance t_Concretization_265873841 : t_Concretization (t_HaxInt) (t_U8) := + { + t_Concretization_f_concretize := fun (self : t_HaxInt) => + Build_t_U8 (impl_10__rem (self) (v_WORDSIZE_8_)); + }. + +Instance t_From_51944146 : t_From (t_U8) (t_U16) := + { + t_From_f_from := fun (x : t_U16) => + t_Concretization_f_concretize (t_Abstraction_f_lift (x) : t_HaxInt); + }. + +Instance t_From_1017513021 : t_From (t_U8) (t_U32) := + { + t_From_f_from := fun (x : t_U32) => + t_Concretization_f_concretize (t_Abstraction_f_lift (x) : t_HaxInt); + }. + +Instance t_From_23951205 : t_From (t_U8) (t_U64) := + { + t_From_f_from := fun (x : t_U64) => + t_Concretization_f_concretize (t_Abstraction_f_lift (x) : t_HaxInt); + }. + +Instance t_From_800503147 : t_From (t_U8) (t_U128) := + { + t_From_f_from := fun (x : t_U128) => + t_Concretization_f_concretize (t_Abstraction_f_lift (x) : t_HaxInt); + }. + +Instance t_Concretization_369613743 : t_Concretization (t_HaxInt) (t_U16) := + { + t_Concretization_f_concretize := fun (self : t_HaxInt) => + Build_t_U16 (impl_10__rem (self) (v_WORDSIZE_16_)); + }. + +Instance t_From_926291537 : t_From (t_U16) (t_U8) := + { + t_From_f_from := fun (x : t_U8) => + t_Concretization_f_concretize (t_Abstraction_f_lift (x) : t_HaxInt); + }. + +Instance t_From_784540441 : t_From (t_U16) (t_U32) := + { + t_From_f_from := fun (x : t_U32) => + t_Concretization_f_concretize (t_Abstraction_f_lift (x) : t_HaxInt); + }. + +Instance t_From_426489148 : t_From (t_U16) (t_U64) := + { + t_From_f_from := fun (x : t_U64) => + t_Concretization_f_concretize (t_Abstraction_f_lift (x) : t_HaxInt); + }. + +Instance t_From_948759743 : t_From (t_U16) (t_U128) := + { + t_From_f_from := fun (x : t_U128) => + t_Concretization_f_concretize (t_Abstraction_f_lift (x) : t_HaxInt); + }. + +Instance t_Concretization_34651280 : t_Concretization (t_HaxInt) (t_U32) := + { + t_Concretization_f_concretize := fun (self : t_HaxInt) => + Build_t_U32 (impl_10__rem (self) (v_WORDSIZE_32_)); + }. + +Instance t_From_35635710 : t_From (t_U32) (t_U8) := + { + t_From_f_from := fun (x : t_U8) => + t_Concretization_f_concretize (t_Abstraction_f_lift (x) : t_HaxInt); + }. + +Instance t_From_487860229 : t_From (t_U32) (t_U16) := + { + t_From_f_from := fun (x : t_U16) => + t_Concretization_f_concretize (t_Abstraction_f_lift (x) : t_HaxInt); + }. + +Instance t_From_726835366 : t_From (t_U32) (t_U64) := + { + t_From_f_from := fun (x : t_U64) => + t_Concretization_f_concretize (t_Abstraction_f_lift (x) : t_HaxInt); + }. + +Instance t_From_452621038 : t_From (t_U32) (t_U128) := + { + t_From_f_from := fun (x : t_U128) => + t_Concretization_f_concretize (t_Abstraction_f_lift (x) : t_HaxInt); + }. + +Instance t_Concretization_841277766 : t_Concretization (t_HaxInt) (t_U64) := + { + t_Concretization_f_concretize := fun (self : t_HaxInt) => + Build_t_U64 (impl_10__rem (self) (v_WORDSIZE_64_)); + }. + +Instance t_From_520130596 : t_From (t_U64) (t_U8) := + { + t_From_f_from := fun (x : t_U8) => + t_Concretization_f_concretize (t_Abstraction_f_lift (x) : t_HaxInt); + }. + +Instance t_From_627850588 : t_From (t_U64) (t_U16) := + { + t_From_f_from := fun (x : t_U16) => + t_Concretization_f_concretize (t_Abstraction_f_lift (x) : t_HaxInt); + }. + +Instance t_From_184030199 : t_From (t_U64) (t_U32) := + { + t_From_f_from := fun (x : t_U32) => + t_Concretization_f_concretize (t_Abstraction_f_lift (x) : t_HaxInt); + }. + +Instance t_From_203853320 : t_From (t_U64) (t_U128) := + { + t_From_f_from := fun (x : t_U128) => + t_Concretization_f_concretize (t_Abstraction_f_lift (x) : t_HaxInt); + }. + +Instance t_Concretization_814811766 : t_Concretization (t_HaxInt) (t_U128) := + { + t_Concretization_f_concretize := fun (self : t_HaxInt) => + Build_t_U128 (impl_10__rem (self) (v_WORDSIZE_128_)); + }. + +Instance t_From_473330350 : t_From (t_U128) (t_U8) := + { + t_From_f_from := fun (x : t_U8) => + t_Concretization_f_concretize (t_Abstraction_f_lift (x) : t_HaxInt); + }. + +Instance t_From_119329024 : t_From (t_U128) (t_U16) := + { + t_From_f_from := fun (x : t_U16) => + t_Concretization_f_concretize (t_Abstraction_f_lift (x) : t_HaxInt); + }. + +Instance t_From_763371499 : t_From (t_U128) (t_U32) := + { + t_From_f_from := fun (x : t_U32) => + t_Concretization_f_concretize (t_Abstraction_f_lift (x) : t_HaxInt); + }. + +Instance t_From_576231031 : t_From (t_U128) (t_U64) := + { + t_From_f_from := fun (x : t_U64) => + t_Concretization_f_concretize (t_Abstraction_f_lift (x) : t_HaxInt); + }. + +Instance t_Neg_351404352 : t_Neg (t_U8) := + { + t_Neg_f_Output := t_U8; + t_Neg_f_neg := fun (self : t_U8) => + t_Concretization_f_concretize (t_Concretization := t_Concretization_265873841) (impl_7__sub (v_WORDSIZE_8_) (impl_10__rem (t_Abstraction_f_lift (self)) (v_WORDSIZE_8_))); + }. + +Instance t_Mul_960114544 : t_Mul (t_U8) (t_U8) := + { + t_Mul_f_Output := t_U8; + t_Mul_f_mul := fun (self : t_U8) (rhs : t_U8) => + t_Concretization_f_concretize (t_Concretization := t_Concretization_265873841) (impl_11__mul (t_Abstraction_f_lift (self)) (t_Abstraction_f_lift (rhs))); + }. + +Instance t_Rem_707040129 : t_Rem (t_U8) (t_U8) := + { + t_Rem_f_Output := t_U8; + t_Rem_f_rem := fun (self : t_U8) (rhs : t_U8) => + t_Concretization_f_concretize (t_Concretization := t_Concretization_265873841) (impl_10__rem (t_Abstraction_f_lift (self)) (t_Abstraction_f_lift (rhs))); + }. + +Instance t_Add_121545721 : t_Add (t_U8) (t_U8) := + { + t_Add_f_Output := t_U8; + t_Add_f_add := fun (self : t_U8) (rhs : t_U8) => + t_Concretization_f_concretize (t_Concretization := t_Concretization_265873841) (impl_6__add (t_Abstraction_f_lift (self)) (t_Abstraction_f_lift (rhs))); + }. + +Instance t_Div_98187967 : t_Div (t_U8) (t_U8) := + { + t_Div_f_Output := t_U8; + t_Div_f_div := fun (self : t_U8) (rhs : t_U8) => + t_Concretization_f_concretize (t_Concretization := t_Concretization_265873841) (impl_10__div (t_Abstraction_f_lift (self)) (t_Abstraction_f_lift (rhs))); + }. + +Instance t_Shl_377719001 : t_Shl (t_U8) (t_U8) := + { + t_Shl_f_Output := t_U8; + t_Shl_f_shl := fun (self : t_U8) (rhs : t_U8) => + t_Concretization_f_concretize (t_Concretization := t_Concretization_265873841) (impl_12__shl (t_Abstraction_f_lift (self)) (t_Abstraction_f_lift (rhs))); + }. + +Instance t_Shl_251987868 : t_Shl (t_U8) (t_U16) := + { + t_Shl_f_Output := t_U8; + t_Shl_f_shl := fun (self : t_U8) (rhs : t_U16) => + t_Concretization_f_concretize (t_Concretization := t_Concretization_265873841) (impl_12__shl (t_Abstraction_f_lift (self)) (t_Abstraction_f_lift (rhs))); + }. + +Instance t_Shl_1004268259 : t_Shl (t_U8) (t_U32) := + { + t_Shl_f_Output := t_U8; + t_Shl_f_shl := fun (self : t_U8) (rhs : t_U32) => + t_Concretization_f_concretize (t_Concretization := t_Concretization_265873841) (impl_12__shl (t_Abstraction_f_lift (self)) (t_Abstraction_f_lift (rhs))); + }. + +Instance t_Shl_400796854 : t_Shl (t_U8) (t_U64) := + { + t_Shl_f_Output := t_U8; + t_Shl_f_shl := fun (self : t_U8) (rhs : t_U64) => + t_Concretization_f_concretize (t_Concretization := t_Concretization_265873841) (impl_12__shl (t_Abstraction_f_lift (self)) (t_Abstraction_f_lift (rhs))); + }. + +Instance t_Shl_79328015 : t_Shl (t_U8) (t_U128) := + { + t_Shl_f_Output := t_U8; + t_Shl_f_shl := fun (self : t_U8) (rhs : t_U128) => + t_Concretization_f_concretize (t_Concretization := t_Concretization_265873841) (impl_12__shl (t_Abstraction_f_lift (self)) (t_Abstraction_f_lift (rhs))); + }. + +Instance t_Shr_319870959 : t_Shr (t_U8) (t_U8) := + { + t_Shr_f_Output := t_U8; + t_Shr_f_shr := fun (self : t_U8) (rhs : t_U8) => + t_Concretization_f_concretize (t_Concretization := t_Concretization_265873841) (impl_13__shr (t_Abstraction_f_lift (self)) (t_Abstraction_f_lift (rhs))); + }. + +Instance t_Shr_879984593 : t_Shr (t_U8) (t_U16) := + { + t_Shr_f_Output := t_U8; + t_Shr_f_shr := fun (self : t_U8) (rhs : t_U16) => + t_Concretization_f_concretize (t_Concretization := t_Concretization_265873841) (impl_13__shr (t_Abstraction_f_lift (self)) (t_Abstraction_f_lift (rhs))); + }. + +Instance t_Shr_88869181 : t_Shr (t_U8) (t_U32) := + { + t_Shr_f_Output := t_U8; + t_Shr_f_shr := fun (self : t_U8) (rhs : t_U32) => + t_Concretization_f_concretize (t_Concretization := t_Concretization_265873841) (impl_13__shr (t_Abstraction_f_lift (self)) (t_Abstraction_f_lift (rhs))); + }. + +Instance t_Shr_77214537 : t_Shr (t_U8) (t_U64) := + { + t_Shr_f_Output := t_U8; + t_Shr_f_shr := fun (self : t_U8) (rhs : t_U64) => + t_Concretization_f_concretize (t_Concretization := t_Concretization_265873841) (impl_13__shr (t_Abstraction_f_lift (self)) (t_Abstraction_f_lift (rhs))); + }. + +Instance t_Shr_346939843 : t_Shr (t_U8) (t_U128) := + { + t_Shr_f_Output := t_U8; + t_Shr_f_shr := fun (self : t_U8) (rhs : t_U128) => + t_Concretization_f_concretize (t_Concretization := t_Concretization_265873841) (impl_13__shr (t_Abstraction_f_lift (self)) (t_Abstraction_f_lift (rhs))); + }. + +Instance t_BitXor_428151757 : t_BitXor (t_U8) (t_U8) := + { + t_BitXor_f_Output := t_U8; + t_BitXor_f_bitxor := fun (self : t_U8) (rhs : t_U8) => + t_Concretization_f_concretize (t_Concretization := t_Concretization_265873841) (impl_14__bitxor (t_Abstraction_f_lift (self)) (t_Abstraction_f_lift (rhs))); + }. + +Instance t_BitAnd_719505946 : t_BitAnd (t_U8) (t_U8) := + { + t_BitAnd_f_Output := t_U8; + t_BitAnd_f_bitand := fun (self : t_U8) (rhs : t_U8) => + t_Concretization_f_concretize (t_Concretization := t_Concretization_265873841) (impl_15__bitand (t_Abstraction_f_lift (self)) (t_Abstraction_f_lift (rhs))); + }. + +Instance t_BitOr_516494164 : t_BitOr (t_U8) (t_U8) := + { + t_BitOr_f_Output := t_U8; + t_BitOr_f_bitor := fun (self : t_U8) (rhs : t_U8) => + t_Concretization_f_concretize (t_Concretization := t_Concretization_265873841) (impl_16__bitor (t_Abstraction_f_lift (self)) (t_Abstraction_f_lift (rhs))); + }. + +Instance t_Neg_758687224 : t_Neg (t_U16) := + { + t_Neg_f_Output := t_U16; + t_Neg_f_neg := fun (self : t_U16) => + t_Concretization_f_concretize (t_Concretization := t_Concretization_369613743) (impl_7__sub (v_WORDSIZE_16_) (impl_10__rem (t_Abstraction_f_lift (self)) (v_WORDSIZE_16_))); + }. + +Instance t_Mul_467924553 : t_Mul (t_U16) (t_U16) := + { + t_Mul_f_Output := t_U16; + t_Mul_f_mul := fun (self : t_U16) (rhs : t_U16) => + t_Concretization_f_concretize (t_Concretization := t_Concretization_369613743) (impl_11__mul (t_Abstraction_f_lift (self)) (t_Abstraction_f_lift (rhs))); + }. + +Instance t_Rem_333671536 : t_Rem (t_U16) (t_U16) := + { + t_Rem_f_Output := t_U16; + t_Rem_f_rem := fun (self : t_U16) (rhs : t_U16) => + t_Concretization_f_concretize (t_Concretization := t_Concretization_369613743) (impl_10__rem (t_Abstraction_f_lift (self)) (t_Abstraction_f_lift (rhs))); + }. + +Instance t_Add_71250682 : t_Add (t_U16) (t_U16) := + { + t_Add_f_Output := t_U16; + t_Add_f_add := fun (self : t_U16) (rhs : t_U16) => + t_Concretization_f_concretize (t_Concretization := t_Concretization_369613743) (impl_6__add (t_Abstraction_f_lift (self)) (t_Abstraction_f_lift (rhs))); + }. + +Instance t_Div_638997407 : t_Div (t_U16) (t_U16) := + { + t_Div_f_Output := t_U16; + t_Div_f_div := fun (self : t_U16) (rhs : t_U16) => + t_Concretization_f_concretize (t_Concretization := t_Concretization_369613743) (impl_10__div (t_Abstraction_f_lift (self)) (t_Abstraction_f_lift (rhs))); + }. + +Instance t_Shl_189335836 : t_Shl (t_U16) (t_U8) := + { + t_Shl_f_Output := t_U16; + t_Shl_f_shl := fun (self : t_U16) (rhs : t_U8) => + t_Concretization_f_concretize (t_Concretization := t_Concretization_369613743) (impl_12__shl (t_Abstraction_f_lift (self)) (t_Abstraction_f_lift (rhs))); + }. + +Instance t_Shl_400009554 : t_Shl (t_U16) (t_U16) := + { + t_Shl_f_Output := t_U16; + t_Shl_f_shl := fun (self : t_U16) (rhs : t_U16) => + t_Concretization_f_concretize (t_Concretization := t_Concretization_369613743) (impl_12__shl (t_Abstraction_f_lift (self)) (t_Abstraction_f_lift (rhs))); + }. + +Instance t_Shl_40960466 : t_Shl (t_U16) (t_U32) := + { + t_Shl_f_Output := t_U16; + t_Shl_f_shl := fun (self : t_U16) (rhs : t_U32) => + t_Concretization_f_concretize (t_Concretization := t_Concretization_369613743) (impl_12__shl (t_Abstraction_f_lift (self)) (t_Abstraction_f_lift (rhs))); + }. + +Instance t_Shl_472600731 : t_Shl (t_U16) (t_U64) := + { + t_Shl_f_Output := t_U16; + t_Shl_f_shl := fun (self : t_U16) (rhs : t_U64) => + t_Concretization_f_concretize (t_Concretization := t_Concretization_369613743) (impl_12__shl (t_Abstraction_f_lift (self)) (t_Abstraction_f_lift (rhs))); + }. + +Instance t_Shl_114665376 : t_Shl (t_U16) (t_U128) := + { + t_Shl_f_Output := t_U16; + t_Shl_f_shl := fun (self : t_U16) (rhs : t_U128) => + t_Concretization_f_concretize (t_Concretization := t_Concretization_369613743) (impl_12__shl (t_Abstraction_f_lift (self)) (t_Abstraction_f_lift (rhs))); + }. + +Instance t_Shr_327818009 : t_Shr (t_U16) (t_U8) := + { + t_Shr_f_Output := t_U16; + t_Shr_f_shr := fun (self : t_U16) (rhs : t_U8) => + t_Concretization_f_concretize (t_Concretization := t_Concretization_369613743) (impl_13__shr (t_Abstraction_f_lift (self)) (t_Abstraction_f_lift (rhs))); + }. + +Instance t_Shr_212310233 : t_Shr (t_U16) (t_U16) := + { + t_Shr_f_Output := t_U16; + t_Shr_f_shr := fun (self : t_U16) (rhs : t_U16) => + t_Concretization_f_concretize (t_Concretization := t_Concretization_369613743) (impl_13__shr (t_Abstraction_f_lift (self)) (t_Abstraction_f_lift (rhs))); + }. + +Instance t_Shr_591081376 : t_Shr (t_U16) (t_U32) := + { + t_Shr_f_Output := t_U16; + t_Shr_f_shr := fun (self : t_U16) (rhs : t_U32) => + t_Concretization_f_concretize (t_Concretization := t_Concretization_369613743) (impl_13__shr (t_Abstraction_f_lift (self)) (t_Abstraction_f_lift (rhs))); + }. + +Instance t_Shr_428437762 : t_Shr (t_U16) (t_U64) := + { + t_Shr_f_Output := t_U16; + t_Shr_f_shr := fun (self : t_U16) (rhs : t_U64) => + t_Concretization_f_concretize (t_Concretization := t_Concretization_369613743) (impl_13__shr (t_Abstraction_f_lift (self)) (t_Abstraction_f_lift (rhs))); + }. + +Instance t_Shr_847453429 : t_Shr (t_U16) (t_U128) := + { + t_Shr_f_Output := t_U16; + t_Shr_f_shr := fun (self : t_U16) (rhs : t_U128) => + t_Concretization_f_concretize (t_Concretization := t_Concretization_369613743) (impl_13__shr (t_Abstraction_f_lift (self)) (t_Abstraction_f_lift (rhs))); + }. + +Instance t_BitXor_448510460 : t_BitXor (t_U16) (t_U16) := + { + t_BitXor_f_Output := t_U16; + t_BitXor_f_bitxor := fun (self : t_U16) (rhs : t_U16) => + t_Concretization_f_concretize (t_Concretization := t_Concretization_369613743) (impl_14__bitxor (t_Abstraction_f_lift (self)) (t_Abstraction_f_lift (rhs))); + }. + +Instance t_BitAnd_493952949 : t_BitAnd (t_U16) (t_U16) := + { + t_BitAnd_f_Output := t_U16; + t_BitAnd_f_bitand := fun (self : t_U16) (rhs : t_U16) => + t_Concretization_f_concretize (t_Concretization := t_Concretization_369613743) (impl_15__bitand (t_Abstraction_f_lift (self)) (t_Abstraction_f_lift (rhs))); + }. + +Instance t_BitOr_196126415 : t_BitOr (t_U16) (t_U16) := + { + t_BitOr_f_Output := t_U16; + t_BitOr_f_bitor := fun (self : t_U16) (rhs : t_U16) => + t_Concretization_f_concretize (t_Concretization := t_Concretization_369613743) (impl_16__bitor (t_Abstraction_f_lift (self)) (t_Abstraction_f_lift (rhs))); + }. + +Instance t_Neg_28434759 : t_Neg (t_U32) := + { + t_Neg_f_Output := t_U32; + t_Neg_f_neg := fun (self : t_U32) => + t_Concretization_f_concretize (t_Concretization := t_Concretization_34651280) (impl_7__sub (v_WORDSIZE_32_) (impl_10__rem (t_Abstraction_f_lift (self)) (v_WORDSIZE_32_))); + }. + +Instance t_Mul_694927493 : t_Mul (t_U32) (t_U32) := + { + t_Mul_f_Output := t_U32; + t_Mul_f_mul := fun (self : t_U32) (rhs : t_U32) => + t_Concretization_f_concretize (t_Concretization := t_Concretization_34651280) (impl_11__mul (t_Abstraction_f_lift (self)) (t_Abstraction_f_lift (rhs))); + }. + +Instance t_Rem_64936096 : t_Rem (t_U32) (t_U32) := + { + t_Rem_f_Output := t_U32; + t_Rem_f_rem := fun (self : t_U32) (rhs : t_U32) => + t_Concretization_f_concretize (t_Concretization := t_Concretization_34651280) (impl_10__rem (t_Abstraction_f_lift (self)) (t_Abstraction_f_lift (rhs))); + }. + +Instance t_Add_54748823 : t_Add (t_U32) (t_U32) := + { + t_Add_f_Output := t_U32; + t_Add_f_add := fun (self : t_U32) (rhs : t_U32) => + t_Concretization_f_concretize (t_Concretization := t_Concretization_34651280) (impl_6__add (t_Abstraction_f_lift (self)) (t_Abstraction_f_lift (rhs))); + }. + +Instance t_Div_579184696 : t_Div (t_U32) (t_U32) := + { + t_Div_f_Output := t_U32; + t_Div_f_div := fun (self : t_U32) (rhs : t_U32) => + t_Concretization_f_concretize (t_Concretization := t_Concretization_34651280) (impl_10__div (t_Abstraction_f_lift (self)) (t_Abstraction_f_lift (rhs))); + }. + +Instance t_Shl_582224230 : t_Shl (t_U32) (t_U8) := + { + t_Shl_f_Output := t_U32; + t_Shl_f_shl := fun (self : t_U32) (rhs : t_U8) => + t_Concretization_f_concretize (t_Concretization := t_Concretization_34651280) (impl_12__shl (t_Abstraction_f_lift (self)) (t_Abstraction_f_lift (rhs))); + }. + +Instance t_Shl_784746781 : t_Shl (t_U32) (t_U16) := + { + t_Shl_f_Output := t_U32; + t_Shl_f_shl := fun (self : t_U32) (rhs : t_U16) => + t_Concretization_f_concretize (t_Concretization := t_Concretization_34651280) (impl_12__shl (t_Abstraction_f_lift (self)) (t_Abstraction_f_lift (rhs))); + }. + +Instance t_Shl_969375690 : t_Shl (t_U32) (t_U32) := + { + t_Shl_f_Output := t_U32; + t_Shl_f_shl := fun (self : t_U32) (rhs : t_U32) => + t_Concretization_f_concretize (t_Concretization := t_Concretization_34651280) (impl_12__shl (t_Abstraction_f_lift (self)) (t_Abstraction_f_lift (rhs))); + }. + +Instance t_Shl_522639233 : t_Shl (t_U32) (t_U64) := + { + t_Shl_f_Output := t_U32; + t_Shl_f_shl := fun (self : t_U32) (rhs : t_U64) => + t_Concretization_f_concretize (t_Concretization := t_Concretization_34651280) (impl_12__shl (t_Abstraction_f_lift (self)) (t_Abstraction_f_lift (rhs))); + }. + +Instance t_Shl_521929493 : t_Shl (t_U32) (t_U128) := + { + t_Shl_f_Output := t_U32; + t_Shl_f_shl := fun (self : t_U32) (rhs : t_U128) => + t_Concretization_f_concretize (t_Concretization := t_Concretization_34651280) (impl_12__shl (t_Abstraction_f_lift (self)) (t_Abstraction_f_lift (rhs))); + }. + +Instance t_Shr_13621365 : t_Shr (t_U32) (t_U8) := + { + t_Shr_f_Output := t_U32; + t_Shr_f_shr := fun (self : t_U32) (rhs : t_U8) => + t_Concretization_f_concretize (t_Concretization := t_Concretization_34651280) (impl_13__shr (t_Abstraction_f_lift (self)) (t_Abstraction_f_lift (rhs))); + }. + +Instance t_Shr_425099630 : t_Shr (t_U32) (t_U16) := + { + t_Shr_f_Output := t_U32; + t_Shr_f_shr := fun (self : t_U32) (rhs : t_U16) => + t_Concretization_f_concretize (t_Concretization := t_Concretization_34651280) (impl_13__shr (t_Abstraction_f_lift (self)) (t_Abstraction_f_lift (rhs))); + }. + +Instance t_Shr_488072124 : t_Shr (t_U32) (t_U32) := + { + t_Shr_f_Output := t_U32; + t_Shr_f_shr := fun (self : t_U32) (rhs : t_U32) => + t_Concretization_f_concretize (t_Concretization := t_Concretization_34651280) (impl_13__shr (t_Abstraction_f_lift (self)) (t_Abstraction_f_lift (rhs))); + }. + +Instance t_Shr_176245311 : t_Shr (t_U32) (t_U64) := + { + t_Shr_f_Output := t_U32; + t_Shr_f_shr := fun (self : t_U32) (rhs : t_U64) => + t_Concretization_f_concretize (t_Concretization := t_Concretization_34651280) (impl_13__shr (t_Abstraction_f_lift (self)) (t_Abstraction_f_lift (rhs))); + }. + +Instance t_Shr_128161029 : t_Shr (t_U32) (t_U128) := + { + t_Shr_f_Output := t_U32; + t_Shr_f_shr := fun (self : t_U32) (rhs : t_U128) => + t_Concretization_f_concretize (t_Concretization := t_Concretization_34651280) (impl_13__shr (t_Abstraction_f_lift (self)) (t_Abstraction_f_lift (rhs))); + }. + +Instance t_BitXor_302699331 : t_BitXor (t_U32) (t_U32) := + { + t_BitXor_f_Output := t_U32; + t_BitXor_f_bitxor := fun (self : t_U32) (rhs : t_U32) => + t_Concretization_f_concretize (t_Concretization := t_Concretization_34651280) (impl_14__bitxor (t_Abstraction_f_lift (self)) (t_Abstraction_f_lift (rhs))); + }. + +Instance t_BitAnd_259909825 : t_BitAnd (t_U32) (t_U32) := + { + t_BitAnd_f_Output := t_U32; + t_BitAnd_f_bitand := fun (self : t_U32) (rhs : t_U32) => + t_Concretization_f_concretize (t_Concretization := t_Concretization_34651280) (impl_15__bitand (t_Abstraction_f_lift (self)) (t_Abstraction_f_lift (rhs))); + }. + +Instance t_BitOr_944485878 : t_BitOr (t_U32) (t_U32) := + { + t_BitOr_f_Output := t_U32; + t_BitOr_f_bitor := fun (self : t_U32) (rhs : t_U32) => + t_Concretization_f_concretize (t_Concretization := t_Concretization_34651280) (impl_16__bitor (t_Abstraction_f_lift (self)) (t_Abstraction_f_lift (rhs))); + }. + +Instance t_Neg_262148082 : t_Neg (t_U64) := + { + t_Neg_f_Output := t_U64; + t_Neg_f_neg := fun (self : t_U64) => + t_Concretization_f_concretize (t_Concretization := t_Concretization_841277766) (impl_7__sub (v_WORDSIZE_64_) (impl_10__rem (t_Abstraction_f_lift (self)) (v_WORDSIZE_64_))); + }. + +Instance t_Mul_542100838 : t_Mul (t_U64) (t_U64) := + { + t_Mul_f_Output := t_U64; + t_Mul_f_mul := fun (self : t_U64) (rhs : t_U64) => + t_Concretization_f_concretize (t_Concretization := t_Concretization_841277766) (impl_11__mul (t_Abstraction_f_lift (self)) (t_Abstraction_f_lift (rhs))); + }. + +Instance t_Rem_476079061 : t_Rem (t_U64) (t_U64) := + { + t_Rem_f_Output := t_U64; + t_Rem_f_rem := fun (self : t_U64) (rhs : t_U64) => + t_Concretization_f_concretize (t_Concretization := t_Concretization_841277766) (impl_10__rem (t_Abstraction_f_lift (self)) (t_Abstraction_f_lift (rhs))); + }. + +Instance t_Add_680559927 : t_Add (t_U64) (t_U64) := + { + t_Add_f_Output := t_U64; + t_Add_f_add := fun (self : t_U64) (rhs : t_U64) => + t_Concretization_f_concretize (t_Concretization := t_Concretization_841277766) (impl_6__add (t_Abstraction_f_lift (self)) (t_Abstraction_f_lift (rhs))); + }. + +Instance t_Div_288928025 : t_Div (t_U64) (t_U64) := + { + t_Div_f_Output := t_U64; + t_Div_f_div := fun (self : t_U64) (rhs : t_U64) => + t_Concretization_f_concretize (t_Concretization := t_Concretization_841277766) (impl_10__div (t_Abstraction_f_lift (self)) (t_Abstraction_f_lift (rhs))); + }. + +Instance t_Shl_458903955 : t_Shl (t_U64) (t_U8) := + { + t_Shl_f_Output := t_U64; + t_Shl_f_shl := fun (self : t_U64) (rhs : t_U8) => + t_Concretization_f_concretize (t_Concretization := t_Concretization_841277766) (impl_12__shl (t_Abstraction_f_lift (self)) (t_Abstraction_f_lift (rhs))); + }. + +Instance t_Shl_547067457 : t_Shl (t_U64) (t_U16) := + { + t_Shl_f_Output := t_U64; + t_Shl_f_shl := fun (self : t_U64) (rhs : t_U16) => + t_Concretization_f_concretize (t_Concretization := t_Concretization_841277766) (impl_12__shl (t_Abstraction_f_lift (self)) (t_Abstraction_f_lift (rhs))); + }. + +Instance t_Shl_467944790 : t_Shl (t_U64) (t_U32) := + { + t_Shl_f_Output := t_U64; + t_Shl_f_shl := fun (self : t_U64) (rhs : t_U32) => + t_Concretization_f_concretize (t_Concretization := t_Concretization_841277766) (impl_12__shl (t_Abstraction_f_lift (self)) (t_Abstraction_f_lift (rhs))); + }. + +Instance t_Shl_188141782 : t_Shl (t_U64) (t_U64) := + { + t_Shl_f_Output := t_U64; + t_Shl_f_shl := fun (self : t_U64) (rhs : t_U64) => + t_Concretization_f_concretize (t_Concretization := t_Concretization_841277766) (impl_12__shl (t_Abstraction_f_lift (self)) (t_Abstraction_f_lift (rhs))); + }. + +Instance t_Shl_936592019 : t_Shl (t_U64) (t_U128) := + { + t_Shl_f_Output := t_U64; + t_Shl_f_shl := fun (self : t_U64) (rhs : t_U128) => + t_Concretization_f_concretize (t_Concretization := t_Concretization_841277766) (impl_12__shl (t_Abstraction_f_lift (self)) (t_Abstraction_f_lift (rhs))); + }. + +Instance t_Shr_362241607 : t_Shr (t_U64) (t_U8) := + { + t_Shr_f_Output := t_U64; + t_Shr_f_shr := fun (self : t_U64) (rhs : t_U8) => + t_Concretization_f_concretize (t_Concretization := t_Concretization_841277766) (impl_13__shr (t_Abstraction_f_lift (self)) (t_Abstraction_f_lift (rhs))); + }. + +Instance t_Shr_336624052 : t_Shr (t_U64) (t_U16) := + { + t_Shr_f_Output := t_U64; + t_Shr_f_shr := fun (self : t_U64) (rhs : t_U16) => + t_Concretization_f_concretize (t_Concretization := t_Concretization_841277766) (impl_13__shr (t_Abstraction_f_lift (self)) (t_Abstraction_f_lift (rhs))); + }. + +Instance t_Shr_87524769 : t_Shr (t_U64) (t_U32) := + { + t_Shr_f_Output := t_U64; + t_Shr_f_shr := fun (self : t_U64) (rhs : t_U32) => + t_Concretization_f_concretize (t_Concretization := t_Concretization_841277766) (impl_13__shr (t_Abstraction_f_lift (self)) (t_Abstraction_f_lift (rhs))); + }. + +Instance t_Shr_998089409 : t_Shr (t_U64) (t_U64) := + { + t_Shr_f_Output := t_U64; + t_Shr_f_shr := fun (self : t_U64) (rhs : t_U64) => + t_Concretization_f_concretize (t_Concretization := t_Concretization_841277766) (impl_13__shr (t_Abstraction_f_lift (self)) (t_Abstraction_f_lift (rhs))); + }. + +Instance t_Shr_1000705430 : t_Shr (t_U64) (t_U128) := + { + t_Shr_f_Output := t_U64; + t_Shr_f_shr := fun (self : t_U64) (rhs : t_U128) => + t_Concretization_f_concretize (t_Concretization := t_Concretization_841277766) (impl_13__shr (t_Abstraction_f_lift (self)) (t_Abstraction_f_lift (rhs))); + }. + +Instance t_BitXor_68539793 : t_BitXor (t_U64) (t_U64) := + { + t_BitXor_f_Output := t_U64; + t_BitXor_f_bitxor := fun (self : t_U64) (rhs : t_U64) => + t_Concretization_f_concretize (t_Concretization := t_Concretization_841277766) (impl_14__bitxor (t_Abstraction_f_lift (self)) (t_Abstraction_f_lift (rhs))); + }. + +Instance t_BitAnd_91153110 : t_BitAnd (t_U64) (t_U64) := + { + t_BitAnd_f_Output := t_U64; + t_BitAnd_f_bitand := fun (self : t_U64) (rhs : t_U64) => + t_Concretization_f_concretize (t_Concretization := t_Concretization_841277766) (impl_15__bitand (t_Abstraction_f_lift (self)) (t_Abstraction_f_lift (rhs))); + }. + +Instance t_BitOr_746401002 : t_BitOr (t_U64) (t_U64) := + { + t_BitOr_f_Output := t_U64; + t_BitOr_f_bitor := fun (self : t_U64) (rhs : t_U64) => + t_Concretization_f_concretize (t_Concretization := t_Concretization_841277766) (impl_16__bitor (t_Abstraction_f_lift (self)) (t_Abstraction_f_lift (rhs))); + }. + +Instance t_Neg_446348865 : t_Neg (t_U128) := + { + t_Neg_f_Output := t_U128; + t_Neg_f_neg := fun (self : t_U128) => + t_Concretization_f_concretize (t_Concretization := t_Concretization_814811766) (impl_7__sub (v_WORDSIZE_128_) (impl_10__rem (t_Abstraction_f_lift (self)) (v_WORDSIZE_128_))); + }. + +Instance t_Mul_529926072 : t_Mul (t_U128) (t_U128) := + { + t_Mul_f_Output := t_U128; + t_Mul_f_mul := fun (self : t_U128) (rhs : t_U128) => + t_Concretization_f_concretize (t_Concretization := t_Concretization_814811766) (impl_11__mul (t_Abstraction_f_lift (self)) (t_Abstraction_f_lift (rhs))); + }. + +Instance t_Rem_813931227 : t_Rem (t_U128) (t_U128) := + { + t_Rem_f_Output := t_U128; + t_Rem_f_rem := fun (self : t_U128) (rhs : t_U128) => + t_Concretization_f_concretize (t_Concretization := t_Concretization_814811766) (impl_10__rem (t_Abstraction_f_lift (self)) (t_Abstraction_f_lift (rhs))); + }. + +Instance t_Add_509210048 : t_Add (t_U128) (t_U128) := + { + t_Add_f_Output := t_U128; + t_Add_f_add := fun (self : t_U128) (rhs : t_U128) => + t_Concretization_f_concretize (t_Concretization := t_Concretization_814811766) (impl_6__add (t_Abstraction_f_lift (self)) (t_Abstraction_f_lift (rhs))); + }. + +Instance t_Div_733456046 : t_Div (t_U128) (t_U128) := + { + t_Div_f_Output := t_U128; + t_Div_f_div := fun (self : t_U128) (rhs : t_U128) => + t_Concretization_f_concretize (t_Concretization := t_Concretization_814811766) (impl_10__div (t_Abstraction_f_lift (self)) (t_Abstraction_f_lift (rhs))); + }. + +Instance t_Shl_634756453 : t_Shl (t_U128) (t_U8) := + { + t_Shl_f_Output := t_U128; + t_Shl_f_shl := fun (self : t_U128) (rhs : t_U8) => + t_Concretization_f_concretize (t_Concretization := t_Concretization_814811766) (impl_12__shl (t_Abstraction_f_lift (self)) (t_Abstraction_f_lift (rhs))); + }. + +Instance t_Shl_17499927 : t_Shl (t_U128) (t_U16) := + { + t_Shl_f_Output := t_U128; + t_Shl_f_shl := fun (self : t_U128) (rhs : t_U16) => + t_Concretization_f_concretize (t_Concretization := t_Concretization_814811766) (impl_12__shl (t_Abstraction_f_lift (self)) (t_Abstraction_f_lift (rhs))); + }. + +Instance t_Shl_839364374 : t_Shl (t_U128) (t_U32) := + { + t_Shl_f_Output := t_U128; + t_Shl_f_shl := fun (self : t_U128) (rhs : t_U32) => + t_Concretization_f_concretize (t_Concretization := t_Concretization_814811766) (impl_12__shl (t_Abstraction_f_lift (self)) (t_Abstraction_f_lift (rhs))); + }. + +Instance t_Shl_268379728 : t_Shl (t_U128) (t_U64) := + { + t_Shl_f_Output := t_U128; + t_Shl_f_shl := fun (self : t_U128) (rhs : t_U64) => + t_Concretization_f_concretize (t_Concretization := t_Concretization_814811766) (impl_12__shl (t_Abstraction_f_lift (self)) (t_Abstraction_f_lift (rhs))); + }. + +Instance t_Shl_50621237 : t_Shl (t_U128) (t_U128) := + { + t_Shl_f_Output := t_U128; + t_Shl_f_shl := fun (self : t_U128) (rhs : t_U128) => + t_Concretization_f_concretize (t_Concretization := t_Concretization_814811766) (impl_12__shl (t_Abstraction_f_lift (self)) (t_Abstraction_f_lift (rhs))); + }. + +Instance t_Shr_205513961 : t_Shr (t_U128) (t_U8) := + { + t_Shr_f_Output := t_U128; + t_Shr_f_shr := fun (self : t_U128) (rhs : t_U8) => + t_Concretization_f_concretize (t_Concretization := t_Concretization_814811766) (impl_13__shr (t_Abstraction_f_lift (self)) (t_Abstraction_f_lift (rhs))); + }. + +Instance t_Shr_691521055 : t_Shr (t_U128) (t_U16) := + { + t_Shr_f_Output := t_U128; + t_Shr_f_shr := fun (self : t_U128) (rhs : t_U16) => + t_Concretization_f_concretize (t_Concretization := t_Concretization_814811766) (impl_13__shr (t_Abstraction_f_lift (self)) (t_Abstraction_f_lift (rhs))); + }. + +Instance t_Shr_345208632 : t_Shr (t_U128) (t_U32) := + { + t_Shr_f_Output := t_U128; + t_Shr_f_shr := fun (self : t_U128) (rhs : t_U32) => + t_Concretization_f_concretize (t_Concretization := t_Concretization_814811766) (impl_13__shr (t_Abstraction_f_lift (self)) (t_Abstraction_f_lift (rhs))); + }. + +Instance t_Shr_1027860982 : t_Shr (t_U128) (t_U64) := + { + t_Shr_f_Output := t_U128; + t_Shr_f_shr := fun (self : t_U128) (rhs : t_U64) => + t_Concretization_f_concretize (t_Concretization := t_Concretization_814811766) (impl_13__shr (t_Abstraction_f_lift (self)) (t_Abstraction_f_lift (rhs))); + }. + +Instance t_Shr_54460338 : t_Shr (t_U128) (t_U128) := + { + t_Shr_f_Output := t_U128; + t_Shr_f_shr := fun (self : t_U128) (rhs : t_U128) => + t_Concretization_f_concretize (t_Concretization := t_Concretization_814811766) (impl_13__shr (t_Abstraction_f_lift (self)) (t_Abstraction_f_lift (rhs))); + }. + +Instance t_BitXor_579850070 : t_BitXor (t_U128) (t_U128) := + { + t_BitXor_f_Output := t_U128; + t_BitXor_f_bitxor := fun (self : t_U128) (rhs : t_U128) => + t_Concretization_f_concretize (t_Concretization := t_Concretization_814811766) (impl_14__bitxor (t_Abstraction_f_lift (self)) (t_Abstraction_f_lift (rhs))); + }. + +Instance t_BitAnd_550145691 : t_BitAnd (t_U128) (t_U128) := + { + t_BitAnd_f_Output := t_U128; + t_BitAnd_f_bitand := fun (self : t_U128) (rhs : t_U128) => + t_Concretization_f_concretize (t_Concretization := t_Concretization_814811766) (impl_15__bitand (t_Abstraction_f_lift (self)) (t_Abstraction_f_lift (rhs))); + }. + +Instance t_BitOr_123199302 : t_BitOr (t_U128) (t_U128) := + { + t_BitOr_f_Output := t_U128; + t_BitOr_f_bitor := fun (self : t_U128) (rhs : t_U128) => + t_Concretization_f_concretize (t_Concretization := t_Concretization_814811766) (impl_16__bitor (t_Abstraction_f_lift (self)) (t_Abstraction_f_lift (rhs))); + }. + +Instance t_Sub_209890052 : t_Sub (t_U8) (t_U8) := + { + t_Sub_f_Output := t_U8; + t_Sub_f_sub := fun (self : t_U8) (rhs : t_U8) => + t_Add_f_add (t_Add := t_Add_121545721) (self) (t_Neg_f_neg (rhs)); + }. + +Instance t_Not_3946298 : t_Not (t_U8) := + { + t_Not_f_Output := t_U8; + t_Not_f_not := fun (self : t_U8) => + t_BitXor_f_bitxor (self) (t_Constants_f_MAX : t_U8); + }. + +Instance t_Sub_307813249 : t_Sub (t_U16) (t_U16) := + { + t_Sub_f_Output := t_U16; + t_Sub_f_sub := fun (self : t_U16) (rhs : t_U16) => + t_Add_f_add (t_Add := t_Add_71250682) (self) (t_Neg_f_neg (rhs)); + }. + +Instance t_Not_887206550 : t_Not (t_U16) := + { + t_Not_f_Output := t_U16; + t_Not_f_not := fun (self : t_U16) => + t_BitXor_f_bitxor (self) (t_Constants_f_MAX); + }. + +Instance t_Sub_967239595 : t_Sub (t_U32) (t_U32) := + { + t_Sub_f_Output := t_U32; + t_Sub_f_sub := fun (self : t_U32) (rhs : t_U32) => + t_Add_f_add (t_Add := t_Add_54748823) (self) (t_Neg_f_neg (rhs)); + }. + +Instance t_Not_966968542 : t_Not (t_U32) := + { + t_Not_f_Output := t_U32; + t_Not_f_not := fun (self : t_U32) => + t_BitXor_f_bitxor (self) (t_Constants_f_MAX); + }. + +Instance t_Sub_324061209 : t_Sub (t_U64) (t_U64) := + { + t_Sub_f_Output := t_U64; + t_Sub_f_sub := fun (self : t_U64) (rhs : t_U64) => + t_Add_f_add (t_Add := t_Add_680559927) (self) (t_Neg_f_neg (rhs)); + }. + +Instance t_Not_807247311 : t_Not (t_U64) := + { + t_Not_f_Output := t_U64; + t_Not_f_not := fun (self : t_U64) => + t_BitXor_f_bitxor (self) (t_Constants_f_MAX); + }. + +Instance t_Sub_549381231 : t_Sub (t_U128) (t_U128) := + { + t_Sub_f_Output := t_U128; + t_Sub_f_sub := fun (self : t_U128) (rhs : t_U128) => + t_Add_f_add (t_Add := t_Add_509210048) (self) (t_Neg_f_neg (rhs)); + }. + +Instance t_Not_651062842 : t_Not (t_U128) := + { + t_Not_f_Output := t_U128; + t_Not_f_not := fun (self : t_U128) => + t_BitXor_f_bitxor (self) (t_Constants_f_MAX); + }. diff --git a/proof-libs/coq/coq/src/Core_Intrinsics.v b/proof-libs/coq/coq/src/Core_Intrinsics.v new file mode 100644 index 000000000..e7216d21d --- /dev/null +++ b/proof-libs/coq/coq/src/Core_Intrinsics.v @@ -0,0 +1,119 @@ +(* File automatically generated by Hacspec *) +From Coq Require Import ZArith. +Import List.ListNotations. +Open Scope Z_scope. +Open Scope bool_scope. +Require Import String. + +From Core Require Import Core_Primitive. +Export Core_Primitive. + +From Core Require Import Core_Int. +Export Core_Int. + +From Core Require Import Core_Coerce. +Export Core_Coerce. + +(* NotImplementedYet *) + +Definition unchecked_add_u128 (x : t_u128) (y : t_u128) : t_u128 := + Build_t_u128 (Build_t_U128 (impl_6__add (t_Abstraction_f_lift (t_u128_0 x)) (t_Abstraction_f_lift (t_u128_0 y)))). + +Definition unchecked_add_u16 (x : t_u16) (y : t_u16) : t_u16 := + Build_t_u16 (Build_t_U16 (impl_6__add (t_Abstraction_f_lift (t_u16_0 x)) (t_Abstraction_f_lift (t_u16_0 y)))). + +Definition unchecked_add_u32 (x : t_u32) (y : t_u32) : t_u32 := + Build_t_u32 (Build_t_U32 (impl_6__add (t_Abstraction_f_lift (t_u32_0 x)) (t_Abstraction_f_lift (t_u32_0 y)))). + +Definition unchecked_add_u64 (x : t_u64) (y : t_u64) : t_u64 := + Build_t_u64 (Build_t_U64 (impl_6__add (t_Abstraction_f_lift (t_u64_0 x)) (t_Abstraction_f_lift (t_u64_0 y)))). + +Definition unchecked_add_u8 (x : t_u8) (y : t_u8) : t_u8 := + Build_t_u8 (Build_t_U8 (impl_6__add (t_Abstraction_f_lift (t_u8_0 x)) (t_Abstraction_f_lift (t_u8_0 y)))). + +Definition unchecked_add_usize (x : t_usize) (y : t_usize) : t_usize := + Build_t_usize (Build_t_U64 (impl_6__add (t_Abstraction_f_lift (t_usize_0 x)) (t_Abstraction_f_lift (t_usize_0 y)))). + +Definition add_with_overflow_u128 (x : t_u128) (y : t_u128) : (t_u128*bool) := + let overflow := impl_6__add (t_Abstraction_f_lift (t_u128_0 x)) (t_Abstraction_f_lift (t_u128_0 y)) in + let res : t_U128 := t_Concretization_f_concretize (t_Clone_f_clone (overflow)) in + (Build_t_u128 (t_Clone_f_clone (res)),t_PartialOrd_f_lt (t_Abstraction_f_lift (t_Abstraction := t_Abstraction_462669591) (res)) (overflow)). + +Definition add_with_overflow_u16 (x : t_u16) (y : t_u16) : (t_u16*bool) := + let overflow := impl_6__add (t_Abstraction_f_lift (t_u16_0 x)) (t_Abstraction_f_lift (t_u16_0 y)) in + let res : t_U16 := t_Concretization_f_concretize (t_Clone_f_clone (overflow)) in + (Build_t_u16 (t_Clone_f_clone (res)),t_PartialOrd_f_lt (t_Abstraction_f_lift (t_Abstraction:=t_Abstraction_134234872) (res)) (overflow)). + +Definition add_with_overflow_u32 (x : t_u32) (y : t_u32) : (t_u32*bool) := + let overflow := impl_6__add (t_Abstraction_f_lift (t_u32_0 x)) (t_Abstraction_f_lift (t_u32_0 y)) in + let res : t_U32 := t_Concretization_f_concretize (t_Clone_f_clone (overflow)) in + (Build_t_u32 (t_Clone_f_clone (res)),t_PartialOrd_f_lt (t_Abstraction_f_lift (t_Abstraction:=t_Abstraction_699270934) (res)) (overflow)). + +Definition add_with_overflow_u64 (x : t_u64) (y : t_u64) : (t_u64*bool) := + let overflow := impl_6__add (t_Abstraction_f_lift (t_u64_0 x)) (t_Abstraction_f_lift (t_u64_0 y)) in + let res : t_U64 := t_Concretization_f_concretize (t_Clone_f_clone (overflow)) in + (Build_t_u64 (t_Clone_f_clone (res)),t_PartialOrd_f_lt (t_Abstraction_f_lift (t_Abstraction:=t_Abstraction_374630185) (res)) (overflow)). + +Definition add_with_overflow_u8 (x : t_u8) (y : t_u8) : (t_u8*bool) := + let overflow := impl_6__add (t_Abstraction_f_lift (t_u8_0 x)) (t_Abstraction_f_lift (t_u8_0 y)) in + let res : t_U8 := t_Concretization_f_concretize (t_Clone_f_clone (overflow)) in + (Build_t_u8 (t_Clone_f_clone (res)),t_PartialOrd_f_lt (t_Abstraction_f_lift (t_Abstraction := t_Abstraction_566214702) (res)) (overflow)). + +Definition add_with_overflow_usize (x : t_usize) (y : t_usize) : (t_usize*bool) := + let overflow := impl_6__add (t_Abstraction_f_lift (t_usize_0 x)) (t_Abstraction_f_lift (t_usize_0 y)) in + let res : t_U64 := t_Concretization_f_concretize (t_Clone_f_clone (overflow)) in + (Build_t_usize (t_Clone_f_clone (res)),t_PartialOrd_f_lt (t_Abstraction_f_lift (t_Abstraction := t_Abstraction_374630185) (res)) (overflow)). + +Definition wrapping_add_u128 (a : t_u128) (b : t_u128) : t_u128 := + Build_t_u128 (t_Add_f_add (t_u128_0 a) (t_u128_0 b)). + +Definition wrapping_add_u16 (a : t_u16) (b : t_u16) : t_u16 := + Build_t_u16 (t_Add_f_add (t_u16_0 a) (t_u16_0 b)). + +Definition wrapping_add_u32 (a : t_u32) (b : t_u32) : t_u32 := + Build_t_u32 (t_Add_f_add (t_u32_0 a) (t_u32_0 b)). + +Definition wrapping_add_u64 (a : t_u64) (b : t_u64) : t_u64 := + Build_t_u64 (t_Add_f_add (t_u64_0 a) (t_u64_0 b)). + +Definition wrapping_add_u8 (a : t_u8) (b : t_u8) : t_u8 := + Build_t_u8 (t_Add_f_add (t_u8_0 a) (t_u8_0 b)). + +Definition wrapping_add_usize (a : t_usize) (b : t_usize) : t_usize := + Build_t_usize (t_Add_f_add (t_usize_0 a) (t_usize_0 b)). + +Definition wrapping_mul_u128 (a : t_u128) (b : t_u128) : t_u128 := + Build_t_u128 (t_Mul_f_mul (t_u128_0 a) (t_u128_0 b)). + +Definition wrapping_mul_u16 (a : t_u16) (b : t_u16) : t_u16 := + Build_t_u16 (t_Mul_f_mul (t_u16_0 a) (t_u16_0 b)). + +Definition wrapping_mul_u32 (a : t_u32) (b : t_u32) : t_u32 := + Build_t_u32 (t_Mul_f_mul (t_u32_0 a) (t_u32_0 b)). + +Definition wrapping_mul_u64 (a : t_u64) (b : t_u64) : t_u64 := + Build_t_u64 (t_Mul_f_mul (t_u64_0 a) (t_u64_0 b)). + +Definition wrapping_mul_u8 (a : t_u8) (b : t_u8) : t_u8 := + Build_t_u8 (t_Mul_f_mul (t_u8_0 a) (t_u8_0 b)). + +Definition wrapping_mul_usize (a : t_usize) (b : t_usize) : t_usize := + Build_t_usize (t_Mul_f_mul (t_usize_0 a) (t_usize_0 b)). + +Definition wrapping_sub_u128 (a : t_u128) (b : t_u128) : t_u128 := + Build_t_u128 (t_Sub_f_sub (t_u128_0 a) (t_u128_0 b)). + +Definition wrapping_sub_u16 (a : t_u16) (b : t_u16) : t_u16 := + Build_t_u16 (t_Sub_f_sub (t_u16_0 a) (t_u16_0 b)). + +Definition wrapping_sub_u32 (a : t_u32) (b : t_u32) : t_u32 := + Build_t_u32 (t_Sub_f_sub (t_u32_0 a) (t_u32_0 b)). + +Definition wrapping_sub_u64 (a : t_u64) (b : t_u64) : t_u64 := + Build_t_u64 (t_Sub_f_sub (t_u64_0 a) (t_u64_0 b)). + +Definition wrapping_sub_u8 (a : t_u8) (b : t_u8) : t_u8 := + Build_t_u8 (t_Sub_f_sub (t_u8_0 a) (t_u8_0 b)). + +Definition wrapping_sub_usize (a : t_usize) (b : t_usize) : t_usize := + Build_t_usize (t_Sub_f_sub (t_usize_0 a) (t_usize_0 b)). diff --git a/proof-libs/coq/coq/src/Core_Marker.v b/proof-libs/coq/coq/src/Core_Marker.v new file mode 100644 index 000000000..1ad36f565 --- /dev/null +++ b/proof-libs/coq/coq/src/Core_Marker.v @@ -0,0 +1,31 @@ +(* File automatically generated by Hacspec *) +From Coq Require Import ZArith. +Import List.ListNotations. +Open Scope Z_scope. +Open Scope bool_scope. +Require Import String. + +From Core Require Import Core_Clone (t_Clone). +Export Core_Clone (t_Clone). + +Class t_Copy `{v_Self : Type} `{t_Clone v_Self} : Type := + { + }. +Arguments t_Copy:clear implicits. +Arguments t_Copy (_) {_}. + +Class t_Destruct `{v_Self : Type} : Type := + { + }. +Arguments t_Destruct:clear implicits. +Arguments t_Destruct (_). + +Class t_Sized `{v_Self : Type} : Type := + { + }. +Arguments t_Sized:clear implicits. +Arguments t_Sized (_). + +(* *** *) + +Instance t_Sized_any T : t_Sized T := {}. diff --git a/proof-libs/coq/coq/src/Core_Num.v b/proof-libs/coq/coq/src/Core_Num.v new file mode 100644 index 000000000..f229d38db --- /dev/null +++ b/proof-libs/coq/coq/src/Core_Num.v @@ -0,0 +1,317 @@ +(* File automatically generated by Hacspec *) +From Coq Require Import ZArith. +Import List.ListNotations. +Open Scope Z_scope. +Open Scope bool_scope. +Require Import String. + +From Core Require Import Core_Int. +Export Core_Int. + +From Core Require Import Core_Primitive. +Export Core_Primitive. + +From Core Require Import Core_Intrinsics. +Export Core_Intrinsics. + +(* NotImplementedYet *) + +Definition impl_4__MAX : t_u128 := + Build_t_u128 (t_Constants_f_MAX). + +Definition impl_4__MIN : t_u128 := + Build_t_u128 (t_Constants_f_MIN). + +Definition impl_1__MAX : t_u16 := + Build_t_u16 (t_Constants_f_MAX). + +Definition impl_1__MIN : t_u16 := + Build_t_u16 (t_Constants_f_MIN). + +Definition impl__BITS : t_u32 := + Build_t_u32 (impl_21__BITS). + +Definition impl_1__BITS : t_u32 := + Build_t_u32 (impl_48__BITS). + +Definition impl_2__BITS : t_u32 := + Build_t_u32 (impl_75__BITS). + +Definition impl_2__MAX : t_u32 := + Build_t_u32 (t_Constants_f_MAX). + +Definition impl_2__MIN : t_u32 := + Build_t_u32 (t_Constants_f_MIN). + +Definition impl_3__BITS : t_u32 := + Build_t_u32 (impl_102__BITS). + +Definition impl_4__BITS : t_u32 := + Build_t_u32 (impl_129__BITS). + +Definition impl_5__BITS : t_u32 := + Build_t_u32 (impl_102__BITS). + +Definition impl_3__MAX : t_u64 := + Build_t_u64 (t_Constants_f_MAX). + +Definition impl_3__MIN : t_u64 := + Build_t_u64 (t_Constants_f_MIN). + +Definition impl__MAX : t_u8 := + Build_t_u8 (t_Constants_f_MAX). + +Definition impl__MIN : t_u8 := + Build_t_u8 (t_Constants_f_MIN). + +Definition impl_5__MAX : t_usize := + Build_t_usize (t_Constants_f_MAX). + +Definition impl_5__MIN : t_usize := + Build_t_usize (t_Constants_f_MIN). + +Definition impl__overflowing_add (self : t_u8) (rhs : t_u8) : (t_u8*bool) := + add_with_overflow_u8 (self) (rhs). + +Definition impl_1__overflowing_add (self : t_u16) (rhs : t_u16) : (t_u16*bool) := + add_with_overflow_u16 (self) (rhs). + +Definition impl_2__overflowing_add (self : t_u32) (rhs : t_u32) : (t_u32*bool) := + add_with_overflow_u32 (self) (rhs). + +Definition impl_3__overflowing_add (self : t_u64) (rhs : t_u64) : (t_u64*bool) := + add_with_overflow_u64 (self) (rhs). + +Definition impl_4__overflowing_add (self : t_u128) (rhs : t_u128) : (t_u128*bool) := + add_with_overflow_u128 (self) (rhs). + +Definition impl_5__overflowing_add (self : t_usize) (rhs : t_usize) : (t_usize*bool) := + add_with_overflow_usize (self) (rhs). + +(* Definition impl__from_le_bytes (bytes : t_Array (t_u8) (Build_t_usize (Build_t_U64 1%N))) : t_u8 := *) +(* let ret := t_Constants_f_ZERO in *) +(* let index := t_Constants_f_ZERO in *) +(* let '(index,ret) := fold_range (Build_t_usize (Build_t_U64 0%N)) (Build_t_usize (Build_t_U64 1%N)) (fun '(index,ret) _ => *) +(* true) ((index,ret)) (fun '(index,ret) i => *) +(* let val_i : t_U8 := t_Into_f_into (t_u8_0 impl_2__index (t_Clone_f_clone (bytes)) (i)) in *) +(* let ret := t_Add_f_add (ret) (t_Shl_f_shl (val_i) (t_Mul_f_mul (impl_21__BITS) (t_Clone_f_clone (index)))) in *) +(* let index := t_Add_f_add (index) (t_Constants_f_ONE) in *) +(* (index,ret)) in *) +(* Build_t_u8 (ret). *) + +(* Definition impl__from_be_bytes (bytes : t_Array (t_u8) (Build_t_usize (Build_t_U64 1%N))) : t_u8 := *) +(* impl__from_le_bytes (impl_2__reverse (bytes)). *) + +Definition impl__wrapping_add (self : t_u8) (rhs : t_u8) : t_u8 := + wrapping_add_u8 (self) (rhs). + +Definition impl__wrapping_mul (self : t_u8) (rhs : t_u8) : t_u8 := + wrapping_mul_u8 (self) (rhs). + +(* Definition impl_1__from_le_bytes (bytes : t_Array (t_u8) (Build_t_usize (Build_t_U64 2%N))) : t_u16 := *) +(* let ret := t_Constants_f_ZERO in *) +(* let index := t_Constants_f_ZERO in *) +(* let '(index,ret) := fold_range (Build_t_usize (Build_t_U64 0%N)) (Build_t_usize (Build_t_U64 2%N)) (fun '(index,ret) _ => *) +(* true) ((index,ret)) (fun '(index,ret) i => *) +(* let val_i : t_U16 := t_Into_f_into (t_u8_0 impl_2__index (t_Clone_f_clone (bytes)) (i)) in *) +(* let ret := t_Add_f_add (ret) (t_Shl_f_shl (val_i) (t_Mul_f_mul (impl_21__BITS) (t_Clone_f_clone (index)))) in *) +(* let index := t_Add_f_add (index) (t_Constants_f_ONE) in *) +(* (index,ret)) in *) +(* Build_t_u16 (ret). *) + +(* Definition impl_1__from_be_bytes (bytes : t_Array (t_u8) (Build_t_usize (Build_t_U64 2%N))) : t_u16 := *) +(* impl_1__from_le_bytes (impl_2__reverse (bytes)). *) + +Definition impl_1__wrapping_add (self : t_u16) (rhs : t_u16) : t_u16 := + wrapping_add_u16 (self) (rhs). + +Definition impl_1__wrapping_mul (self : t_u16) (rhs : t_u16) : t_u16 := + wrapping_mul_u16 (self) (rhs). + +(* Definition impl_2__from_le_bytes (bytes : t_Array (t_u8) (Build_t_usize (Build_t_U64 4%N))) : t_u32 := *) +(* let ret := t_Constants_f_ZERO in *) +(* let index := t_Constants_f_ZERO in *) +(* let '(index,ret) := fold_range (Build_t_usize (Build_t_U64 0%N)) (Build_t_usize (Build_t_U64 4%N)) (fun '(index,ret) _ => *) +(* true) ((index,ret)) (fun '(index,ret) i => *) +(* let val_i : t_U32 := t_Into_f_into (t_u8_0 impl_2__index (t_Clone_f_clone (bytes)) (i)) in *) +(* let ret := t_Add_f_add (ret) (t_Shl_f_shl (val_i) (t_Mul_f_mul (impl_21__BITS) (t_Clone_f_clone (index)))) in *) +(* let index := t_Add_f_add (index) (t_Constants_f_ONE) in *) +(* (index,ret)) in *) +(* Build_t_u32 (ret). *) + +(* Definition impl_2__from_be_bytes (bytes : t_Array (t_u8) (Build_t_usize (Build_t_U64 4%N))) : t_u32 := *) +(* impl_2__from_le_bytes (impl_2__reverse (bytes)). *) + +Definition impl_2__wrapping_add (self : t_u32) (rhs : t_u32) : t_u32 := + wrapping_add_u32 (self) (rhs). + +Definition impl_2__wrapping_mul (self : t_u32) (rhs : t_u32) : t_u32 := + wrapping_mul_u32 (self) (rhs). + +(* Definition impl_3__from_le_bytes (bytes : t_Array (t_u8) (Build_t_usize (Build_t_U64 8%N))) : t_u64 := *) +(* let ret := t_Constants_f_ZERO in *) +(* let index := t_Constants_f_ZERO in *) +(* let '(index,ret) := fold_range (Build_t_usize (Build_t_U64 0%N)) (Build_t_usize (Build_t_U64 8%N)) (fun '(index,ret) _ => *) +(* true) ((index,ret)) (fun '(index,ret) i => *) +(* let val_i : t_U64 := t_Into_f_into (t_u8_0 impl_2__index (t_Clone_f_clone (bytes)) (i)) in *) +(* let ret := t_Add_f_add (ret) (t_Shl_f_shl (val_i) (t_Mul_f_mul (impl_21__BITS) (t_Clone_f_clone (index)))) in *) +(* let index := t_Add_f_add (index) (t_Constants_f_ONE) in *) +(* (index,ret)) in *) +(* Build_t_u64 (ret). *) + +(* Definition impl_3__from_be_bytes (bytes : t_Array (t_u8) (Build_t_usize (Build_t_U64 8%N))) : t_u64 := *) +(* impl_3__from_le_bytes (impl_2__reverse (bytes)). *) + +Definition impl_3__wrapping_add (self : t_u64) (rhs : t_u64) : t_u64 := + wrapping_add_u64 (self) (rhs). + +Definition impl_3__wrapping_mul (self : t_u64) (rhs : t_u64) : t_u64 := + wrapping_mul_u64 (self) (rhs). + +(* Definition impl_4__from_le_bytes (bytes : t_Array (t_u8) (Build_t_usize (Build_t_U64 16%N))) : t_u128 := *) +(* let ret := t_Constants_f_ZERO in *) +(* let index := t_Constants_f_ZERO in *) +(* let '(index,ret) := fold_range (Build_t_usize (Build_t_U64 0%N)) (Build_t_usize (Build_t_U64 16%N)) (fun '(index,ret) _ => *) +(* true) ((index,ret)) (fun '(index,ret) i => *) +(* let val_i : t_U128 := t_Into_f_into (t_u8_0 impl_2__index (t_Clone_f_clone (bytes)) (i)) in *) +(* let ret := t_Add_f_add (ret) (t_Shl_f_shl (val_i) (t_Mul_f_mul (impl_21__BITS) (t_Clone_f_clone (index)))) in *) +(* let index := t_Add_f_add (index) (t_Constants_f_ONE) in *) +(* (index,ret)) in *) +(* Build_t_u128 (ret). *) + +(* Definition impl_4__from_be_bytes (bytes : t_Array (t_u8) (Build_t_usize (Build_t_U64 16%N))) : t_u128 := *) +(* impl_4__from_le_bytes (impl_2__reverse (bytes)). *) + +Definition impl_4__wrapping_add (self : t_u128) (rhs : t_u128) : t_u128 := + wrapping_add_u128 (self) (rhs). + +Definition impl_4__wrapping_mul (self : t_u128) (rhs : t_u128) : t_u128 := + wrapping_mul_u128 (self) (rhs). + +(* Definition impl_5__from_le_bytes (bytes : t_Array (t_u8) (Build_t_usize (Build_t_U64 8%N))) : t_usize := *) +(* let ret := t_Constants_f_ZERO in *) +(* let index := t_Constants_f_ZERO in *) +(* let '(index,ret) := fold_range (Build_t_usize (Build_t_U64 0%N)) (Build_t_usize (Build_t_U64 8%N)) (fun '(index,ret) _ => *) +(* true) ((index,ret)) (fun '(index,ret) i => *) +(* let val_i : t_U64 := t_Into_f_into (t_u8_0 impl_2__index (t_Clone_f_clone (bytes)) (i)) in *) +(* let ret := t_Add_f_add (ret) (t_Shl_f_shl (val_i) (t_Mul_f_mul (impl_21__BITS) (t_Clone_f_clone (index)))) in *) +(* let index := t_Add_f_add (index) (t_Constants_f_ONE) in *) +(* (index,ret)) in *) +(* Build_t_usize (ret). *) + +(* Definition impl_5__from_be_bytes (bytes : t_Array (t_u8) (Build_t_usize (Build_t_U64 8%N))) : t_usize := *) +(* impl_5__from_le_bytes (impl_2__reverse (bytes)). *) + +Definition impl_5__wrapping_add (self : t_usize) (rhs : t_usize) : t_usize := + wrapping_add_usize (self) (rhs). + +Definition impl_5__wrapping_mul (self : t_usize) (rhs : t_usize) : t_usize := + wrapping_mul_usize (self) (rhs). + +Definition impl__wrapping_sub (self : t_u8) (rhs : t_u8) : t_u8 := + wrapping_sub_u8 (self) (rhs). + +Definition impl__wrapping_neg (self : t_u8) : t_u8 := + impl__wrapping_sub (Build_t_u8 (t_Constants_f_ZERO)) (self). + +Definition impl_1__wrapping_sub (self : t_u16) (rhs : t_u16) : t_u16 := + wrapping_sub_u16 (self) (rhs). + +Definition impl_1__wrapping_neg (self : t_u16) : t_u16 := + impl_1__wrapping_sub (Build_t_u16 (t_Constants_f_ZERO)) (self). + +Definition impl_2__wrapping_sub (self : t_u32) (rhs : t_u32) : t_u32 := + wrapping_sub_u32 (self) (rhs). + +Definition impl_2__wrapping_neg (self : t_u32) : t_u32 := + impl_2__wrapping_sub (Build_t_u32 (t_Constants_f_ZERO)) (self). + +Definition impl_3__wrapping_sub (self : t_u64) (rhs : t_u64) : t_u64 := + wrapping_sub_u64 (self) (rhs). + +Definition impl_3__wrapping_neg (self : t_u64) : t_u64 := + impl_3__wrapping_sub (Build_t_u64 (t_Constants_f_ZERO)) (self). + +Definition impl_4__wrapping_sub (self : t_u128) (rhs : t_u128) : t_u128 := + wrapping_sub_u128 (self) (rhs). + +Definition impl_4__wrapping_neg (self : t_u128) : t_u128 := + impl_4__wrapping_sub (Build_t_u128 (t_Constants_f_ZERO)) (self). + +Definition impl_5__wrapping_sub (self : t_usize) (rhs : t_usize) : t_usize := + wrapping_sub_usize (self) (rhs). + +Definition impl_5__wrapping_neg (self : t_usize) : t_usize := + impl_5__wrapping_sub (Build_t_usize (t_Constants_f_ZERO)) (self). + +Definition impl__wrapping_rem (self : t_u8) (rhs : t_u8) : t_u8 := + t_Rem_f_rem (self) (rhs). + +Definition impl__wrapping_rem_euclid (self : t_u8) (rhs : t_u8) : t_u8 := + t_Rem_f_rem (self) (rhs). + +Definition impl__wrapping_div (self : t_u8) (rhs : t_u8) : t_u8 := + t_Div_f_div (self) (rhs). + +Definition impl__wrapping_div_euclid (self : t_u8) (rhs : t_u8) : t_u8 := + t_Div_f_div (self) (rhs). + +Definition impl_1__wrapping_rem (self : t_u16) (rhs : t_u16) : t_u16 := + t_Rem_f_rem (self) (rhs). + +Definition impl_1__wrapping_rem_euclid (self : t_u16) (rhs : t_u16) : t_u16 := + t_Rem_f_rem (self) (rhs). + +Definition impl_1__wrapping_div (self : t_u16) (rhs : t_u16) : t_u16 := + t_Div_f_div (self) (rhs). + +Definition impl_1__wrapping_div_euclid (self : t_u16) (rhs : t_u16) : t_u16 := + t_Div_f_div (self) (rhs). + +Definition impl_2__wrapping_rem (self : t_u32) (rhs : t_u32) : t_u32 := + t_Rem_f_rem (self) (rhs). + +Definition impl_2__wrapping_rem_euclid (self : t_u32) (rhs : t_u32) : t_u32 := + t_Rem_f_rem (self) (rhs). + +Definition impl_2__wrapping_div (self : t_u32) (rhs : t_u32) : t_u32 := + t_Div_f_div (self) (rhs). + +Definition impl_2__wrapping_div_euclid (self : t_u32) (rhs : t_u32) : t_u32 := + t_Div_f_div (self) (rhs). + +Definition impl_3__wrapping_rem (self : t_u64) (rhs : t_u64) : t_u64 := + t_Rem_f_rem (self) (rhs). + +Definition impl_3__wrapping_rem_euclid (self : t_u64) (rhs : t_u64) : t_u64 := + t_Rem_f_rem (self) (rhs). + +Definition impl_3__wrapping_div (self : t_u64) (rhs : t_u64) : t_u64 := + t_Div_f_div (self) (rhs). + +Definition impl_3__wrapping_div_euclid (self : t_u64) (rhs : t_u64) : t_u64 := + t_Div_f_div (self) (rhs). + +Definition impl_4__wrapping_rem (self : t_u128) (rhs : t_u128) : t_u128 := + t_Rem_f_rem (self) (rhs). + +Definition impl_4__wrapping_rem_euclid (self : t_u128) (rhs : t_u128) : t_u128 := + t_Rem_f_rem (self) (rhs). + +Definition impl_4__wrapping_div (self : t_u128) (rhs : t_u128) : t_u128 := + t_Div_f_div (self) (rhs). + +Definition impl_4__wrapping_div_euclid (self : t_u128) (rhs : t_u128) : t_u128 := + t_Div_f_div (self) (rhs). + +Definition impl_5__wrapping_rem (self : t_usize) (rhs : t_usize) : t_usize := + t_Rem_f_rem (self) (rhs). + +Definition impl_5__wrapping_rem_euclid (self : t_usize) (rhs : t_usize) : t_usize := + t_Rem_f_rem (self) (rhs). + +Definition impl_5__wrapping_div (self : t_usize) (rhs : t_usize) : t_usize := + t_Div_f_div (self) (rhs). + +Definition impl_5__wrapping_div_euclid (self : t_usize) (rhs : t_usize) : t_usize := + t_Div_f_div (self) (rhs). diff --git a/proof-libs/coq/coq/src/Core_Ops.v b/proof-libs/coq/coq/src/Core_Ops.v new file mode 100644 index 000000000..f3f969e13 --- /dev/null +++ b/proof-libs/coq/coq/src/Core_Ops.v @@ -0,0 +1,52 @@ +(* File automatically generated by Hacspec *) +From Coq Require Import ZArith. +Import List.ListNotations. +Open Scope Z_scope. +Open Scope bool_scope. +Require Import String. + +From Core Require Import Core_Ops_Arith. +Export Core_Ops_Arith. + +(* From Core Require Import Core_Ops_Arith (t_Add). *) +(* Export Core_Ops_Arith (t_Add). *) + +(* From Core Require Import Core_Ops_Arith (t_Div). *) +(* Export Core_Ops_Arith (t_Div). *) + +(* From Core Require Import Core_Ops_Arith (t_Mul). *) +(* Export Core_Ops_Arith (t_Mul). *) + +(* From Core Require Import Core_Ops_Arith (t_Neg). *) +(* Export Core_Ops_Arith (t_Neg). *) + +(* From Core Require Import Core_Ops_Arith (t_Rem). *) +(* Export Core_Ops_Arith (t_Rem). *) + +(* From Core Require Import Core_Ops_Arith (t_Sub). *) +(* Export Core_Ops_Arith (t_Sub). *) + +From Core Require Import Core_Ops_Bit. +Export Core_Ops_Bit. + +(* From Core Require Import Core_Ops_Bit (t_BitAnd). *) +(* Export Core_Ops_Bit (t_BitAnd). *) + +(* From Core Require Import Core_Ops_Bit (t_BitOr). *) +(* Export Core_Ops_Bit (t_BitOr). *) + +(* From Core Require Import Core_Ops_Bit (t_BitXor). *) +(* Export Core_Ops_Bit (t_BitXor). *) + +(* From Core Require Import Core_Ops_Bit (t_Not). *) +(* Export Core_Ops_Bit (t_Not). *) + +(* From Core Require Import Core_Ops_Bit (t_Shl). *) +(* Export Core_Ops_Bit (t_Shl). *) + +(* From Core Require Import Core_Ops_Bit (t_Shr). *) +(* Export Core_Ops_Bit (t_Shr). *) + +(* NotImplementedYet *) + +(* NotImplementedYet *) diff --git a/proof-libs/coq/coq/src/Core_Ops_Arith.v b/proof-libs/coq/coq/src/Core_Ops_Arith.v new file mode 100644 index 000000000..9a8eb127a --- /dev/null +++ b/proof-libs/coq/coq/src/Core_Ops_Arith.v @@ -0,0 +1,59 @@ +(* File automatically generated by Hacspec *) +From Coq Require Import ZArith. +Import List.ListNotations. +Open Scope Z_scope. +Open Scope bool_scope. +Require Import String. + +From Core Require Import Core_Marker (t_Sized). +Export Core_Marker (t_Sized). + +(* NotImplementedYet *) + +Class t_Add `{v_Self : Type} `{v_Rhs : Type} `{t_Sized v_Rhs} : Type := + { + t_Add_f_Output : Type; + t_Add_f_add : v_Self -> v_Rhs -> t_Add_f_Output; + }. +Arguments t_Add:clear implicits. +Arguments t_Add (_) (_) {_}. + +Class t_Div `{v_Self : Type} `{v_Rhs : Type} `{t_Sized v_Rhs} : Type := + { + t_Div_f_Output : Type; + t_Div_f_div : v_Self -> v_Rhs -> t_Div_f_Output; + }. +Arguments t_Div:clear implicits. +Arguments t_Div (_) (_) {_}. + +Class t_Mul `{v_Self : Type} `{v_Rhs : Type} `{t_Sized v_Rhs} : Type := + { + t_Mul_f_Output : Type; + t_Mul_f_mul : v_Self -> v_Rhs -> t_Mul_f_Output; + }. +Arguments t_Mul:clear implicits. +Arguments t_Mul (_) (_) {_}. + +Class t_Neg `{v_Self : Type} : Type := + { + t_Neg_f_Output : Type; + t_Neg_f_neg : v_Self -> t_Neg_f_Output; + }. +Arguments t_Neg:clear implicits. +Arguments t_Neg (_). + +Class t_Rem `{v_Self : Type} `{v_Rhs : Type} `{t_Sized v_Rhs} : Type := + { + t_Rem_f_Output : Type; + t_Rem_f_rem : v_Self -> v_Rhs -> t_Rem_f_Output; + }. +Arguments t_Rem:clear implicits. +Arguments t_Rem (_) (_) {_}. + +Class t_Sub `{v_Self : Type} `{v_Rhs : Type} `{t_Sized v_Rhs} : Type := + { + t_Sub_f_Output : Type; + t_Sub_f_sub : v_Self -> v_Rhs -> t_Sub_f_Output; + }. +Arguments t_Sub:clear implicits. +Arguments t_Sub (_) (_) {_}. diff --git a/proof-libs/coq/coq/src/Core_Ops_Bit.v b/proof-libs/coq/coq/src/Core_Ops_Bit.v new file mode 100644 index 000000000..6ec42a34d --- /dev/null +++ b/proof-libs/coq/coq/src/Core_Ops_Bit.v @@ -0,0 +1,57 @@ +(* File automatically generated by Hacspec *) +From Coq Require Import ZArith. +Import List.ListNotations. +Open Scope Z_scope. +Open Scope bool_scope. +Require Import String. + +From Core Require Import Core_Marker (t_Sized). +Export Core_Marker (t_Sized). + +Class t_BitAnd `{v_Self : Type} `{v_Rhs : Type} `{t_Sized v_Rhs} : Type := + { + t_BitAnd_f_Output : Type; + t_BitAnd_f_bitand : v_Self -> v_Rhs -> t_BitAnd_f_Output; + }. +Arguments t_BitAnd:clear implicits. +Arguments t_BitAnd (_) (_) {_}. + +Class t_BitOr `{v_Self : Type} `{v_Rhs : Type} `{t_Sized v_Rhs} : Type := + { + t_BitOr_f_Output : Type; + t_BitOr_f_bitor : v_Self -> v_Rhs -> t_BitOr_f_Output; + }. +Arguments t_BitOr:clear implicits. +Arguments t_BitOr (_) (_) {_}. + +Class t_BitXor `{v_Self : Type} `{v_Rhs : Type} `{t_Sized v_Rhs} : Type := + { + t_BitXor_f_Output : Type; + t_BitXor_f_bitxor : v_Self -> v_Rhs -> t_BitXor_f_Output; + }. +Arguments t_BitXor:clear implicits. +Arguments t_BitXor (_) (_) {_}. + +Class t_Not `{v_Self : Type} : Type := + { + t_Not_f_Output : Type; + t_Not_f_not : v_Self -> t_Not_f_Output; + }. +Arguments t_Not:clear implicits. +Arguments t_Not (_). + +Class t_Shl `{v_Self : Type} `{v_Rhs : Type} `{t_Sized v_Rhs} : Type := + { + t_Shl_f_Output : Type; + t_Shl_f_shl : v_Self -> v_Rhs -> t_Shl_f_Output; + }. +Arguments t_Shl:clear implicits. +Arguments t_Shl (_) (_) {_}. + +Class t_Shr `{v_Self : Type} `{v_Rhs : Type} `{t_Sized v_Rhs} : Type := + { + t_Shr_f_Output : Type; + t_Shr_f_shr : v_Self -> v_Rhs -> t_Shr_f_Output; + }. +Arguments t_Shr:clear implicits. +Arguments t_Shr (_) (_) {_}. diff --git a/proof-libs/coq/coq/src/Core_Option.v b/proof-libs/coq/coq/src/Core_Option.v new file mode 100644 index 000000000..665b6adf9 --- /dev/null +++ b/proof-libs/coq/coq/src/Core_Option.v @@ -0,0 +1,12 @@ +(* File automatically generated by Hacspec *) +From Coq Require Import ZArith. +Import List.ListNotations. +Open Scope Z_scope. +Open Scope bool_scope. +Require Import String. + +Inductive t_Option `{v_T : Type} : Type := +| t_Option_Option_None +| t_Option_Option_Some : v_T -> _. +Arguments t_Option:clear implicits. +Arguments t_Option (_). diff --git a/proof-libs/coq/coq/src/Core_Panicking.v b/proof-libs/coq/coq/src/Core_Panicking.v new file mode 100644 index 000000000..086ae44e0 --- /dev/null +++ b/proof-libs/coq/coq/src/Core_Panicking.v @@ -0,0 +1,20 @@ +(* File automatically generated by Hacspec *) +From Coq Require Import ZArith. +Import List.ListNotations. +Open Scope Z_scope. +Open Scope bool_scope. +Require Import String. + +From Core Require Import Core_Marker. +Export Core_Marker. + +Definition t_Never : Type := False. + +Definition never_to_any `{v_T : Type} `{t_Sized v_T} (x : t_Never) : v_T := + (match x with end). + +Fixpoint panic (expr : string) `{false = true} : t_Never := + never_to_any (Bool.diff_false_true H). + +Definition panic_explicit (_ : unit) `{false = true} : t_Never := + never_to_any (Bool.diff_false_true H). diff --git a/proof-libs/coq/coq/src/Core_Primitive.v b/proof-libs/coq/coq/src/Core_Primitive.v new file mode 100644 index 000000000..7c5050da2 --- /dev/null +++ b/proof-libs/coq/coq/src/Core_Primitive.v @@ -0,0 +1,552 @@ +(* File automatically generated by Hacspec *) +From Coq Require Import ZArith. +Import List.ListNotations. +Open Scope Z_scope. +Open Scope bool_scope. +Require Import String. + +From Core Require Import Core_Int. +Export Core_Int. + + +From Core Require Import Core_Ops_Arith. +Export Core_Ops_Arith. + + +From Core Require Import Core_Ops_Bit. +Export Core_Ops_Bit. + + +From Core Require Import Core_Cmp. +Export Core_Cmp. + + +From Core Require Import Core_Base_Int_Base_impl. +Export Core_Base_Int_Base_impl. + +From Core Require Import Core_Base_Seq_Base_impl. +Export Core_Base_Seq_Base_impl. + +(* NotImplementedYet *) + +(* NotImplementedYet *) + +(* NotImplementedYet *) + +Record t_u128 : Type := + { + t_u128_0 : t_U128 + }. +Arguments t_u128:clear implicits. +Arguments t_u128. + +Instance t_Clone_687423776 : t_Clone (t_u128) := + { + t_Clone_f_clone := fun (self : t_u128) => + Build_t_u128 (t_Clone_f_clone (t_u128_0 self)); + }. + +Instance t_PartialEq_359515708 : t_PartialEq (t_u128) (t_u128) := + { + t_PartialEq_f_eq := fun (self : t_u128) (rhs : t_u128) => + t_PartialEq_f_eq (t_u128_0 self) (t_u128_0 rhs); + t_PartialEq_f_ne := fun (self : t_u128) (rhs : t_u128) => + negb (t_PartialEq_f_eq (t_u128_0 self) (t_u128_0 rhs)); + }. + +Instance t_PartialOrd_133463987 : t_PartialOrd (t_u128) (t_u128) := + { + t_PartialOrd_f_partial_cmp := fun (self : t_u128) (rhs : t_u128) => + t_PartialOrd_f_partial_cmp (t_u128_0 self) (t_u128_0 rhs); + t_PartialOrd_f_lt := fun (self : t_u128) (rhs : t_u128) => + match t_PartialOrd_f_partial_cmp (t_u128_0 self) (t_u128_0 rhs) with + | t_Option_Option_Some (t_Ordering_Ordering_Less) => + true + | _ => + false + end; + t_PartialOrd_f_le := fun (self : t_u128) (rhs : t_u128) => + match t_PartialOrd_f_partial_cmp (t_u128_0 self) (t_u128_0 rhs) with + | t_Option_Option_Some (t_Ordering_Ordering_Less + | t_Ordering_Ordering_Equal) => + true + | _ => + false + end; + t_PartialOrd_f_gt := fun (self : t_u128) (rhs : t_u128) => + match t_PartialOrd_f_partial_cmp (t_u128_0 self) (t_u128_0 rhs) with + | t_Option_Option_Some (t_Ordering_Ordering_Greater) => + true + | _ => + false + end; + t_PartialOrd_f_ge := fun (self : t_u128) (rhs : t_u128) => + match t_PartialOrd_f_partial_cmp (t_u128_0 self) (t_u128_0 rhs) with + | t_Option_Option_Some (t_Ordering_Ordering_Greater + | t_Ordering_Ordering_Equal) => + true + | _ => + false + end; + }. + +Record t_u16 : Type := + { + t_u16_0 : t_U16 + }. +Arguments t_u16:clear implicits. +Arguments t_u16. + +Instance t_Clone_676169635 : t_Clone (t_u16) := + { + t_Clone_f_clone := fun (self : t_u16) => + Build_t_u16 (t_Clone_f_clone (t_u16_0 self)); + }. + +Instance t_PartialEq_499855381 : t_PartialEq (t_u16) (t_u16) := + { + t_PartialEq_f_eq := fun (self : t_u16) (rhs : t_u16) => + t_PartialEq_f_eq (t_u16_0 self) (t_u16_0 rhs); + t_PartialEq_f_ne := fun (self : t_u16) (rhs : t_u16) => + negb (t_PartialEq_f_eq (t_u16_0 self) (t_u16_0 rhs)); + }. + +Instance t_PartialOrd_901197325 : t_PartialOrd (t_u16) (t_u16) := + { + t_PartialOrd_f_partial_cmp := fun (self : t_u16) (rhs : t_u16) => + t_PartialOrd_f_partial_cmp (t_u16_0 self) (t_u16_0 rhs); + t_PartialOrd_f_lt := fun (self : t_u16) (rhs : t_u16) => + match t_PartialOrd_f_partial_cmp (t_u16_0 self) (t_u16_0 rhs) with + | t_Option_Option_Some (t_Ordering_Ordering_Less) => + true + | _ => + false + end; + t_PartialOrd_f_le := fun (self : t_u16) (rhs : t_u16) => + match t_PartialOrd_f_partial_cmp (t_u16_0 self) (t_u16_0 rhs) with + | t_Option_Option_Some (t_Ordering_Ordering_Less + | t_Ordering_Ordering_Equal) => + true + | _ => + false + end; + t_PartialOrd_f_gt := fun (self : t_u16) (rhs : t_u16) => + match t_PartialOrd_f_partial_cmp (t_u16_0 self) (t_u16_0 rhs) with + | t_Option_Option_Some (t_Ordering_Ordering_Greater) => + true + | _ => + false + end; + t_PartialOrd_f_ge := fun (self : t_u16) (rhs : t_u16) => + match t_PartialOrd_f_partial_cmp (t_u16_0 self) (t_u16_0 rhs) with + | t_Option_Option_Some (t_Ordering_Ordering_Greater + | t_Ordering_Ordering_Equal) => + true + | _ => + false + end; + }. + +Record t_u32 : Type := + { + t_u32_0 : t_U32 + }. +Arguments t_u32:clear implicits. +Arguments t_u32. + +Instance t_Clone_148051061 : t_Clone (t_u32) := + { + t_Clone_f_clone := fun (self : t_u32) => + Build_t_u32 (t_Clone_f_clone (t_u32_0 self)); + }. + +Instance t_PartialEq_988555028 : t_PartialEq (t_u32) (t_u32) := + { + t_PartialEq_f_eq := fun (self : t_u32) (rhs : t_u32) => + t_PartialEq_f_eq (t_u32_0 self) (t_u32_0 rhs); + t_PartialEq_f_ne := fun (self : t_u32) (rhs : t_u32) => + negb (t_PartialEq_f_eq (t_u32_0 self) (t_u32_0 rhs)); + }. + +Instance t_PartialOrd_675443355 : t_PartialOrd (t_u32) (t_u32) := + { + t_PartialOrd_f_partial_cmp := fun (self : t_u32) (rhs : t_u32) => + t_PartialOrd_f_partial_cmp (t_u32_0 self) (t_u32_0 rhs); + t_PartialOrd_f_lt := fun (self : t_u32) (rhs : t_u32) => + match t_PartialOrd_f_partial_cmp (t_u32_0 self) (t_u32_0 rhs) with + | t_Option_Option_Some (t_Ordering_Ordering_Less) => + true + | _ => + false + end; + t_PartialOrd_f_le := fun (self : t_u32) (rhs : t_u32) => + match t_PartialOrd_f_partial_cmp (t_u32_0 self) (t_u32_0 rhs) with + | t_Option_Option_Some (t_Ordering_Ordering_Less + | t_Ordering_Ordering_Equal) => + true + | _ => + false + end; + t_PartialOrd_f_gt := fun (self : t_u32) (rhs : t_u32) => + match t_PartialOrd_f_partial_cmp (t_u32_0 self) (t_u32_0 rhs) with + | t_Option_Option_Some (t_Ordering_Ordering_Greater) => + true + | _ => + false + end; + t_PartialOrd_f_ge := fun (self : t_u32) (rhs : t_u32) => + match t_PartialOrd_f_partial_cmp (t_u32_0 self) (t_u32_0 rhs) with + | t_Option_Option_Some (t_Ordering_Ordering_Greater + | t_Ordering_Ordering_Equal) => + true + | _ => + false + end; + }. + +Record t_u64 : Type := + { + t_u64_0 : t_U64 + }. +Arguments t_u64:clear implicits. +Arguments t_u64. + +Instance t_Clone_732456945 : t_Clone (t_u64) := + { + t_Clone_f_clone := fun (self : t_u64) => + Build_t_u64 (t_Clone_f_clone (t_u64_0 self)); + }. + +Instance t_PartialEq_387792562 : t_PartialEq (t_u64) (t_u64) := + { + t_PartialEq_f_eq := fun (self : t_u64) (rhs : t_u64) => + t_PartialEq_f_eq (t_u64_0 self) (t_u64_0 rhs); + t_PartialEq_f_ne := fun (self : t_u64) (rhs : t_u64) => + negb (t_PartialEq_f_eq (t_u64_0 self) (t_u64_0 rhs)); + }. + +Instance t_PartialOrd_864557835 : t_PartialOrd (t_u64) (t_u64) := + { + t_PartialOrd_f_partial_cmp := fun (self : t_u64) (rhs : t_u64) => + t_PartialOrd_f_partial_cmp (t_u64_0 self) (t_u64_0 rhs); + t_PartialOrd_f_lt := fun (self : t_u64) (rhs : t_u64) => + match t_PartialOrd_f_partial_cmp (t_u64_0 self) (t_u64_0 rhs) with + | t_Option_Option_Some (t_Ordering_Ordering_Less) => + true + | _ => + false + end; + t_PartialOrd_f_le := fun (self : t_u64) (rhs : t_u64) => + match t_PartialOrd_f_partial_cmp (t_u64_0 self) (t_u64_0 rhs) with + | t_Option_Option_Some (t_Ordering_Ordering_Less + | t_Ordering_Ordering_Equal) => + true + | _ => + false + end; + t_PartialOrd_f_gt := fun (self : t_u64) (rhs : t_u64) => + match t_PartialOrd_f_partial_cmp (t_u64_0 self) (t_u64_0 rhs) with + | t_Option_Option_Some (t_Ordering_Ordering_Greater) => + true + | _ => + false + end; + t_PartialOrd_f_ge := fun (self : t_u64) (rhs : t_u64) => + match t_PartialOrd_f_partial_cmp (t_u64_0 self) (t_u64_0 rhs) with + | t_Option_Option_Some (t_Ordering_Ordering_Greater + | t_Ordering_Ordering_Equal) => + true + | _ => + false + end; + }. + +Record t_u8 : Type := + { + t_u8_0 : t_U8 + }. +Arguments t_u8:clear implicits. +Arguments t_u8. + +Instance t_Clone_448525304 : t_Clone (t_u8) := + { + t_Clone_f_clone := fun (self : t_u8) => + Build_t_u8 (t_Clone_f_clone (t_u8_0 self)); + }. + +Instance t_PartialEq_92335612 : t_PartialEq (t_u8) (t_u8) := + { + t_PartialEq_f_eq := fun (self : t_u8) (rhs : t_u8) => + t_PartialEq_f_eq (t_u8_0 self) (t_u8_0 rhs); + t_PartialEq_f_ne := fun (self : t_u8) (rhs : t_u8) => + negb (t_PartialEq_f_eq (t_u8_0 self) (t_u8_0 rhs)); + }. + +Instance t_PartialOrd_414384327 : t_PartialOrd (t_u8) (t_u8) := + { + t_PartialOrd_f_partial_cmp := fun (self : t_u8) (rhs : t_u8) => + t_PartialOrd_f_partial_cmp (t_u8_0 self) (t_u8_0 rhs); + t_PartialOrd_f_lt := fun (self : t_u8) (rhs : t_u8) => + match t_PartialOrd_f_partial_cmp (t_u8_0 self) (t_u8_0 rhs) with + | t_Option_Option_Some (t_Ordering_Ordering_Less) => + true + | _ => + false + end; + t_PartialOrd_f_le := fun (self : t_u8) (rhs : t_u8) => + match t_PartialOrd_f_partial_cmp (t_u8_0 self) (t_u8_0 rhs) with + | t_Option_Option_Some (t_Ordering_Ordering_Less + | t_Ordering_Ordering_Equal) => + true + | _ => + false + end; + t_PartialOrd_f_gt := fun (self : t_u8) (rhs : t_u8) => + match t_PartialOrd_f_partial_cmp (t_u8_0 self) (t_u8_0 rhs) with + | t_Option_Option_Some (t_Ordering_Ordering_Greater) => + true + | _ => + false + end; + t_PartialOrd_f_ge := fun (self : t_u8) (rhs : t_u8) => + match t_PartialOrd_f_partial_cmp (t_u8_0 self) (t_u8_0 rhs) with + | t_Option_Option_Some (t_Ordering_Ordering_Greater + | t_Ordering_Ordering_Equal) => + true + | _ => + false + end; + }. + +Record t_usize : Type := + { + t_usize_0 : t_U64 + }. +Arguments t_usize:clear implicits. +Arguments t_usize. + +Instance t_Clone_323393662 : t_Clone (t_usize) := + { + t_Clone_f_clone := fun (self : t_usize) => + Build_t_usize (t_Clone_f_clone (t_usize_0 self)); + }. + +Instance t_PartialEq_585670484 : t_PartialEq (t_usize) (t_usize) := + { + t_PartialEq_f_eq := fun (self : t_usize) (rhs : t_usize) => + t_PartialEq_f_eq (t_usize_0 self) (t_usize_0 rhs); + t_PartialEq_f_ne := fun (self : t_usize) (rhs : t_usize) => + negb (t_PartialEq_f_eq (t_usize_0 self) (t_usize_0 rhs)); + }. + +Instance t_PartialOrd_249911946 : t_PartialOrd (t_usize) (t_usize) := + { + t_PartialOrd_f_partial_cmp := fun (self : t_usize) (rhs : t_usize) => + t_PartialOrd_f_partial_cmp (t_usize_0 self) (t_usize_0 rhs); + t_PartialOrd_f_lt := fun (self : t_usize) (rhs : t_usize) => + match t_PartialOrd_f_partial_cmp (t_usize_0 self) (t_usize_0 rhs) with + | t_Option_Option_Some (t_Ordering_Ordering_Less) => + true + | _ => + false + end; + t_PartialOrd_f_le := fun (self : t_usize) (rhs : t_usize) => + match t_PartialOrd_f_partial_cmp (t_usize_0 self) (t_usize_0 rhs) with + | t_Option_Option_Some (t_Ordering_Ordering_Less + | t_Ordering_Ordering_Equal) => + true + | _ => + false + end; + t_PartialOrd_f_gt := fun (self : t_usize) (rhs : t_usize) => + match t_PartialOrd_f_partial_cmp (t_usize_0 self) (t_usize_0 rhs) with + | t_Option_Option_Some (t_Ordering_Ordering_Greater) => + true + | _ => + false + end; + t_PartialOrd_f_ge := fun (self : t_usize) (rhs : t_usize) => + match t_PartialOrd_f_partial_cmp (t_usize_0 self) (t_usize_0 rhs) with + | t_Option_Option_Some (t_Ordering_Ordering_Greater + | t_Ordering_Ordering_Equal) => + true + | _ => + false + end; + }. + +Instance t_Mul_310564612 : t_Mul (t_u8) (t_u8) := + { + t_Mul_f_Output := t_u8; + t_Mul_f_mul := fun (self : t_u8) (rhs : t_u8) => + Build_t_u8 (t_Mul_f_mul (t_u8_0 self) (t_u8_0 rhs)); + }. + +Instance t_Rem_765572693 : t_Rem (t_u8) (t_u8) := + { + t_Rem_f_Output := t_u8; + t_Rem_f_rem := fun (self : t_u8) (rhs : t_u8) => + Build_t_u8 (t_Rem_f_rem (t_u8_0 self) (t_u8_0 rhs)); + }. + +Instance t_Add_960049504 : t_Add (t_u8) (t_u8) := + { + t_Add_f_Output := t_u8; + t_Add_f_add := fun (self : t_u8) (rhs : t_u8) => + Build_t_u8 (t_Add_f_add (t_u8_0 self) (t_u8_0 rhs)); + }. + +Instance t_Div_866285265 : t_Div (t_u8) (t_u8) := + { + t_Div_f_Output := t_u8; + t_Div_f_div := fun (self : t_u8) (rhs : t_u8) => + Build_t_u8 (t_Div_f_div (t_u8_0 self) (t_u8_0 rhs)); + }. + +Instance t_Mul_257417847 : t_Mul (t_u16) (t_u16) := + { + t_Mul_f_Output := t_u16; + t_Mul_f_mul := fun (self : t_u16) (rhs : t_u16) => + Build_t_u16 (t_Mul_f_mul (t_u16_0 self) (t_u16_0 rhs)); + }. + +Instance t_Rem_318118895 : t_Rem (t_u16) (t_u16) := + { + t_Rem_f_Output := t_u16; + t_Rem_f_rem := fun (self : t_u16) (rhs : t_u16) => + Build_t_u16 (t_Rem_f_rem (t_u16_0 self) (t_u16_0 rhs)); + }. + +Instance t_Add_554073404 : t_Add (t_u16) (t_u16) := + { + t_Add_f_Output := t_u16; + t_Add_f_add := fun (self : t_u16) (rhs : t_u16) => + Build_t_u16 (t_Add_f_add (t_u16_0 self) (t_u16_0 rhs)); + }. + +Instance t_Div_1045893244 : t_Div (t_u16) (t_u16) := + { + t_Div_f_Output := t_u16; + t_Div_f_div := fun (self : t_u16) (rhs : t_u16) => + Build_t_u16 (t_Div_f_div (t_u16_0 self) (t_u16_0 rhs)); + }. + +Instance t_Mul_800987573 : t_Mul (t_u32) (t_u32) := + { + t_Mul_f_Output := t_u32; + t_Mul_f_mul := fun (self : t_u32) (rhs : t_u32) => + Build_t_u32 (t_Mul_f_mul (t_u32_0 self) (t_u32_0 rhs)); + }. + +Instance t_Rem_666023061 : t_Rem (t_u32) (t_u32) := + { + t_Rem_f_Output := t_u32; + t_Rem_f_rem := fun (self : t_u32) (rhs : t_u32) => + Build_t_u32 (t_Rem_f_rem (t_u32_0 self) (t_u32_0 rhs)); + }. + +Instance t_Add_446443714 : t_Add (t_u32) (t_u32) := + { + t_Add_f_Output := t_u32; + t_Add_f_add := fun (self : t_u32) (rhs : t_u32) => + Build_t_u32 (t_Add_f_add (t_u32_0 self) (t_u32_0 rhs)); + }. + +Instance t_Div_688119654 : t_Div (t_u32) (t_u32) := + { + t_Div_f_Output := t_u32; + t_Div_f_div := fun (self : t_u32) (rhs : t_u32) => + Build_t_u32 (t_Div_f_div (t_u32_0 self) (t_u32_0 rhs)); + }. + +Instance t_Mul_33292302 : t_Mul (t_u64) (t_u64) := + { + t_Mul_f_Output := t_u64; + t_Mul_f_mul := fun (self : t_u64) (rhs : t_u64) => + Build_t_u64 (t_Mul_f_mul (t_u64_0 self) (t_u64_0 rhs)); + }. + +Instance t_Rem_647345183 : t_Rem (t_u64) (t_u64) := + { + t_Rem_f_Output := t_u64; + t_Rem_f_rem := fun (self : t_u64) (rhs : t_u64) => + Build_t_u64 (t_Rem_f_rem (t_u64_0 self) (t_u64_0 rhs)); + }. + +Instance t_Add_843567851 : t_Add (t_u64) (t_u64) := + { + t_Add_f_Output := t_u64; + t_Add_f_add := fun (self : t_u64) (rhs : t_u64) => + Build_t_u64 (t_Add_f_add (t_u64_0 self) (t_u64_0 rhs)); + }. + +Instance t_Div_1022519543 : t_Div (t_u64) (t_u64) := + { + t_Div_f_Output := t_u64; + t_Div_f_div := fun (self : t_u64) (rhs : t_u64) => + Build_t_u64 (t_Div_f_div (t_u64_0 self) (t_u64_0 rhs)); + }. + +Instance t_Mul_338793759 : t_Mul (t_u128) (t_u128) := + { + t_Mul_f_Output := t_u128; + t_Mul_f_mul := fun (self : t_u128) (rhs : t_u128) => + Build_t_u128 (t_Mul_f_mul (t_u128_0 self) (t_u128_0 rhs)); + }. + +Instance t_Rem_265261400 : t_Rem (t_u128) (t_u128) := + { + t_Rem_f_Output := t_u128; + t_Rem_f_rem := fun (self : t_u128) (rhs : t_u128) => + Build_t_u128 (t_Rem_f_rem (t_u128_0 self) (t_u128_0 rhs)); + }. + +Instance t_Add_6018763 : t_Add (t_u128) (t_u128) := + { + t_Add_f_Output := t_u128; + t_Add_f_add := fun (self : t_u128) (rhs : t_u128) => + Build_t_u128 (t_Add_f_add (t_u128_0 self) (t_u128_0 rhs)); + }. + +Instance t_Div_344800454 : t_Div (t_u128) (t_u128) := + { + t_Div_f_Output := t_u128; + t_Div_f_div := fun (self : t_u128) (rhs : t_u128) => + Build_t_u128 (t_Div_f_div (t_u128_0 self) (t_u128_0 rhs)); + }. + +Instance t_Mul_628159638 : t_Mul (t_usize) (t_usize) := + { + t_Mul_f_Output := t_usize; + t_Mul_f_mul := fun (self : t_usize) (rhs : t_usize) => + Build_t_usize (t_Mul_f_mul (t_usize_0 self) (t_usize_0 rhs)); + }. + +Instance t_Rem_315243380 : t_Rem (t_usize) (t_usize) := + { + t_Rem_f_Output := t_usize; + t_Rem_f_rem := fun (self : t_usize) (rhs : t_usize) => + Build_t_usize (t_Rem_f_rem (t_usize_0 self) (t_usize_0 rhs)); + }. + +Instance t_Add_1007246287 : t_Add (t_usize) (t_usize) := + { + t_Add_f_Output := t_usize; + t_Add_f_add := fun (self : t_usize) (rhs : t_usize) => + Build_t_usize (t_Add_f_add (t_usize_0 self) (t_usize_0 rhs)); + }. + +Instance t_Div_611868226 : t_Div (t_usize) (t_usize) := + { + t_Div_f_Output := t_usize; + t_Div_f_div := fun (self : t_usize) (rhs : t_usize) => + Build_t_usize (t_Div_f_div (t_usize_0 self) (t_usize_0 rhs)); + }. + +Record t_Array `{v_T : Type} `{v_N : t_usize} `{t_Sized v_T} : Type := + { + t_Array_f_v : t_Seq (v_T) + }. +Arguments t_Array:clear implicits. +Arguments t_Array (_) (_) {_}. +Arguments Build_t_Array {_} {_} {_}.