Add a test

.github/workflows/coq-hacspec-ssprove-lib.yml

@@ -32,7 +32,7 @@ jobs:
           custom_image: ${{ matrix.image }}
       - after_script: |
           startGroup "Run ssprove coq library tests"
-            make test
+            coqc ./tests/enum-repr/proofs/ssprove/extraction/Enum_repr.v
           endGroup "Run ssprove coq library tests"
 
 # See also:

engine/backends/coq/ssprove/ssprove_backend.ml

@@ -2372,8 +2372,6 @@ let hardcoded_coq_headers =
    From Crypt Require Import choice_type Package Prelude.\n\
    Import PackageNotation.\n\
    From extructures Require Import ord fset.\n\
-   From mathcomp Require Import word_ssrZ word.\n\
-   From Jasmin Require Import word.\n\n\
    From Coq Require Import ZArith.\n\
    From Coq Require Import Strings.String.\n\
    Import List.ListNotations.\n\

proof-libs/coq/ssprove/src/ChoiceEquality.v

@@ -209,11 +209,11 @@ Ltac solve_match :=
    | |- context [ fsubset ?a (_ :|: ?a) ] => apply fsubsetUr
    | |- context [ fsubset fset0 _ ] => apply fsub0set
    | |- context [ fsubset ?a ?a ] => apply fsubsetxx
+   (* | |- context [ fsubset ?a (?b :|: _) ] => assert (a = b) by reflexivity ; apply fsubsetUl *)
+   (* | |- context [ fsubset ?a (_ :|: ?b) ] => assert (a = b) by reflexivity ; apply fsubsetUr *)
+   (* | |- context [ fsubset ?a _ ] => assert (a = fset0) by reflexivity ; apply fsub0set *)
+   (* | |- context [fsubset ?a ?b ] => assert (a = b) by reflexivity ; apply fsubsetxx *)
    end).
-(* || (progress (try apply fsubsetUl ; *)
-(*                    try apply fsubsetUr ; *)
-(*                    try apply fsub0set ; *)
-(*                    try apply fsubsetxx)) *)
 
 Ltac split_fsubset_lhs :=
   repeat (rewrite !is_true_split_and || rewrite !fsubUset) ;

proof-libs/coq/ssprove/src/Hacspec_Lib_Ltac.v

@@ -249,11 +249,14 @@ Ltac solve_in_mem :=
 Ltac solve_ssprove_obligations :=
   repeat (
       intros ; autounfold ; normalize_fset ;
-      (now solve_in_mem) (* TODO: add match goal *)
-      || (now fset_equality) (* TODO: add match goal *)
-      || (now solve_in_fset) (* TODO: add match goal *)
-      || (ssprove_valid'_2)
-      || ((now (* try *) (Tactics.program_simpl; fail)))).
+      now (solve_match || now (apply fsubsetxx || apply fsub0set)
+           || solve_in_mem (* TODO: add match goal *)
+           || fset_equality (* TODO: add match goal *)
+           || solve_in_fset (* TODO: add match goal *)
+           || ssprove_valid'_2
+           || now apply fsubsetUl
+           || now apply fsubsetUr
+           || (Tactics.program_simpl; fail))).
 
 Ltac solve_fsubset_trans :=
   now (solve_match || (refine (fsubset_trans _ _) ; [ | eassumption ] ; solve_ssprove_obligations)).

tests/enum-repr/proofs/ssprove/extraction/Enum_repr.v

