Add equivalence lemma for montgomery_multuiply

fstar-helpers/Makefile.base

@@ -10,6 +10,4 @@ EXTRA_HELPMESSAGE += printf "Libcrux specifics:\n";
 EXTRA_HELPMESSAGE += target SLOW_MODULES 'a list of modules to verify fully only when `VERIFY_SLOW_MODULES` is set to `yes`. When `VERIFY_SLOW_MODULES`, those modules are admitted.';
 EXTRA_HELPMESSAGE += target VERIFY_SLOW_MODULES '`yes` or `no`, defaults to `no`';
 
-FSTAR_INCLUDE_DIRS_EXTRA += $(HACL_HOME)/specs
-FSTAR_INCLUDE_DIRS_EXTRA += $(shell git rev-parse --show-toplevel)/fstar-helpers/tactics
 include $(shell git rev-parse --show-toplevel)/fstar-helpers/Makefile.generic

fstar-helpers/Makefile.generic

@@ -174,6 +174,7 @@ target "all" "Verify every F* files (stops whenever an F* fails first)"
 target "all-keep-going" "Verify every F* files (tries as many F* module as possible)"
 target "" ""
 target "run/${ANSI_COLOR_TONE}<MyModule.fst>  " 'Runs F* on `MyModule.fst` only'
+target "check/${ANSI_COLOR_TONE}<MyModule.fst>  " 'Typecheck up to `MyModule.fst`'
 target "" ""
 target "vscode" 'Generates a `hax.fst.config.json` file'
 target "${ANSI_COLOR_TONE}<MyModule.fst>${ANSI_COLOR_BLUE}-in   " 'Useful for Emacs, outputs the F* prefix command to be used'
@@ -216,6 +217,9 @@ run/%: | .depend $(HINT_DIR) $(CACHE_DIR)
 	${HEADER}
 	$(Q)$(FSTAR) $(OTHERFLAGS) $(@:run/%=%)
 
+check/%: | .depend $(HINT_DIR) $(CACHE_DIR) $(HACL_HOME)
+	$(Q)$(MAKE) "${CACHE_DIR}/$(@:check/%=%).checked"
+
 VERIFIED_CHECKED = $(addsuffix .checked, $(addprefix $(CACHE_DIR)/,$(ROOTS)))
 ADMIT_CHECKED = $(addsuffix .checked, $(addprefix $(CACHE_DIR)/,$(ADMIT_MODULES)))
 

fstar-helpers/core-models/Cargo.toml

@@ -12,6 +12,7 @@ publish = false
 [dependencies]
 rand = "0.9"
 hax-lib.workspace = true
+pastey = "0.1.0"
 
 [lints.rust]
 unexpected_cfgs = { level = "warn", check-cfg = ['cfg(hax)'] }

fstar-helpers/core-models/proofs/fstar/extraction/Makefile

@@ -0,0 +1,2 @@
+include $(shell git rev-parse --show-toplevel)/fstar-helpers/Makefile.base
+

fstar-helpers/tactics/Tactics.Circuits.fst → fstar-helpers/core-models/proofs/fstar/extraction/Tactics.Circuits.fst

@@ -201,11 +201,12 @@ let mk_app_bs (t: term) (bs: list binder): Tac term
     mk_app t args
 
 /// Given a lemma `i1 -> ... -> iN -> Lemma (lhs == rhs)`, this tactic
-/// produces a lemma `i1 -> ... -> iN -> Lemma (lhs == rhs')` where
-/// `rhs'` is given by the tactic call `f <rhs>`.
-let map_lemma_rhs (f: term -> Tac term) (lemma: term) (d: dbg): Tac term
+/// produces a lemma `i1 -> ... -> iN -> ...extra_args... -> Lemma (lhs' == rhs')` where
+/// `lhs'` and `rhs'` are given by the tactic call `f <rhs>`.
+let edit_lemma (extra_args: list binder) (f_lhs g_rhs: term -> Tac term) (lemma: term) (d: dbg): Tac term
   = let typ = tc (top_env ()) lemma in
