Library implementation needed for coverage

proof-libs/coq/coq/generated-core/_CoqProject

@@ -60,12 +60,17 @@
 
 ./phase_library/ControlFlow.v
 
-# ./src/Core_Primitive.v
-
+# Bundles: Core_Primitive.v,
 ./src/Core_Array_Rec_bundle_579704328.v
 
+./src/Core_Primitive.v
+
 # ./src/Core_Num.v # Broken?
 
+./phase_library/NumberNotation.v
+./phase_library/TODO.v
+
+./src/Core.v
 
 # # Extra
 
@@ -74,7 +79,7 @@
 # Core_Slice_Index_Private_slice_index.v
 # Core_Slice_Index.v
 # Core_Slice.v
-# Core_Result.v
+# ----- Core_Result.v
 # Core_Primitive_Number_conversion_i.v
 # Core_Primitive_Number_conversion.v
 # Core_Primitive.v
@@ -89,8 +94,8 @@
 # Core_Ops_Arith_Impls_for_prims.v
 # ----- Core_Ops_Arith.v
 # ----- Core_Ops.v
-# Core_Num_Uint_macros.v
-# Core_Num_Int_macros.v
+# ----- Core_Num_Uint_macros.v
+# ----- Core_Num_Int_macros.v
 # Core_Num.v
 # ----- Core_Marker.v
 # Core_Iter_Traits_Marker.v

proof-libs/coq/coq/generated-core/phase_library/NumberNotation.v

@@ -0,0 +1,52 @@
+(* File automatically generated by Hacspec *)
+From Coq Require Import ZArith.
+Require Import List.
+Import List.ListNotations.
+Open Scope Z_scope.
+Open Scope bool_scope.
+Require Import Ascii.
+Require Import String.
+Require Import Coq.Floats.Floats.
+From RecordUpdate Require Import RecordSet.
+Import RecordSetNotations.
+
+Require Import Core_Primitive.
+Export Core_Primitive.
+
+(* Handwritten *)
+
+Coercion Build_t_i8 : t_I8 >-> t_i8.
+Coercion Build_t_I8 : Z >-> t_I8.
+
+Coercion Build_t_i16 : t_I16 >-> t_i16.
+Coercion Build_t_I16 : Z >-> t_I16.
+
+Coercion Build_t_i32 : t_I32 >-> t_i32.
+Coercion Build_t_I32 : Z >-> t_I32.
+
+Coercion Build_t_i64 : t_I64 >-> t_i64.
+Coercion Build_t_I64 : Z >-> t_I64.
+
+Coercion Build_t_i128 : t_I128 >-> t_i128.
+Coercion Build_t_I128 : Z >-> t_I128.
+
+Coercion Build_t_isize : t_I64 >-> t_isize.
+
+Coercion Build_t_u8 : t_U8 >-> t_u8.
+Coercion Build_t_U8 : N >-> t_U8.
+
+Coercion Build_t_u16 : t_U16 >-> t_u16.
+Coercion Build_t_U16 : N >-> t_U16.
+
+Coercion Build_t_u32 : t_U32 >-> t_u32.
+Coercion Build_t_U32 : N >-> t_U32.
+
+Coercion Build_t_u64 : t_U64 >-> t_u64.
+Coercion Build_t_U64 : N >-> t_U64.
+
+Coercion Build_t_u128 : t_U128 >-> t_u128.
+Coercion Build_t_U128 : N >-> t_U128.
+
+Coercion Build_t_usize : t_U64 >-> t_usize.
+
+Coercion Z.to_N : Z >-> N.

proof-libs/coq/coq/generated-core/phase_library/TODO.v

@@ -0,0 +1,24 @@
+(* File automatically generated by Hacspec *)
+From Coq Require Import ZArith.
+Require Import List.
+Import List.ListNotations.
+Open Scope Z_scope.
+Open Scope bool_scope.
+Require Import Ascii.
+Require Import String.
+Require Import Coq.Floats.Floats.
+From RecordUpdate Require Import RecordSet.
+Import RecordSetNotations.
+
+Require Import Core_Primitive.
+Export Core_Primitive.
+
+(* Array coercions *)
+Coercion Build_t_Array : t_Slice >-> t_Array.
+Coercion Build_t_Slice : list >-> t_Slice.
+
+Definition unsize {A} (x : A) := x.
+Definition repeat {v_T} (a : v_T) b : t_Array v_T b := List.repeat a (N.to_nat (U64_f_v (usize_0 b))).
+
+Definition t_String := string.
+Definition ToString_f_to_string (x : string) : string := x.

proof-libs/coq/coq/generated-core/src/Core.v