@@ -0,0 +1,110 @@
+(* File automatically generated by Hacspec *)
+Set Warnings "-notation-overridden,-ambiguous-paths".
+From Crypt Require Import choice_type Package Prelude.
+Import PackageNotation.
+From extructures Require Import ord fset.
+
+From Coq Require Import ZArith.
+From Coq Require Import Strings.String.
+Import List.ListNotations.
+Open Scope list_scope.
+Open Scope Z_scope.
+Open Scope bool_scope.
+
+From Crypt Require Import jasmin_word.
+
+From Hacspec Require Import ChoiceEquality.
+From Hacspec Require Import LocationUtility.
+From Hacspec Require Import Hacspec_Lib_Comparable.
+From Hacspec Require Import Hacspec_Lib_Pre.
+From Hacspec Require Import Hacspec_Lib.
+
+Open Scope hacspec_scope.
+Import choice.Choice.Exports.
+
+Obligation Tactic := (* try timeout 8 *) solve_ssprove_obligations.
+
+Equations discriminant_EnumWithRepr_ExplicitDiscr1 {L : {fset Location}} {I : Interface} : both L I int16 :=
+  discriminant_EnumWithRepr_ExplicitDiscr1  :=
+    solve_lift (ret_both (1 : int16)) : both L I int16.
+Fail Next Obligation.
+
+Equations discriminant_EnumWithRepr_ExplicitDiscr2 {L : {fset Location}} {I : Interface} : both L I int16 :=
+  discriminant_EnumWithRepr_ExplicitDiscr2  :=
+    solve_lift (ret_both (5 : int16)) : both L I int16.
+Fail Next Obligation.
+
+Definition t_EnumWithRepr : choice_type :=
+  ('unit ∐ 'unit ∐ 'unit ∐ 'unit).
+Notation "'EnumWithRepr_ExplicitDiscr1_case'" := (inl (inl (inl tt))) (at level 100).
+Equations EnumWithRepr_ExplicitDiscr1 {L : {fset Location}} {I : Interface} : both L I t_EnumWithRepr :=
+  EnumWithRepr_ExplicitDiscr1  :=
+    solve_lift (ret_both (inl (inl (inl (tt : 'unit))) : t_EnumWithRepr)) : both L I t_EnumWithRepr.
+Fail Next Obligation.
+Notation "'EnumWithRepr_ExplicitDiscr2_case'" := (inl (inl (inr tt))) (at level 100).
+Equations EnumWithRepr_ExplicitDiscr2 {L : {fset Location}} {I : Interface} : both L I t_EnumWithRepr :=
+  EnumWithRepr_ExplicitDiscr2  :=
+    solve_lift (ret_both (inl (inl (inr (tt : 'unit))) : t_EnumWithRepr)) : both L I t_EnumWithRepr.
+Fail Next Obligation.
+Notation "'EnumWithRepr_ImplicitDiscrEmptyTuple_case'" := (inl (inr tt)) (at level 100).
+Equations EnumWithRepr_ImplicitDiscrEmptyTuple {L : {fset Location}} {I : Interface} : both L I t_EnumWithRepr :=
+  EnumWithRepr_ImplicitDiscrEmptyTuple  :=
+    solve_lift (ret_both (inl (inr (tt : 'unit)) : t_EnumWithRepr)) : both L I t_EnumWithRepr.
+Fail Next Obligation.
+Notation "'EnumWithRepr_ImplicitDiscrEmptyStruct_case'" := (inr tt) (at level 100).
+Equations EnumWithRepr_ImplicitDiscrEmptyStruct {L : {fset Location}} {I : Interface} : both L I t_EnumWithRepr :=
+  EnumWithRepr_ImplicitDiscrEmptyStruct  :=
+    solve_lift (ret_both (inr (tt : 'unit) : t_EnumWithRepr)) : both L I t_EnumWithRepr.
+Fail Next Obligation.
+
+Ltac solve_ssprove_obligations :=
+  repeat (
+      intros ; autounfold ; normalize_fset ;
+      now (solve_match || now (apply fsubsetxx || apply fsub0set)
+           || solve_in_mem (* TODO: add match goal *)
+           || fset_equality (* TODO: add match goal *)
+           || solve_in_fset (* TODO: add match goal *)
+           || ssprove_valid'_2
+           || now apply fsubsetUl
+           || now apply fsubsetUr
+           || (Tactics.program_simpl; fail))).
+
+Obligation Tactic := (* try timeout 8 *) solve_ssprove_obligations.
+
+Equations t_EnumWithRepr_cast_to_repr {L1 : {fset Location}} {I1 : Interface} (x : both L1 I1 t_EnumWithRepr) : both L1 I1 int16 :=
+  t_EnumWithRepr_cast_to_repr x  := 
+    matchb x with
+    | EnumWithRepr_ExplicitDiscr1_case  =>
+      solve_lift discriminant_EnumWithRepr_ExplicitDiscr1
+    | EnumWithRepr_ExplicitDiscr2_case  =>
+      solve_lift discriminant_EnumWithRepr_ExplicitDiscr2
+    | EnumWithRepr_ImplicitDiscrEmptyTuple_case  =>
+      solve_lift (discriminant_EnumWithRepr_ExplicitDiscr2 .+ (ret_both (1 : int16)))
+    | EnumWithRepr_ImplicitDiscrEmptyStruct_case  =>
+      solve_lift (discriminant_EnumWithRepr_ExplicitDiscr2 .+ (ret_both (2 : int16)))
+    end : both L1 I1 int16.
+Fail Next Obligation.
+
+(*Not implemented yet? todo(item)*)
+
+Equations f {L1 : {fset Location}} {I1 : Interface} (_ : both L1 I1 'unit) : both L1 I1 int32 :=
+  f _  :=
+    letb v__x := cast_int (WS2 := U32) (discriminant_EnumWithRepr_ExplicitDiscr2 .+ (ret_both (0 : int16))) in
+    solve_lift ((cast_int (WS2 := U32) (t_EnumWithRepr_cast_to_repr EnumWithRepr_ImplicitDiscrEmptyTuple)) .+ (cast_int (WS2 := U32) (t_EnumWithRepr_cast_to_repr EnumWithRepr_ImplicitDiscrEmptyStruct))) : both L1 I1 int32.
+Next Obligation.
+Fail Next Obligation.
+
+Equations ff__CONST {L : {fset Location}} {I : Interface} : both L I int16 :=
+  ff__CONST  :=
+    solve_lift (cast_int (WS2 := _) (discriminant_EnumWithRepr_ExplicitDiscr1 .+ (ret_both (0 : int16)))) : both L I int16.
+Fail Next Obligation.
+
+Equations get_casted_repr {L1 : {fset Location}} {I1 : Interface} (x : both L1 I1 t_EnumWithRepr) : both L1 I1 int64 :=
+  get_casted_repr x  :=
+    solve_lift (cast_int (WS2 := _) (t_EnumWithRepr_cast_to_repr x)) : both L1 I1 int64.
+Fail Next Obligation.
+
+Equations get_repr {L1 : {fset Location}} {I1 : Interface} (x : both L1 I1 t_EnumWithRepr) : both L1 I1 int16 :=
+  get_repr x  :=
+    solve_lift (t_EnumWithRepr_cast_to_repr x) : both L1 I1 int16.
+Fail Next Obligation.