Working example

hacspec · Mar 18, 2024 · 83ce316 · 83ce316
1 parent 7961346
commit 83ce316
Show file tree

Hide file tree

Showing 4 changed files with 14 additions and 30 deletions.
diff --git a/engine/backends/coq/ssprove/ssprove_backend.ml b/engine/backends/coq/ssprove/ssprove_backend.ml
@@ -2378,6 +2378,7 @@ let hardcoded_coq_headers =
    Open Scope list_scope.\n\
    Open Scope Z_scope.\n\
    Open Scope bool_scope.\n\n\
+   From Crypt Require Import jasmin_word.\n\n\
    From Hacspec Require Import ChoiceEquality.\n\
    From Hacspec Require Import LocationUtility.\n\
    From Hacspec Require Import Hacspec_Lib_Comparable.\n\

diff --git a/proof-libs/coq/ssprove/src/ChoiceEquality.v b/proof-libs/coq/ssprove/src/ChoiceEquality.v
@@ -204,16 +204,18 @@ Ltac normalize_fset :=
 
 Ltac solve_match :=
   try set (fset _) ;
-  (lazymatch (* match *) goal with
-   | |- context [ fsubset ?a (?a :|: _) ] => apply fsubsetUl
-   | |- 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).
+  (apply fsub0set
+   || apply fsubsetxx
+   || (lazymatch (* match *) goal with
+      | |- context [ fsubset ?a (?a :|: _) ] => apply fsubsetUl
+      | |- 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)).
 
 Ltac split_fsubset_lhs :=
   repeat (rewrite !is_true_split_and || rewrite !fsubUset) ;

diff --git a/proof-libs/coq/ssprove/src/Hacspec_Lib_Ltac.v b/proof-libs/coq/ssprove/src/Hacspec_Lib_Ltac.v
@@ -254,8 +254,6 @@ Ltac solve_ssprove_obligations :=
            || 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 :=

diff --git a/tests/enum-repr/proofs/ssprove/extraction/Enum_repr.v b/tests/enum-repr/proofs/ssprove/extraction/Enum_repr.v
@@ -57,22 +57,8 @@ Equations EnumWithRepr_ImplicitDiscrEmptyStruct {L : {fset Location}} {I : Inter
     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  := 
+  t_EnumWithRepr_cast_to_repr x  :=
     matchb x with
     | EnumWithRepr_ExplicitDiscr1_case  =>
       solve_lift discriminant_EnumWithRepr_ExplicitDiscr1
@@ -85,13 +71,10 @@ Equations t_EnumWithRepr_cast_to_repr {L1 : {fset Location}} {I1 : Interface} (x
     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 :=