WIP

cryspen · Apr 3, 2024 · 9f289da · 9f289da
1 parent 7599e84
commit 9f289da
Show file tree

Hide file tree

Showing 11 changed files with 337 additions and 211 deletions.
diff --git a/engine/backends/coq/coq_ast.ml b/engine/backends/coq/coq_ast.ml
@@ -131,7 +131,7 @@ functor
         | ModuleType of string * argument list * record_field list
         | Module of string * string * argument list * record_field list
         | Parameter of string * ty (* definition_type minus 'term' *)
-        | HintUnfold of string * ty option
+        | HintUnfold of string * ty option * string option
     end
 
     let __TODO_pat__ s = AST.Ident (s ^ " todo(pat)")
@@ -649,10 +649,8 @@ functor
       | AST.Require (Some x, imports, rename) ->
           "From" ^ " " ^ x ^ " "
           ^ decl_to_string (AST.Require (None, imports, rename))
-      | AST.HintUnfold (n, Some typ) ->
-          let ty_str = ty_to_string_without_paren typ in
-          "Hint Unfold" ^ " " ^ ty_str ^ "_" ^ n ^ "."
-      | AST.HintUnfold (n, None) -> "Hint Unfold" ^ " " ^ n ^ "."
+      | AST.HintUnfold (n, t, db) ->
+          "Hint Unfold" ^ " " ^ Option.value_map ~default:"" ~f:(fun typ -> let ty_str = ty_to_string_without_paren typ in ty_str ^ "_")  ^ n ^ Option.value_map ~default:"" ~f:(fun s -> " " ^ ":" ^ " " ^ s) db ^ "."
 
     and definition_value_to_equation_definition
         ((name, arguments, term, ty) : AST.definition_type) =

diff --git a/engine/backends/coq/ssprove/ssprove_backend.ml b/engine/backends/coq/ssprove/ssprove_backend.ml
@@ -798,8 +798,8 @@ struct
         SSP.AST.TuplePat (List.map ~f:(fun { pat; _ } -> ppat pat) args)
     (* Record *)
     | PConstruct { name; args; is_record = true; _ } ->
-      (* __TODO_pat__ p.span "record pattern" *)
-      SSP.AST.RecordPat (pglobal_ident name, List.map ~f:(fun {field; pat} -> (pglobal_ident field, ppat pat)) args)
+      __TODO_pat__ p.span "record pattern"
+      (* SSP.AST.RecordPat (pglobal_ident name, List.map ~f:(fun {field; pat} -> (pglobal_ident field, ppat pat)) args) *)
     (* (\* SSP.AST.Ident (pglobal_ident name) *\) *)
     (* SSP.AST.RecordPat (pglobal_ident name, List.map ~f:(fun {field; pat} -> (pglobal_ident field, ppat pat)) args) *)
     (*       (\* SSP.AST.ConstructorPat (pglobal_ident name ^ "_case", [SSP.AST.Ident "temp"]) *\) *)
@@ -1779,7 +1779,7 @@ struct
                 | TIFn (TArrow _) ->
                     [
                       SSP.AST.HintUnfold
-                        (pconcrete_ident x.ti_ident ^ "_loc", None);
+                        (pconcrete_ident x.ti_ident ^ "_loc", None, Some "hacspec_hints");
                     ]
                 | _ -> [])
               items
@@ -1862,7 +1862,7 @@ struct
                              ])
                        items) );
             ]
-          @ [ SSP.AST.HintUnfold (pglobal_ident name, Some (pty span self_ty)) ]
+          @ [ SSP.AST.HintUnfold (pglobal_ident name, Some (pty span self_ty), Some "hacspec_hints") ]
     in
     decls_from_item
 

diff --git a/proof-libs/coq/ssprove/_CoqProject b/proof-libs/coq/ssprove/_CoqProject
@@ -7,6 +7,7 @@ src/LocationUtility.v
 src/ChoiceEquality.v
 src/Hacspec_Lib_Pre.v
 
+src/Hacspec_Lib_StdLib.v
 src/Hacspec_Lib_Integers.v
 src/Hacspec_Lib_Loops.v
 src/Hacspec_Lib_Seq.v
@@ -20,6 +21,8 @@ src/Hacspec_Lib_Notation.v
 src/Hacspec_Lib_Cast.v
 src/Hacspec_Lib_TODO.v
 
+src/ConCertLib.v
+
 src/Hacspec_Lib.v
 
 # src/Hacspec_Aes_Jazz.v

diff --git a/proof-libs/coq/ssprove/src/ChoiceEquality.v b/proof-libs/coq/ssprove/src/ChoiceEquality.v
@@ -501,6 +501,27 @@ Section Both_helper.
     now intros ? ? ? [[] ? ?] ?.
   Defined.
 
+  Lemma valid_both_is_deterministic : forall {L A} (b : raw_both A),
+         valid_both L b -> deterministic (is_state b).
+  Proof.
+    intros.
+    destruct b as [is_pure is_state] ; simpl.
+    induction is_state.
+    - apply deterministic_ret.
+    - exfalso ; inversion H.
+    - apply deterministic_get.
+      intros.
+      apply X.
+      inversion H.
+    - apply deterministic_put.
+      apply IHis_state.
+      inversion H.
+      + admit.
+      + subst. now apply valid_both_eta.
+    - exfalso.
+      inversion H.
+  Admitted.
+
   Lemma both_valid_injectLocations :
     forall A L1 L2 (* I *) (v : raw_both A),
       fsubset L1 L2 ->

diff --git a/proof-libs/coq/ssprove/src/Hacspec_Lib.v b/proof-libs/coq/ssprove/src/Hacspec_Lib.v
@@ -39,6 +39,7 @@ Open Scope hacspec_scope.
 Open Scope nat_scope.
 Open Scope list_scope.
 
+From Hacspec Require Import Hacspec_Lib_StdLib. Export Hacspec_Lib_StdLib.
 From Hacspec Require Import Hacspec_Lib_Integers. Export Hacspec_Lib_Integers.
 From Hacspec Require Import Hacspec_Lib_Loops. Export Hacspec_Lib_Loops.
 From Hacspec Require Import Hacspec_Lib_Seq. Export Hacspec_Lib_Seq.
@@ -53,6 +54,9 @@ From Hacspec Require Import Hacspec_Lib_Cast. Export Hacspec_Lib_Cast.
 From Hacspec Require Import Hacspec_Lib_TODO. Export Hacspec_Lib_TODO.
 From Hacspec Require Import ConCertLib. Export ConCertLib.
 
+Set Bullet Behavior "Strict Subproofs".
+Set Default Goal Selector "!".
+
 (*** Result *)
 
 Definition Ok {L I} {a b : choice_type} : both L I a -> both L I (result b a) := lift1_both Ok.
@@ -66,4 +70,3 @@ Infix "||" := orb : bool_scope.
 
 Definition u32_word_t := nseq_ uint8 4.
 Definition u128_word_t := nseq_ uint8 16.
-