WIP

.github/workflows/extract_and_run_coq.yml

@@ -16,7 +16,6 @@ jobs:
         env
         opam switch 4.13.1+flambda
         eval $(opam env)
-        ./setup.sh
         cd examples/coverage
         cargo hax into coq
         cd proofs/coq/extraction

examples/coverage/proofs/coq/extraction/Coverage.v

@@ -0,0 +1,53 @@
+(* 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.
+
+(* From Core Require Import Core. *)
+
+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.
+
+
+
+(* NotImplementedYet *)
+
+(* NotImplementedYet *)
+
+(* NotImplementedYet *)
+
+(* NotImplementedYet *)
+
+(* NotImplementedYet *)
+
+(* NotImplementedYet *)
+
+(* NotImplementedYet *)
+
+(* NotImplementedYet *)

examples/coverage/proofs/coq/extraction/Coverage_Test_enum.v

@@ -0,0 +1,136 @@
+(* 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.
+
+(* From Core Require Import Core. *)
+
+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.
+
+Inductive t_test__AnimalA : Type :=
+| test__AnimalA_Dog
+| test__AnimalA_Cat.
+Arguments test__AnimalA_Dog.
+Arguments test__AnimalA_Cat.
+
+Definition t_test__AnimalA_cast_to_repr (x : t_test__AnimalA) : t_isize :=
+  match x with
+  | test__AnimalA_Dog =>
+    0
+  | test__AnimalA_Cat =>
+    1
+  end.
+
+Record test__AnimalB_Cat_record : Type :=
+  {
+    Cat_f_name : t_String;
+    Cat_f_weight : float;
+  }.
+Arguments Build_test__AnimalB_Cat_record.
+Arguments Cat_f_name.
+Arguments Cat_f_weight.
+#[export] Instance settable_test__AnimalB_Cat_record : Settable _ :=
+  settable! (Build_test__AnimalB_Cat_record) <Cat_f_name; Cat_f_weight>.
+Inductive t_test__AnimalB : Type :=
+| test__AnimalB_Dog : t_String -> float -> _
+| test__AnimalB_Cat : test__AnimalB_Cat_record  -> _.
+Arguments test__AnimalB_Dog.
+Arguments test__AnimalB_Cat.
+
+Record test__Enum_Struct_record : Type :=
+  {
+    Struct_f_a : t_u8;
+    Struct_f_b : t_u16;
+  }.
+Arguments Build_test__Enum_Struct_record.
+Arguments Struct_f_a.
+Arguments Struct_f_b.
+#[export] Instance settable_test__Enum_Struct_record : Settable _ :=
+  settable! (Build_test__Enum_Struct_record) <Struct_f_a; Struct_f_b>.
+Inductive t_test__Enum : Type :=
+| test__Enum_Unit
+| test__Enum_Tuple : t_u16 -> _
+| test__Enum_Struct : test__Enum_Struct_record  -> _.
+Arguments test__Enum_Unit.
+Arguments test__Enum_Tuple.
+Arguments test__Enum_Struct.
+
+Record test__Examples_StructLike_record : Type :=
+  {
+    StructLike_f_value : t_i32;
+  }.
+Arguments Build_test__Examples_StructLike_record.
+Arguments StructLike_f_value.
+#[export] Instance settable_test__Examples_StructLike_record : Settable _ :=
+  settable! (Build_test__Examples_StructLike_record) <StructLike_f_value>.
+Inductive t_test__Examples : Type :=
+| test__Examples_UnitLike
+| test__Examples_TupleLike : t_i32 -> _
+| test__Examples_StructLike : test__Examples_StructLike_record  -> _.
+Arguments test__Examples_UnitLike.
+Arguments test__Examples_TupleLike.
+Arguments test__Examples_StructLike.
+
+Record test__Foo_Qux_record (v_T : Type) (v_N : t_usize) `{t_Sized (v_T)} : Type :=
+  {
+    Qux_f_x : v_T;
+    Qux_f_y : t_Array (v_T) (v_N);
+    Qux_f_z : t_u8;
+  }.
+Arguments Build_test__Foo_Qux_record (_) (_) {_}.
+Arguments Qux_f_x {_} {_} {_}.
+Arguments Qux_f_y {_} {_} {_}.
+Arguments Qux_f_z {_} {_} {_}.
+#[export] Instance settable_test__Foo_Qux_record `{v_T : Type} `{v_N : t_usize} `{t_Sized (v_T)} : Settable _ :=
+  settable! (Build_test__Foo_Qux_record v_T v_N) <Qux_f_x; Qux_f_y; Qux_f_z>.
+Inductive t_test__Foo (v_T : Type) (v_N : t_usize) `{t_Sized (v_T)} : Type :=
+| test__Foo_Bar : t_u8 -> _
+| test__Foo_Baz
+| test__Foo_Qux : test__Foo_Qux_record  v_T v_N -> _.
+Arguments test__Foo_Bar {_} {_} {_}.
+Arguments test__Foo_Baz {_} {_} {_}.
+Arguments test__Foo_Qux {_} {_} {_}.
+
+Definition test '(_ : unit) : unit :=
+  let x : t_test__Foo ((t_u8)) (12) := test__Foo_Baz in
+  let _ := tt in
+  let a : t_test__AnimalA := test__AnimalA_Dog in
+  let a := test__AnimalA_Cat in
+  let _ := tt in
+  let a : t_test__AnimalB := test__AnimalB_Dog (ToString_f_to_string ("Cocoa"%string)) (37.2%float) in
+  let a := test__AnimalB_Cat {| Cat_f_name := (ToString_f_to_string ("Spotty"%string)); Cat_f_weight := (2.7%float) |} in
+  let _ := tt in
+  let x := test__Examples_UnitLike in
+  let x := test__Examples_UnitLike in
+  let y := test__Examples_TupleLike (123) in
+  let y := test__Examples_TupleLike (123) in
+  let z := test__Examples_StructLike {| StructLike_f_value := (123) |} in
+  let _ := tt in
+  tt.

examples/coverage/proofs/coq/extraction/Coverage_Test_enum_Test.v

@@ -0,0 +1,41 @@
+(* 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.
+
+(* From Core Require Import Core. *)
+
+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 discriminant_test__Enum_Struct : t_u8 :=
+  1.
+
+Definition discriminant_test__Enum_Unit : t_u8 :=
+  3.

examples/coverage/proofs/coq/extraction/Coverage_Test_functions.v

@@ -0,0 +1,53 @@
+(* 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.
+
+(* From Core Require Import Core. *)
+
+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 first `{v_A : Type} `{v_B : Type} `{t_Sized (v_A)} `{t_Sized (v_B)} `{t_Clone (v_B)} '((value,_) : (v_A*t_i32)) (y : v_B) : v_A :=
+  value.
+
+Definition foo1 `{v_A : Type} `{v_B : Type} `{t_Sized (v_A)} `{t_Sized (v_B)} (x : v_A) (y : v_B) : unit :=
+  tt.
+
+Definition foo2 `{v_T : Type} `{t_Sized (v_T)} `{t_Clone (v_T)} (x : t_Slice v_T) (y : t_Array (v_T) (1)) : unit :=
+  tt.
+
+Definition foo3 '(_ : unit) : unit :=
+  tt.
+
+Definition test '(_ : unit) : unit :=
+  let x := [1] in
+  let _ := foo2 (unsize (x)) (x) in
+  let _ := foo2 (unsize ([1; 2])) (x) in
+  tt.

examples/coverage/proofs/coq/extraction/Coverage_Test_instance.v

@@ -0,0 +1,58 @@
+(* 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.
+
+(* From Core Require Import Core. *)
+
+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.
+
+Inductive t_SomeEnum (v_T : Type) `{t_Sized (v_T)} : Type :=
+| SomeEnum_None
+| SomeEnum_Some : v_T -> _.
+Arguments SomeEnum_None {_} {_}.
+Arguments SomeEnum_Some {_} {_}.
+
+Class t_SomeTrait (v_Self : Type) : Type :=
+  {
+    SomeTrait_f_some_fun : v_Self -> v_Self;
+  }.
+Arguments t_SomeTrait (_).
+
+Instance t_SomeTrait_153652929 `{v_T : Type} `{t_Sized (v_T)} `{t_SomeTrait (v_T)} : t_SomeTrait ((t_SomeEnum ((v_T)))) :=
+  {
+    SomeTrait_impl_f_some_fun := fun  (self : t_SomeEnum ((v_T)))=>
+      match self with
+      | SomeEnum_Some x =>
+        SomeEnum_Some (SomeTrait_f_some_fun (x))
+      | SomeEnum_None =>
+        SomeEnum_None
+      end;
+  }.