CI for coq coverage

.github/workflows/extract_and_run_coq.yml

@@ -0,0 +1,29 @@
+name: Extract and Run - Coq
+
+on: [pull_request]
+jobs:
+  extract-bertie:
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v4
+        with:
+          path: hax
+
+      - uses: DeterminateSystems/nix-installer-action@main
+      - uses: DeterminateSystems/magic-nix-cache-action@main
+
+      - name: ⤵ Install hax
+        run: |
+          nix profile install --verbose ./hax
+
+      - name: build coverage example
+        working-directory: hax/examples/coverage
+        run: |
+          nix run . into coq
+
+      - name: run coq
+        working-directory: hax/examples/coverage/proofs/coq/extraction
+        run: |
+          sed 's/_impl_f_/_f_/' < Coverage_Test_instance.v > Coverage_Test_instance.v
+          nix-shell --packages coq coqPackages.coq-record-update --run "coq_makefile -f _CoqProject -o Makefile"
+          nix-shell --packages coq coqPackages.coq-record-update --run "make"

engine/backends/coq/coq/coq_backend.ml

@@ -116,7 +116,7 @@ let hardcoded_coq_headers =
    Require Import Coq.Floats.Floats.\n\
    From RecordUpdate Require Import RecordSet.\n\
    Import RecordSetNotations.\n\n\
-   From Core Require Import Core.\n"
+   (* From Core Require Import Core. *)\n"
 
 let dummy_lib =
   "Class t_Sized (T : Type) := { }.\n\
@@ -136,8 +136,11 @@ let dummy_lib =
    Definition t_String := string.\n\
    Definition ToString_f_to_string (x : string) := x.\n\
    Instance Sized_any : forall {t_A}, t_Sized t_A := {}.\n\
-   Instance Clone_any : forall {t_A}, t_Clone t_A := {t_Clone_f_clone := fun x \
-   => x}.\n"
+   Class t_Clone (T : Type) := { Clone_f_clone : T -> T }.\n\
+   Instance Clone_any : forall {t_A}, t_Clone t_A := {Clone_f_clone := fun x \
+   => x}.\n\
+   Definition t_Slice (T : Type) := list T.\n\
+   Definition unsize {T : Type} : list T -> t_Slice T := id.\n"
 
 module BasePrinter = Generic_printer.Make (InputLanguage)
 
@@ -435,7 +438,7 @@ struct
       method impl_ident ~goal ~name:_ = goal#p
 
       method impl_item ~ii_span:_ ~ii_generics:_ ~ii_v ~ii_ident ~ii_attrs:_ =
