diff --git a/.github/workflows/extract_and_run_coq.yml b/.github/workflows/extract_and_run_coq.yml index 8f6670e48..91be761cf 100644 --- a/.github/workflows/extract_and_run_coq.yml +++ b/.github/workflows/extract_and_run_coq.yml @@ -6,6 +6,7 @@ jobs: runs-on: ubuntu-latest container: image: coqorg/coq:8.18.0-ocaml-4.13.1-flambda + options: --user root steps: - uses: actions/checkout@v3 - name: Build diff --git a/examples/Cargo.lock b/examples/Cargo.lock index af90ddc48..668d60c74 100644 --- a/examples/Cargo.lock +++ b/examples/Cargo.lock @@ -151,6 +151,10 @@ dependencies = [ "hax-lib", ] +[[package]] +name = "coverage" +version = "0.1.0" + [[package]] name = "cpufeatures" version = "0.2.11" diff --git a/examples/coverage/proofs/coq/extraction/Coverage.v b/examples/coverage/proofs/coq/extraction/Coverage.v deleted file mode 100644 index 73677f973..000000000 --- a/examples/coverage/proofs/coq/extraction/Coverage.v +++ /dev/null @@ -1,48 +0,0 @@ -(* 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 := {}. -Instance Clone_any : forall {t_A}, t_Clone t_A := {t_Clone_f_clone := fun x => x}. - - - -(* NotImplementedYet *) - -(* NotImplementedYet *) - -(* NotImplementedYet *) - -(* NotImplementedYet *) - -(* NotImplementedYet *) - -(* NotImplementedYet *) - -(* NotImplementedYet *) diff --git a/examples/coverage/proofs/coq/extraction/Coverage_Test_closures.v b/examples/coverage/proofs/coq/extraction/Coverage_Test_closures.v deleted file mode 100644 index a085ed82d..000000000 --- a/examples/coverage/proofs/coq/extraction/Coverage_Test_closures.v +++ /dev/null @@ -1,44 +0,0 @@ -(* 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 := {}. -Instance Clone_any : forall {t_A}, t_Clone t_A := {t_Clone_f_clone := fun x => x}. - -(* Definition test__f `{v_F : Type} `{t_Sized (v_F)} `{t_FnOnce (v_F) (unit)} `{_.(t_FnOnce_f_Output) = t_u8} (g : v_F) : t_u8 := *) -(* t_Add_f_add (t_Add := _) (t_FnOnce_f_call_once (t_FnOnce := _) (g) (tt)) (Build_t_u8 (Build_t_U8 2)). *) - -(* Definition test '(_ : unit) : unit := *) -(* let add : t_i32 -> t_i32 -> t_i32 := fun x y => *) -(* t_Add_f_add (x) (y) in *) -(* let _ := Fn_f_call (fun x => *) -(* Add_f_add (x) (x)) ((2)) in *) -(* let _ := test__f (fun _ => *) -(* 23) in *) -(* tt. *) diff --git a/examples/coverage/proofs/coq/extraction/Coverage_Test_enum.v b/examples/coverage/proofs/coq/extraction/Coverage_Test_enum.v deleted file mode 100644 index d32fd0595..000000000 --- a/examples/coverage/proofs/coq/extraction/Coverage_Test_enum.v +++ /dev/null @@ -1,118 +0,0 @@ -(* 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 := {}. -Instance Clone_any : forall {t_A}, t_Clone t_A := {t_Clone_f_clone := fun x => x}. - -Record 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_Foo_Qux_record (_) (_) {_}. -Arguments Qux_f_x {_} {_} {_}. -Arguments Qux_f_y {_} {_} {_}. -Arguments Qux_f_z {_} {_} {_}. -#[export] Instance settable_Foo_Qux_record `{v_T : Type} `{v_N : t_usize} `{t_Sized (v_T)} : Settable _ := - settable! (Build_Foo_Qux_record v_T v_N) . -Inductive t_Foo `{v_T : Type} `{v_N : t_usize} `{t_Sized (v_T)} : Type := -| Foo_Bar : t_u8 -> _ -| Foo_Baz -| Foo_Qux : Foo_Qux_record v_T v_N -> _. - -Inductive t_test__AnimalA : Type := -| test__AnimalA_Dog -| 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) . -Inductive t_test__AnimalB : Type := -| test__AnimalB_Dog : t_String -> float -> _ -| test__AnimalB_Cat : test__AnimalB_Cat_record -> _. - -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) . -Inductive t_test__Enum : Type := -| test__Enum_Unit -| test__Enum_Tuple : t_u16 -> _ -| test__Enum_Struct : test__Enum_Struct_record -> _. - -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) . -Inductive t_test__Examples : Type := -| test__Examples_UnitLike -| test__Examples_TupleLike : t_i32 -> _ -| test__Examples_StructLike : test__Examples_StructLike_record -> _. - -Definition test '(_ : unit) : unit := - 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. diff --git a/examples/coverage/proofs/coq/extraction/Coverage_Test_enum_Test.v b/examples/coverage/proofs/coq/extraction/Coverage_Test_enum_Test.v deleted file mode 100644 index d2c30d4c9..000000000 --- a/examples/coverage/proofs/coq/extraction/Coverage_Test_enum_Test.v +++ /dev/null @@ -1,41 +0,0 @@ -(* 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 := {}. -Instance Clone_any : forall {t_A}, t_Clone t_A := {t_Clone_f_clone := fun x => x}. - -From Coverage Require Import Examples. -Export Examples. - -Definition discriminant_test__Enum_Struct : t_u8 := - 1. - -Definition discriminant_test__Enum_Unit : t_u8 := - 3. diff --git a/examples/coverage/proofs/coq/extraction/Coverage_Test_functions.v b/examples/coverage/proofs/coq/extraction/Coverage_Test_functions.v deleted file mode 100644 index 6b18c8c9e..000000000 --- a/examples/coverage/proofs/coq/extraction/Coverage_Test_functions.v +++ /dev/null @@ -1,50 +0,0 @@ -(* 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 := {}. -Instance Clone_any : forall {t_A}, t_Clone t_A := {t_Clone_f_clone := fun x => x}. - -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. diff --git a/examples/coverage/proofs/coq/extraction/Coverage_Test_primitives.v b/examples/coverage/proofs/coq/extraction/Coverage_Test_primitives.v deleted file mode 100644 index 4aa5c8a02..000000000 --- a/examples/coverage/proofs/coq/extraction/Coverage_Test_primitives.v +++ /dev/null @@ -1,53 +0,0 @@ -(* 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 := {}. -Instance Clone_any : forall {t_A}, t_Clone t_A := {t_Clone_f_clone := fun x => x}. - -Definition test '(_ : unit) : unit := - let _ : bool := false in - let _ : bool := true in - let _ : t_u8 := 12 in - let _ : t_u16 := 123 in - let _ : t_u32 := 1234 in - let _ : t_u64 := 12345 in - let _ : t_u128 := 123456 in - let _ : t_usize := 32 in - let _ : t_i8 := -12 in - let _ : t_i16 := 123 in - let _ : t_i32 := -1234 in - let _ : t_i64 := 12345 in - let _ : t_i128 := 123456 in - let _ : t_isize := -32 in - let _ : float := 1.2%float in - let _ : float := (-1.23)%float in - let _ : ascii := "c"%char in - let _ : string := "hello world"%string in - tt. diff --git a/examples/coverage/proofs/coq/extraction/Coverage_Test_sequence.v b/examples/coverage/proofs/coq/extraction/Coverage_Test_sequence.v deleted file mode 100644 index dd8ecb148..000000000 --- a/examples/coverage/proofs/coq/extraction/Coverage_Test_sequence.v +++ /dev/null @@ -1,45 +0,0 @@ -(* 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 := {}. -Instance Clone_any : forall {t_A}, t_Clone t_A := {t_Clone_f_clone := fun x => x}. - -Definition test '(_ : unit) : unit := - let _ : unit := tt in - let _ : (t_u8*t_u16*t_i8) := (1,2,3) in - let _ : t_u8 := (fst(1,2)) in - let _ : t_u8 := (1) in - let _ : t_u8 := (snd(fst(1,2,3,4,5))) in - let _ : t_Array (t_u8) (0) := [] in - let _ : t_Array (string) (3) := ["23"%string; "a"%string; "hllo"%string] in - let _ : t_Array (t_u8) (14) := repeat (2) (14) in - let _ : t_Slice t_u8 := unsize ([1; 2; 3; 4]) in - let _ : t_Slice string := unsize ([]) in - tt. diff --git a/examples/coverage/proofs/coq/extraction/Coverage_Test_struct.v b/examples/coverage/proofs/coq/extraction/Coverage_Test_struct.v deleted file mode 100644 index 984908e8b..000000000 --- a/examples/coverage/proofs/coq/extraction/Coverage_Test_struct.v +++ /dev/null @@ -1,149 +0,0 @@ -(* 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 := {}. -Instance Clone_any : forall {t_A}, t_Clone t_A := {t_Clone_f_clone := fun x => x}. - -Record t_foo (v_T : Type) (v_N : t_usize) `{t_Sized (v_T)} : Type := - { - foo_f_bar : v_T; - foo_f_baz : t_Array (v_T) (v_N); - foo_f_qux : t_u8; - }. -Arguments Build_t_foo (_) (_) {_}. -Arguments foo_f_bar {_} {_} {_}. -Arguments foo_f_baz {_} {_} {_}. -Arguments foo_f_qux {_} {_} {_}. -#[export] Instance settable_t_foo `{v_T : Type} `{v_N : t_usize} `{t_Sized (v_T)} : Settable _ := - settable! (Build_t_foo v_T v_N) . - -Record t_test__Color : Type := - { - test__Color_0 : t_u8; - test__Color_1 : t_u8; - test__Color_2 : t_u8; - }. -Arguments Build_t_test__Color. -Arguments test__Color_0. -Arguments test__Color_1. -Arguments test__Color_2. -#[export] Instance settable_t_test__Color : Settable _ := - settable! (Build_t_test__Color) . -Notation "'test__Color'" := Build_t_test__Color. - -Record t_test__Cookie : Type := - { - }. -Arguments Build_t_test__Cookie. -#[export] -Notation "'test__Cookie'" := Build_t_test__Cookie. - -Record t_test__CookieA : Type := - { - }. -Arguments Build_t_test__CookieA. -#[export] -Notation "'test__CookieA'" := Build_t_test__CookieA. - -Record t_test__Gamma : Type := - { - }. -Arguments Build_t_test__Gamma. -#[export] -Notation "'test__Gamma'" := Build_t_test__Gamma. - -Record t_test__PointA : Type := - { - test__PointA_f_x : t_i32; - test__PointA_f_y : t_i32; - }. -Arguments Build_t_test__PointA. -Arguments test__PointA_f_x. -Arguments test__PointA_f_y. -#[export] Instance settable_t_test__PointA : Settable _ := - settable! (Build_t_test__PointA) . - -Record t_test__PointB : Type := - { - test__PointB_0 : t_i32; - test__PointB_1 : t_i32; - }. -Arguments Build_t_test__PointB. -Arguments test__PointB_0. -Arguments test__PointB_1. -#[export] Instance settable_t_test__PointB : Settable _ := - settable! (Build_t_test__PointB) . -Notation "'test__PointB'" := Build_t_test__PointB. - -Record t_test__Position : Type := - { - test__Position_0 : t_i32; - test__Position_1 : t_i32; - test__Position_2 : t_i32; - }. -Arguments Build_t_test__Position. -Arguments test__Position_0. -Arguments test__Position_1. -Arguments test__Position_2. -#[export] Instance settable_t_test__Position : Settable _ := - settable! (Build_t_test__Position) . -Notation "'test__Position'" := Build_t_test__Position. - -Definition test__Cookie : t_test__Cookie := - Build_t_test__Cookie. - -Definition test '(_ : unit) : unit := - let a := Build_t_test__Gamma in - let b := Build_t_test__Gamma in - let _ := tt in - let _ := Build_t_test__Position (0) (0) (0) in - let c := Build_t_test__Position in - let pos := test__Position (8) (6) (7) in - let _ := tt in - let c1 := Build_t_test__Color (0) (0) (0) in - let c2 := Build_t_test__Color (255) (127) (0) in - let c3 := Build_t_test__Color (0) in - let _ := tt in - let p := Build_t_test__PointA (10) (11) in - let px : t_i32 := test__PointA_f_x p in - let p2 := Build_t_test__PointA (10) (11) in - let p2 := p2 <|test__PointA_f_x := 10 |> in - let p2 := p2 <|test__PointA_f_y := 14 |> in - let _ := tt in - let p := Build_t_test__PointB (10) (11) in - let px : t_i32 := match p with - | Build_t_test__PointB x _ => - x - end in - let _ := tt in - let c := [Build_t_test__CookieA; Build_t_test__CookieA; Build_t_test__CookieA; Build_t_test__CookieA] in - let _ := tt in - let c := [test__Cookie; Build_t_test__Cookie; test__Cookie; Build_t_test__Cookie] in - tt. diff --git a/examples/coverage/proofs/coq/extraction/_CoqProject b/examples/coverage/proofs/coq/extraction/_CoqProject deleted file mode 100644 index 636260f7a..000000000 --- a/examples/coverage/proofs/coq/extraction/_CoqProject +++ /dev/null @@ -1,11 +0,0 @@ --R ./ Core --arg -w --arg all - -./Coverage_Test_closures.v -./Coverage_Test_enum.v -./Coverage_Test_functions.v -./Coverage_Test_primitives.v -./Coverage_Test_sequence.v -./Coverage_Test_struct.v -./Coverage.v