@@ -12,54 +12,8 @@ Import RecordSetNotations.
 
 (* From Core Require Import Core. *)
 
-(* TODO: Replace this dummy lib with core lib *)
-Class t_Sized (T : Type) := { }.
-Definition t_u8 := Z.
-Definition t_u16 := Z.
-Definition t_u32 := Z.
-Definition t_u64 := Z.
-Definition t_u128 := Z.
-Definition t_usize := Z.
-Definition t_i8 := Z.
-Definition t_i16 := Z.
-Definition t_i32 := Z.
-Definition t_i64 := Z.
-Definition t_i128 := Z.
-Definition t_isize := Z.
-Definition t_Array T (x : t_usize) := list T.
-Definition t_String := string.
-Definition ToString_f_to_string (x : string) := x.
-Instance Sized_any : forall {t_A}, t_Sized t_A := {}.
-Class t_Clone (T : Type) := { Clone_f_clone : T -> T }.
-Instance Clone_any : forall {t_A}, t_Clone t_A := {Clone_f_clone := fun x => x}.
-Definition t_Slice (T : Type) := list T.
-Definition unsize {T : Type} : list T -> t_Slice T := id.
-Definition t_PartialEq_f_eq x y := x =? y.
-Definition t_Rem_f_rem (x y : Z) := x mod y.
-Definition assert (b : bool) (* `{H_assert : b = true} *) : unit := tt.
-Inductive globality := | t_Global.
-Definition t_Vec T (_ : globality) : Type := list T.
-Definition impl_1__append {T} l1 l2 : list T * list T := (app l1 l2, l2).
-Definition impl_1__len {A} (l : list A) := Z.of_nat (List.length l).
-Definition impl__new {A} (_ : Datatypes.unit) : list A := nil.
-Definition impl__with_capacity {A} (_ : Z)  : list A := nil.
-Definition impl_1__push {A} l (x : A) := cons x l.
-Class t_From (A B : Type) := { From_f_from : B -> A }.
-Definition impl__to_vec {T} (x : t_Slice T) : t_Vec T t_Global := x.
-Class t_Into (A B : Type) := { Into_f_into : A -> B }.
-Instance t_Into_from_t_From {A B : Type} `{H : t_From B A} : t_Into A B := { Into_f_into x := @From_f_from B A H x }.
-Definition from_elem {A} (x : A) (l : Z) := repeat x (Z.to_nat l).
-Definition t_Option := option.
-Definition impl__map {A B} (x : t_Option A) (f : A -> B) : t_Option B := match x with | Some x => Some (f x) | None => None end.
-Definition t_Add_f_add x y := x + y.
-Class Cast A B := { cast : A -> B }.
-Instance cast_t_u8_t_u32 : Cast t_u8 t_u32 := {| cast x := x |}.
-(* / dummy lib *)
-
-
-
-From Core Require Import primitive.
-Export primitive.
+From Core Require Import Core_Primitive.
+Export Core_Primitive.
 
 (* NotImplementedYet *)
 
@@ -106,3 +60,10 @@ Export primitive.
 (* NotImplementedYet *)
 
 (* NotImplementedYet *)
+
+
+From Core Require Import NumberNotation.
+Export NumberNotation.
+
+From Core Require Import TODO.
+Export TODO.

proof-libs/coq/coq/generated-core/src/Core_Primitive.v

@@ -27,11 +27,14 @@ Export Core_Base.
 From Core Require Import Core_Base_interface_Int.
 Export Core_Base_interface_Int.
 
+From Core Require Import Core_Array_Rec_bundle_579704328.
+Export Core_Array_Rec_bundle_579704328.
+
 Notation "'t_Slice'" := (t_Slice).
 
 Notation "'Slice_f_v'" := (Slice_f_v).
 
-Notation "'impl_2'" := (impl_2).
+(* Notation "'impl_2'" := (impl_2). *)
 
 Notation "'t_Array'" := (t_Array).
 
@@ -43,37 +46,37 @@ Notation "'t_i128'" := (t_i128).
 
 Notation "'i128_0'" := (i128_0).
 
-Notation "'impl_25'" := (impl_25).
+(* Notation "'impl_25'" := (impl_25). *)
 
 Notation "'t_i16'" := (t_i16).
 
 Notation "'i16_0'" := (i16_0).
 
-Notation "'impl_19'" := (impl_19).
+(* Notation "'impl_19'" := (impl_19). *)
 
 Notation "'t_i32'" := (t_i32).
 
 Notation "'i32_0'" := (i32_0).
 
-Notation "'impl_21'" := (impl_21).
+(* Notation "'impl_21'" := (impl_21). *)
 
 Notation "'t_i64'" := (t_i64).
 
 Notation "'i64_0'" := (i64_0).
 
-Notation "'impl_23'" := (impl_23).
+(* Notation "'impl_23'" := (impl_23). *)
 
 Notation "'t_i8'" := (t_i8).
 
 Notation "'i8_0'" := (i8_0).
 
-Notation "'impl_17'" := (impl_17).
+(* Notation "'impl_17'" := (impl_17). *)
 
 Notation "'t_isize'" := (t_isize).
 
 Notation "'isize_0'" := (isize_0).
 
-Notation "'impl_27'" := (impl_27).
+(* Notation "'impl_27'" := (impl_27). *)
 
 (* NotImplementedYet *)
 
@@ -111,66 +114,66 @@ Notation "'usize_0'" := (usize_0).
 
 (* NotImplementedYet *)
 
-Notation "'impl_1'" := (impl_1).
+(* Notation "'impl_1'" := (impl_1). *)
 
-Notation "'impl_5'" := (impl_5).
+(* Notation "'impl_5'" := (impl_5). *)
 
-Notation "'impl_7'" := (impl_7).
+(* Notation "'impl_7'" := (impl_7). *)
 
-Notation "'impl_9'" := (impl_9).
+(* Notation "'impl_9'" := (impl_9). *)
 
-Notation "'impl_11'" := (impl_11).
+(* Notation "'impl_11'" := (impl_11). *)
 
-Notation "'impl_13'" := (impl_13).
+(* Notation "'impl_13'" := (impl_13). *)
 
-Notation "'impl_15'" := (impl_15).
+(* Notation "'impl_15'" := (impl_15). *)
 
-Notation "'impl'" := (impl).
+(* Notation "'impl'" := (impl). *)
 
-Notation "'impl_29'" := (impl_29).
+(* Notation "'impl_29'" := (impl_29). *)
 
-Notation "'impl_30'" := (impl_30).
+(* Notation "'impl_30'" := (impl_30). *)
 
-Notation "'impl_31'" := (impl_31).
+(* Notation "'impl_31'" := (impl_31). *)
 
-Notation "'impl_32'" := (impl_32).
+(* Notation "'impl_32'" := (impl_32). *)
 
-Notation "'impl_33'" := (impl_33).
+(* Notation "'impl_33'" := (impl_33). *)
 
-Notation "'impl_34'" := (impl_34).
+(* Notation "'impl_34'" := (impl_34). *)
 
-Notation "'impl_35'" := (impl_35).
+(* Notation "'impl_35'" := (impl_35). *)
 
-Notation "'impl_36'" := (impl_36).
+(* Notation "'impl_36'" := (impl_36). *)
 
-Notation "'impl_37'" := (impl_37).
+(* Notation "'impl_37'" := (impl_37). *)
 
-Notation "'impl_38'" := (impl_38).
+(* Notation "'impl_38'" := (impl_38). *)
 
-Notation "'impl_39'" := (impl_39).
+(* Notation "'impl_39'" := (impl_39). *)
 
-Notation "'impl_40'" := (impl_40).
+(* Notation "'impl_40'" := (impl_40). *)
 
-Notation "'impl_41'" := (impl_41).
+(* Notation "'impl_41'" := (impl_41). *)
 
-Notation "'impl_42'" := (impl_42).
+(* Notation "'impl_42'" := (impl_42). *)
 
-Notation "'impl_43'" := (impl_43).
+(* Notation "'impl_43'" := (impl_43). *)
 
-Notation "'impl_44'" := (impl_44).
+(* Notation "'impl_44'" := (impl_44). *)
 
-Notation "'impl_45'" := (impl_45).
+(* Notation "'impl_45'" := (impl_45). *)
 
-Notation "'impl_46'" := (impl_46).
+(* Notation "'impl_46'" := (impl_46). *)
 
-Notation "'impl_47'" := (impl_47).
+(* Notation "'impl_47'" := (impl_47). *)
 
-Notation "'impl_48'" := (impl_48).
+(* Notation "'impl_48'" := (impl_48). *)
 
-Notation "'impl_49'" := (impl_49).
+(* Notation "'impl_49'" := (impl_49). *)
 
-Notation "'impl_50'" := (impl_50).
+(* Notation "'impl_50'" := (impl_50). *)
 
-Notation "'impl_51'" := (impl_51).
+(* Notation "'impl_51'" := (impl_51). *)
 
-Notation "'impl_52'" := (impl_52).
+(* Notation "'impl_52'" := (impl_52). *)