feat(specs): add a [-proof-manifest] flag, emit a .json

backends/lean/Aeneas/Std/WP.lean

@@ -704,6 +704,14 @@ theorem Result.of_wp {α} {x : Result α} (P : Result α → Prop) :
   simp only [WP.wp, PredTrans.apply] at hspec
   split at hspec <;> simp_all
 
+/-- Lift an Aeneas step spec to an mvcgen-compatible `Triple`. -/
+theorem spec_to_mvcgen {α : Type} {x : Result α} {Q : α → Prop}
+    (h : spec x Q) :
+    ⦃ ⌜ True ⌝ ⦄ x ⦃ ⇓ r => ⌜ Q r ⌝ ⦄ := by
+  obtain ⟨v, hx, hQv⟩ := spec_imp_exists h
+  subst hx
+  simp [Triple, hQv, WP.wp, PredTrans.apply]
+
 end Aeneas.Std.WP
 
 namespace Aeneas.Std

backends/lean/Aeneas/Tactic/Step/Init.lean

@@ -267,8 +267,40 @@ structure StepSpecAttr where
   ext  : Extension
   deriving Inhabited
 
-private def saveStepSpecFromThm (ext : Extension) (attrKind : AttributeKind) (thName : Name) :
-  AttrM Unit := do
+private def generateMvcgenSpec (stx : Syntax) (attrKind : AttributeKind) (thName : Name) :
+    MetaM Unit := do
+  let env ← getEnv
+  let some decl := env.findAsync? thName
+    | throwError "Could not find theorem {thName}"
+  let sig := decl.sig.get
+  -- Specialise all universe level parameters to 0 so that spec_to_mvcgen {α : Type} applies.
+  -- The generated mvcgen_spec is a valid Type-0 instance of the original theorem.
+  let zeroLevels := List.replicate sig.levelParams.length Level.zero
+  let ty ← normalizeLetBindings (sig.type.instantiateLevelParams sig.levelParams zeroLevels)
+  forallTelescope ty fun fvars _ => do
+    -- Apply the original theorem (at universe 0) to all fvars to get: spec (f args) Q
+    let thConst := Lean.mkConst thName zeroLevels
+    let thApp := mkAppN thConst fvars
+    -- Wrap with spec_to_mvcgen to produce: Triple (f args) ⌜True⌝ post⟨...⟩
+    let proof ← mkAppM ``Aeneas.Std.WP.spec_to_mvcgen #[thApp]
+    let innerTy ← inferType proof
+    -- Re-introduce all fvars as binders
+    let proofTerm ← mkLambdaFVars fvars proof
+    let thmTy ← mkForallFVars fvars innerTy
+    let mvcgenSpecName := Name.str thName "mvcgen_spec"
+    let auxDecl : TheoremVal := {
+      name        := mvcgenSpecName
+      levelParams := []    -- all level params have been fixed to 0
+      type        := thmTy
+      value       := proofTerm
+    }
+    addDecl (.thmDecl auxDecl)
+    addDeclarationRangesFromSyntax mvcgenSpecName stx
+    -- Register with @[spec] so mvcgen can find it
+    Lean.Attribute.add mvcgenSpecName `spec .missing attrKind
+
+private def saveStepSpecFromThm (ext : Extension) (attrKind : AttributeKind) (stx : Syntax)
+    (thName : Name) : AttrM Unit := do
   -- Lookup the theorem
   let env ← getEnv
   -- Ignore some auxiliary definitions (see the comments for attrIgnoreMutRec)
@@ -289,6 +321,12 @@ private def saveStepSpecFromThm (ext : Extension) (attrKind : AttributeKind) (th
     -- Save the entry
     ScopedEnvExtension.add ext (fKey, thName) attrKind
     trace[Step] "Saved the entry"
+    -- Also generate a corresponding mvcgen (@[spec]) lemma
+    try
+      trace[Step] "Registering with mvcgen"
+      MetaM.run' (generateMvcgenSpec stx attrKind thName)
+    catch e =>
+      logWarning m!"Could not generate mvcgen spec for {thName}: {e.toMessageData}"
     pure ()
 
 /- Initiliaze the `step` attribute. -/
@@ -299,7 +337,7 @@ initialize stepAttr : StepSpecAttr ← do
     descr := "Adds theorems to the `step` database"
     add := fun thName stx attrKind => do
       Attribute.Builtin.ensureNoArgs stx
-      saveStepSpecFromThm ext attrKind thName
+      saveStepSpecFromThm ext attrKind stx thName
     erase := fun thName => do
       let s := ext.getState (← getEnv)
       let s := s.erase thName
@@ -822,7 +860,7 @@ initialize stepPureAttribute : StepPureSpecAttr ← do
         -- Introduce the lifted theorem
         let liftedThmName ← MetaM.run' (liftThm stx thName pat)
         -- Save the lifted theorem to the `step` database
-        saveStepSpecFromThm stepAttr.ext attrKind liftedThmName
+        saveStepSpecFromThm stepAttr.ext attrKind stx liftedThmName
   }
   registerBuiltinAttribute attrImpl
   pure { attr := attrImpl }
@@ -963,7 +1001,7 @@ initialize stepPureDefAttribute : StepPureDefSpecAttr ← do
         -- Introduce the lifted theorem
         let thmName ← MetaM.run' (mkStepPureDefThm stx pat declName)
         -- Save the lifted theorem to the `step` database
-        saveStepSpecFromThm stepAttr.ext attrKind thmName
+        saveStepSpecFromThm stepAttr.ext attrKind stx thmName
   }
   registerBuiltinAttribute attrImpl
   pure { attr := attrImpl }

backends/lean/Aeneas/Tactic/Step/Tests.lean

@@ -1,3 +1,4 @@
 import Aeneas.Tactic.Step.Tests.HigherOrder
 import Aeneas.Tactic.Step.Tests.TupleDestruct
 import Aeneas.Tactic.Step.Tests.UncurryBind
+import Aeneas.Tactic.Step.Tests.MvcgenSpec

backends/lean/Aeneas/Tactic/Step/Tests/MvcgenSpec.lean

@@ -0,0 +1,31 @@
+import Aeneas.Std.Scalar
+import Aeneas.Std.Array
+import Aeneas.Tactic.Step
+
+open Aeneas Aeneas.Std Result Std.Do
+set_option mvcgen.warning false
+
+/-!
+# Tests: mvcgen spec generation from @[step]
+
+For every @[step] theorem, the attribute handler also generates an `mvcgen` spec.
+-/
+
+example {x y : U8} (hmax : x.val + y.val ≤ U8.max) :
+    ⦃ ⌜ True ⌝ ⦄ (x + y) ⦃ ⇓ z => ⌜ z.val = x.val + y.val ⌝ ⦄ := by
+  mvcgen; scalar_tac
+
+example {x y : U8} :
+    ⦃ ⌜ True ⌝ ⦄
+      (do
+        if x < 10#u8
+        then x * 2#u8
+        else pure y)
+    ⦃ ⇓ z => ⌜ z.val ≠ y → z.val < 20 ⌝ ⦄ := by
+  mvcgen <;> scalar_tac
+
+example (arr : Array U8 25#usize) (i : Usize) (a : U8) (hi : i < arr.length) :
+    ⦃ ⌜ True ⌝ ⦄
+      Array.update arr i a
+    ⦃ ⇓ r => ⌜ r.get? i = some a ⌝ ⦄ := by
+  mvcgen; grind

src/Config.ml

@@ -26,6 +26,45 @@ let set_backend (b : string) : unit =
          belonging to the proper set *)
       raise (Failure "Unexpected")
 
+(** {1 Specs config} *)
+
+type spec_source = Hax
+type spec_backend = Mvcgen | Step
+type spec_config = spec_source * spec_backend
+
+let spec_config_options = [ "hax"; "hax-step" ]
+
+(** Utility to compute a spec source from an input parameter *)
+let spec_config_of_string (s : string) : spec_config option =
+  match s with
+  | "hax" | "Hax" -> Some (Hax, Mvcgen)
+  | "hax-step" | "Hax-Step" -> Some (Hax, Step)
+  | _ -> None
+
+(** The spec source requested via [-specs] *)
+let opt_spec_config : spec_config option ref = ref None
+
+let set_spec_config (s : string) : unit =
+  match spec_config_of_string s with
+  | Some s -> opt_spec_config := Some s
+  | None ->
+      (* We shouldn't get there: the string should have been checked as
+         belonging to the proper set *)
+      raise (Failure "Unexpected")
+
+(** Returns [true] if the config for specs is enabled. *)
+let spec_config_enabled () = Option.is_some !opt_spec_config
+
+(** Returns [true] if the saved config for specs uses Hax annotations as a
+    source *)
+let spec_config_is_hax () =
+  match !opt_spec_config with
+  | Some (Hax, _) -> true
+  | _ -> false
+
+(** The spec backend selected via [-specs], if specs are enabled. *)
+let spec_backend () : spec_backend option = Option.map snd !opt_spec_config
+
 (** Specify the namespace of the extract code.
 
     For instance, if the crate name is [foo] the namespace used for the
@@ -228,6 +267,10 @@ let generate_lib_entry_point = ref false
 (** For Lean, controls whether we generate a lakefile or not. *)
 let lean_gen_lakefile = ref false
 
+(** For Lean, controls whether we write a sidecar JSON manifest listing the
+    names of the emitted proof obligations *)
+let proof_manifest = ref false
+
 (** If true, treat the unit functions (function taking no inputs and returning
     no outputs) as unit tests: evaluate them with the interpreter and check that
     they don't panic. *)
@@ -595,3 +638,14 @@ let max_recdepth = ref 2048
 (** If [false], evaluate [drop(p)] as [p := bottom]. Otherwise, evaluate it as a
     no-op (which means that we do not borrow-check the drops). *)
 let drop_as_no_op = ref true
+
+(** For Lean only: disable the Rust core library overrides defined in
+    [ExtractBuiltinLean.ml].
+
+    With this flag, references to items such as [core::clone::Clone<[T; N]>] are
+    extracted using the standard name-mangling scheme rather than the hand-tuned
+    names like [core.array.CloneArray.clone], and the associated shape overrides
+    ([keep_params], [can_fail], etc.) are ignored. This is useful when
+    extracting against a separate Lean library that mirrors the Rust core API
+    under the standard names. *)
+let core_models_lib = ref false

src/Main.ml

@@ -136,6 +136,14 @@ let () =
       ( "-lean-default-lakefile",
         Arg.Clear lean_gen_lakefile,
         " Generate a default lakefile.lean (Lean only)" );
+      ( "-specs",
+        Arg.Symbol (spec_config_options, set_spec_config),
+        " Gather and emit specs from the given source. Available: "
+        ^ String.concat ", " spec_config_options );
+      ( "-proof-manifest",
+        Arg.Set proof_manifest,
+        " Write a JSON manifest ProofObligations.json in the extraction folder, \
+         listing the emitted proof-obligation names (Lean only)" );
       ("-print-llbc", Arg.Set print_llbc, " Print the imported LLBC");
       ( "-abort-on-error",
         Arg.Set fail_hard,
@@ -208,6 +216,14 @@ let () =
          collisions with field projectors. Example: the `len` method in `impl \
          Struct { fn len(&self) -> usize { ... } }` would be named \
          `Struct.impl.len`." );
+      ( "-core-models-lib",
+        Arg.Set core_models_lib,
+        " For Lean: disable the Rust core library overrides from \
+         ExtractBuiltinLean.ml. Items like the `Clone` impl for arrays are \
+         extracted using the standard name-mangling scheme rather than \
+         hand-tuned names such as `core.array.CloneArray.clone`, and the \
+         associated shape overrides (keep_params, can_fail, etc.) are ignored."
+      );
       ( "-all-computable",
         Arg.Set all_computable,
         " For Lean: do not insert `noncomputable section` at the top of the \
@@ -449,17 +465,24 @@ let () =
     "-decreases-clauses";
   check_arg_implies !generate_lib_entry_point "-gen-lib-entry" !split_files
     "-split-files";
+  check_arg_implies !proof_manifest "-proof-manifest"
+    (Option.is_some !opt_spec_config) "-specs";
   check_arg_not !generate_lib_entry_point "-gen-lib-entry"
     (Option.is_some !subdir) "-subdir";
   if !lean_gen_lakefile && not (backend () = Lean) then
     fail_with_error
       "The -lean-default-lakefile option is valid only for the Lean backend";
+  if !core_models_lib && not (backend () = Lean) then
+    fail_with_error
+      "The -core-models-lib option is valid only for the Lean backend";
   if !set_max_heartbeats && not (backend () = Lean) then
     fail_with_error
       "The -max-heartbeats option is valid only for the Lean backend";
   if !set_max_recdepth && not (backend () = Lean) then
     fail_with_error
       "The -max-recdepth option is valid only for the Lean backend";
+  if Option.is_some !opt_spec_config && not (backend () = Lean) then
+    fail_with_error "The -specs option is valid only for the Lean backend";
 
   check_arg_implies !diagnose_detailed "-diagnose-detailed"
     !diagnose_micro_passes "-diagnose-micro-passes";
@@ -592,8 +615,15 @@ let () =
       (* Print the external definitions which are not listed in the builtin functions *)
       if !print_unknown_externals then (
         let open TranslateCore in
-        let { type_decls; fun_decls; global_decls; trait_decls; trait_impls; _ }
-            =
+        let ({
+               type_decls;
+               fun_decls;
+               global_decls;
+               trait_decls;
+               trait_impls;
+               _;
+             }
+              : crate) =
           m
         in
         (* Filter the definitions *)