-        string (String.chop_prefix_exn ~prefix:"impl_" (U.Concrete_ident_view.to_definition_name ii_ident#v)) ^^ space ^^ string ":=" ^^ space ^^ ii_v#p ^^ semi
+        ii_ident#p ^^ space ^^ string ":=" ^^ space ^^ ii_v#p ^^ semi
 
       method impl_item'_IIFn ~body ~params =
         if List.length params == 0 then body#p
@@ -527,7 +530,13 @@ struct
           (braces
              (nest 2
                 (concat_map_with
-                   ~pre:(break 1 ^^ string (String.drop_prefix (U.Concrete_ident_view.to_definition_name name#v) 2) ^^ !^"_")
+                   ~pre:
+                     (break 1
+                     ^^ string
+                          (String.drop_prefix
+                             (U.Concrete_ident_view.to_definition_name name#v)
+                             2)
+                     ^^ !^"_")
                    (fun x -> x#p)
                    items)
              ^^ break 1))
@@ -539,12 +548,10 @@ struct
 
       method item'_Trait ~super:_ ~name ~generics ~items ~safety:_ =
         let _, params, constraints = generics#v in
-        CoqNotation.class_ name#p (concat_map_with ~pre:space
-             (fun x -> parens x#p)
-             params
-          ^^ concat_map_with ~pre:space
-               (fun x -> x#p)
-               constraints) [] !^"Type"
+        CoqNotation.class_ name#p
+          (concat_map_with ~pre:space (fun x -> parens x#p) params
+          ^^ concat_map_with ~pre:space (fun x -> x#p) constraints)
+          [] !^"Type"
           (braces
              (nest 2 (concat_map_with ~pre:(break 1) (fun x -> x#p) items)
              ^^ break 1))
@@ -989,9 +996,7 @@ let translate m _ ~bundles:_ (items : AST.item list) : Types.file list =
            {
              path = mod_name ^ ".v";
              contents =
-               hardcoded_coq_headers ^ "\n"
-               (* ^ dummy_lib ^ "\n" *)
-               ^ contents;
+               hardcoded_coq_headers ^ "\n" ^ dummy_lib ^ "\n" ^ contents;
              sourcemap = None;
            }))
   @ [

engine/lib/concrete_ident/concrete_ident.ml

@@ -244,7 +244,7 @@ module View = struct
     let string_of_def_path_item : Imported.def_path_item -> string option =
       function
       | TypeNs s | ValueNs s | MacroNs s | LifetimeNs s -> Some s
-      | Impl ->  Some "impl"
+      | Impl -> Some "impl"
       | AnonConst -> Some "anon_const"
       | _ -> None
 
@@ -560,6 +560,8 @@ let to_debug_string = T.show
 let map_path_strings ~(f : string -> string) (cid : t) : t =
   { cid with def_id = Imported.map_path_strings ~f cid.def_id }
 
+let parent (cid : t) : t = { cid with def_id = Imported.parent cid.def_id }
+
 module DefaultNamePolicy = struct
   let reserved_words = Hash_set.create (module String)
   let index_field_transform = Fn.id
@@ -649,3 +651,15 @@ let parent_impl (id : t) : t option =
 
 module DefaultViewAPI = MakeViewAPI (DefaultNamePolicy)
 include DefaultViewAPI
+
+let remove_impl old =
+  let new_parent = (parent (parent old)).def_id in
+  {
+    kind = Macro;
+    (* Field; *)
+    def_id =
+      {
+        new_parent with
+        path = new_parent.path @ [ List.last_exn old.def_id.path ];
+      };
+  }

engine/lib/concrete_ident/concrete_ident.mli

@@ -74,3 +74,6 @@ identifier points to an [Impl] block. *)
 val parent_impl : t -> t option
 (** Returns the identifier pointing to the parent `impl` block, if it
 exists. *)
+
+val remove_impl : t -> t
+(** Returns the parent *)

examples/Cargo.toml

@@ -6,7 +6,8 @@ members = [
     "barrett",
     "kyber_compress",
     "proverif-psk",
-    "coq-example"]
+    "coq-example",
+    "coverage"]
 resolver = "2"
 
 [workspace.dependencies]

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

@@ -10,7 +10,7 @@ Require Import Coq.Floats.Floats.
 From RecordUpdate Require Import RecordSet.
 Import RecordSetNotations.
 
-From Core Require Import Core.
+(* From Core Require Import Core. *)
 
 Class t_Sized (T : Type) := { }.
 Definition t_u8 := Z.
@@ -29,7 +29,10 @@ 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}.
+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.
 
 
 
@@ -46,3 +49,5 @@ Instance Clone_any : forall {t_A}, t_Clone t_A := {t_Clone_f_clone := fun x => x
 (* NotImplementedYet *)
 
 (* NotImplementedYet *)
+
+(* NotImplementedYet *)

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

@@ -10,7 +10,7 @@ Require Import Coq.Floats.Floats.
 From RecordUpdate Require Import RecordSet.
 Import RecordSetNotations.
 
-From Core Require Import Core.
+(* From Core Require Import Core. *)
 
 Class t_Sized (T : Type) := { }.
 Definition t_u8 := Z.
@@ -29,28 +29,16 @@ 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) <Qux_f_x; Qux_f_y; Qux_f_z>.
-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 -> _.
+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
@@ -73,6 +61,8 @@ Arguments 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 :=
   {
@@ -88,6 +78,9 @@ 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 :=
   {
@@ -101,8 +94,33 @@ 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

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

@@ -10,7 +10,7 @@ Require Import Coq.Floats.Floats.
 From RecordUpdate Require Import RecordSet.
 Import RecordSetNotations.
 
-From Core Require Import Core.
+(* From Core Require Import Core. *)
 
 Class t_Sized (T : Type) := { }.
 Definition t_u8 := Z.
@@ -29,10 +29,10 @@ 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.
+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.

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

@@ -10,7 +10,7 @@ Require Import Coq.Floats.Floats.
 From RecordUpdate Require Import RecordSet.
 Import RecordSetNotations.
 
-From Core Require Import Core.
+(* From Core Require Import Core. *)
 
 Class t_Sized (T : Type) := { }.
 Definition t_u8 := Z.
@@ -29,7 +29,10 @@ 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}.
+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.