-    let inputs, comp = collect_arr_bs typ in
+    let inputs0, comp = collect_arr_bs typ in
+    let inputs = List.Tot.append inputs0 extra_args in
     let post =
       match inspect_comp comp with
       | C_Lemma pre post _ ->
@@ -221,28 +222,115 @@ let map_lemma_rhs (f: term -> Tac term) (lemma: term) (d: dbg): Tac term
       | _, [_; (lhs, _); (rhs, _)] -> (lhs, rhs)
       | _ -> d.fail "expected lhs == rhs"
     in
-    let lemma_body = mk_abs inputs (mk_app_bs lemma inputs) in
-    let post = mk_abs [post_bd] (mk_e_app (`eq2) [lhs; f rhs]) in
+    let lemma_body = mk_abs inputs (mk_app_bs lemma inputs0) in
+    let post = mk_abs [post_bd] (mk_e_app (`eq2) [f_lhs lhs; g_rhs rhs]) in
     let lemma_typ = mk_arr inputs (pack_comp (C_Lemma (`True) post (`[]))) in
     let lemma = pack (Tv_AscribedT lemma_body lemma_typ None false) in
     lemma
 
+/// Specialize a lemma `lhs == rhs` into `lhs x == rhs x` if possible.
+let specialize_lemma_apply (lemma: term): Tac (option term)
+  = let x: binder = fresh_binder_named "arg0" (`_) in
+    let f t: Tac _ = mk_e_app t [binder_to_term x] in
+    let h = edit_lemma [x] f f lemma (mk_dbg "") in
+    trytac (fun _ -> norm_term [] h)
+
+let rec flatten_options (l: list (option 't)): list 't
+  = match l with
+  | Some hd::tl -> hd::flatten_options tl
+  | None   ::tl -> flatten_options tl
+  | []         -> []
+
+/// Given a lemma `i1 -> ... -> iN -> Lemma (lhs == rhs)`, this tactic
+/// produces a lemma `i1 -> ... -> iN -> Lemma (lhs == rhs')` where
+/// `rhs'` is given by the tactic call `f <rhs>`.
+let map_lemma_rhs (f: term -> Tac term) (lemma: term) (d: dbg): Tac term
+  = edit_lemma [] (fun t -> t) f lemma d
+
 /// Helper to mark terms. This is an identity function.
 /// It is used to normalize terms selectively in two passes:
 ///  1. browse the term, mark the subterms you want to target
 ///  2. use `ctrl_rewrite`, doing something only for `mark_to_normalize_here #_ _` terms.
 private let mark_to_normalize_here #t (x: t): t = x
 
+/// Unapplies a function named `f_name` of arity `arity`.
+let mk_unapply_lemma (f_name: string) (arity: nat): Tac term =
+  let f = pack (Tv_FVar (pack_fv (explode_qn f_name))) in
+  let bds =
+    let rec aux (n: nat): Tac _ = match n with | 0 -> [] | _ -> fresh_binder (`_) :: aux (n - 1) in
+    aux arity
+  in
+  let applied_f = mk_app_bs f bds in
+  let rhs = norm_term [delta_only [f_name]] f in
+  let rhs = mk_app_bs rhs bds in
+  let post = mk_e_app (`(==)) [rhs; applied_f] in
+  let typ = mk_arr bds (pack_comp (C_Lemma (`True) (mk_abs [fresh_binder (`_)] post) (`[]))) in
+  let body = mk_abs bds (`()) in
+  let lemma = `(`#body <: `#typ) in
+  norm_term [] lemma
+
+let (let??) (x: option 'a) (f: 'a -> Tac (option 'b)): Tac (option 'b)
+  = match x with
+  | Some x -> f x
+  | None   -> None
+
+let expect_const_int (t: term): Tac (option int)
+  = match t with
+  | Tv_Const (C_Int n) -> Some n
+  | _ -> None
+
+let expect_fvar (f: string) (t: term): Tac (option unit)
+  = match t with
+  | Tv_UInst fv _ | Tv_FVar fv ->
+    if implode_qn (inspect_fv fv) = f
+    then Some ()
+    else None
+  | _ -> None
+
+let expect_app (f: string) (arity: nat) (t: term): Tac (option (l: list term {List.Tot.length l = arity}))
+  = let hd, args = collect_app t in
+    let?? () = expect_fvar f hd in
+    let args = List.Tot.map fst args in
+    if List.Tot.length args = arity
+    then let args: l: list term {List.Tot.length l = arity} = args in
+         Some args
+    else None
+
+let auto_unapply (arity: int) = ()
+
+let get_unapply_auto_lemmas ()
+  = filter_map
+        (fun f ->
+          let name = inspect_fv f in
+          let?? sg = lookup_typ (top_env ()) name in
+          let attrs = sigelt_attrs sg in
+          let?? [arity] = tryPick (expect_app (`%auto_unapply) 1) attrs in
+          let?? arity = expect_const_int arity in
+          if arity < 0 then fail "negative arity";
+          Some (mk_unapply_lemma (implode_qn name) arity)
+        )
+        (lookup_attr (`auto_unapply) (top_env ()))
+
 let flatten_circuit_aux
   (namespace_always_norm: list string)
   (lift_lemmas: list term) (simpl_lemmas: list term)
   (eta_match_lemmas: list term)
   d
   =
     d.sub "postprocess_tactic" (fun d ->
-        norm [primops; iota; delta_namespace ["Libcrux_intrinsics"]; zeta_full];
+        let namespaces_to_unfold =
+          let crate = match cur_module () with | crate::_ -> crate | _ -> fail "Empty module name" in
+          [crate; "Libcrux_intrinsics"]
+        in
+        d.dump ("will unfold namespaces [" ^ FStar.String.concat ";" namespaces_to_unfold ^ "]");
+        norm [primops; iota; delta_namespace namespaces_to_unfold; zeta_full];
         d.dump "definitions unfolded";
 
+
+        let simpl_lemmas = simpl_lemmas
+          `List.Tot.append` flatten_options (map specialize_lemma_apply simpl_lemmas)
+        in
+
         rewrite_with_lifts lift_lemmas simpl_lemmas d;
 
         let eta_match_lemmas =
@@ -278,10 +366,19 @@ let flatten_circuit_aux
         d.dump "after full normalization";
         set_smt_goals sgs;
 
+
+        d.print "unapply functions";
+        let unapply_lemmas = get_unapply_auto_lemmas () in
+        l_to_r unapply_lemmas;
+
+        let sgs = smt_goals () in
+        set_smt_goals [];
+        d.dump "after unapply";
+        set_smt_goals sgs;
+
         ()
     )
 
-
 /// `flatten_circuit` works on a goal `squash (c == ?u)` such that `c`
 /// is a circuit.
 ///
@@ -333,6 +430,15 @@ let flatten_circuit
         eta_match_lemmas d;
     trefl ()
   in
-  if lax_on ()
+  let disable_ext_flag =
+    // Disabling the flatten circuit tactic in lax/admit mode is usually a bad idea:
+    //  - if there are no checked file, dependencies will be checked in lax mode
+    //  - then, if we want to apply the circuit flattening tactic on a function `A.f`
+    //    that happens to use a function `B.g` and expect it to be flattened,
+    //    then `B.g` actually not be flattened since it was lax checked
+    FStar.Stubs.Tactics.V2.Builtins.ext_enabled "disable_circuit_norm"
+  in
+  let is_lax_on = lax_on () in
+  if is_lax_on && disable_ext_flag
   then trefl ()
   else run (mk_dbg "")