Lean backend [Part 1/3]

cli/default.nix

@@ -5,7 +5,7 @@ let
   is-webapp-static-asset = path:
     builtins.match ".*(script[.]js|index[.]html)" path != null;
   buildInputs = lib.optionals stdenv.isDarwin [ libiconv libz.dev ];
-  binaries = [ hax hax-engine.bin rustc gcc ] ++ buildInputs;
+  binaries = [ hax hax-engine.bin rustc gcc hax_rust_engine ] ++ buildInputs;
   commonArgs = {
     version = "0.0.1";
     src = lib.cleanSourceWith {
@@ -40,6 +40,12 @@ let
     inherit cargoArtifacts pname;
     doInstallCargoArtifacts = true;
   });
+  hax_rust_engine = craneLib.buildPackage (commonArgs // {
+    inherit cargoArtifacts;
+    buildInputs = buildInputs ++ [ makeWrapper ];
+    pname = "hax-rust-engine";
+    cargoExtraArgs = "--manifest-path rust-engine/Cargo.toml --locked";
+  });
   docs = craneLib.cargoDoc (commonArgs // {
     # preBuildPhases = [ "addRustcDocs" ];
     cargoDocExtraArgs = "--document-private-items";

cli/subcommands/src/cargo_hax.rs

@@ -133,7 +133,7 @@ const RUST_ENGINE_BINARY_NOT_FOUND: &str =
 fn find_rust_hax_engine(message_format: MessageFormat) -> process::Command {
     use which::which;
 
-    std::env::var("HAX_RUST_BINARY")
+    std::env::var("HAX_RUST_ENGINE_BINARY")
         .ok()
         .map(process::Command::new)
         .or_else(|| {

engine/lib/profiling.ml

@@ -1,7 +1,7 @@
 open Prelude
 
 (** Is profiling enabled? *)
-let enabled = ref true
+let enabled = ref false
 
 (** Profiles the function `f`, that operates in a given context over a given quantity of things it is processing. *)
 let profile (type b) (context : Diagnostics.Context.t) (quantity : int)

examples/barrett/Makefile

@@ -1,7 +1,10 @@
-.PHONY: default clean
-default:
+.PHONY: default lean clean
+default: lean
 	make -C proofs/fstar/extraction
 
+lean:
+	cargo hax into lean
+
 clean:
 	rm -f proofs/fstar/extraction/.depend
 	rm -f proofs/fstar/extraction/*.fst

examples/barrett/proofs/lean/extraction/Lib.lean

@@ -0,0 +1,83 @@
+abbrev u8 := Nat
+abbrev u16 := Nat
+abbrev u32 := Nat
+abbrev u64 := Nat
+abbrev usize := Nat
+abbrev i8 := Nat
+abbrev i16 := Nat
+abbrev i32 := Nat
+abbrev i64 := Nat
+abbrev isize := Nat
+
+-- Arithmetic
+def hax_machine_int_add (x y: Nat) := x + y
+def hax_machine_int_mul (x y: Nat) := x * y
+def hax_machine_int_bitxor (x y: Nat) : Nat := sorry
+
+def hax_machine_int_eq (x y: Nat) : Bool := x = y
+def hax_machine_int_ne (x y: Nat) : Bool := x != y
+def hax_machine_int_ge (x y: Nat) : Bool := x >= y
+def hax_machine_int_gt (x y: Nat) : Bool := x > y
+def hax_machine_int_le (x y: Nat) : Bool := x <= y
+def hax_machine_int_lt (x y: Nat) : Bool := x < y
+
+
+-- Nums
+def num_impl_wrapping_add : Nat -> Nat -> Nat := sorry
+def num_impl_from_le_bytes {α} : (Array α) -> u32 := sorry
+
+-- Results
+inductive result_Result α β
+| ok : α -> result_Result α β
+| err : β -> result_Result α β
+
+axiom array_TryFromSliceError : Type
+
+-- Assert
+def assert : Bool -> Unit := fun _ => ()
+def assume : Prop -> Unit := fun _ => ()
+def prop_constructors_from_bool : Bool -> Prop := sorry
+
+-- Hax
+def hax_folds_fold_range
+  (s: Nat)
+  (e: Nat) :
+  ((Array u32) -> Nat -> Bool) ->
+  (Array u32) ->
+  ((Array u32) -> Nat -> (Array u32)) ->
+  (Array u32) := sorry
+
+def hax_monomorphized_update_at_update_at_usize :
+  (Array u32) ->
+  Nat ->
+  u32 ->
+  (Array u32) := sorry
+
+abbrev hax__autogenerated_refinement__BoundedUsize_BoundedUsize (_: Nat) (_: Nat) := Nat
+
+def result_impl_unwrap {α} : α -> Array β := sorry
+
+-- Vectors
+def hax_repeat (x:Nat) (y:Nat) : Array u32 := sorry
+
+-- Ranges
+
+structure ops_range_Range_arg (α: Type) where
+ops_range_Range_start : α
+ops_range_Range_end : α
+
+inductive ops_range_Range (α: Type)  where
+| constr_ops_range_Range : ops_range_Range_arg α -> ops_range_Range α
+
+
+-- Arrays
+def ops_index_Index_index (a: Array u8) : α -> β := sorry
+def convert_TryInto_try_into {α} : Array α ->
+   result_Result (Array α) array_TryFromSliceError := sorry
+
+
+-- Slices
+def slice_impl_len (a: Array u32) : Nat := sorry
+
+-- Bytes
+def num_impl_to_le_bytes : u32 -> Array u8 := sorry

examples/barrett/proofs/lean/extraction/lakefile.toml

@@ -0,0 +1,10 @@
+name = "barrett"
+version = "0.1.0"
+defaultTargets = ["barrett"]
+
+[[lean_lib]]
+name = "Lib"
+
+[[lean_exe]]
+name = "barrett"
+root = "barrett"

rust-engine/Cargo.toml

@@ -17,4 +17,4 @@ serde_json = { workspace = true, features = ["unbounded_depth"] }
 schemars.workspace = true
 serde-jsonlines = "0.5.0"
 serde_stacker = "0.1.12"
-pretty = "0.12.4"
+pretty = "0.12"

rust-engine/src/ast.rs

@@ -1156,7 +1156,7 @@ pub enum AttributeKind {
     Tool {
         /// The path to the tool
         path: String,
-        /// The payload        
+        /// The payload
         tokens: String,
     },
     /// A doc comment
@@ -1540,5 +1540,15 @@ pub mod traits {
             }
         }
     }
+
+    /// Manual implementation of HasKind as the Ty struct contains a Box<TyKind>
+    /// instead of a TyKind directly.
+    impl HasKind for Ty {
+        type Kind = TyKind;
+
+        fn kind(&self) -> &Self::Kind {
+            &(*self.0)
+        }
+    }
 }
 pub use traits::*;

rust-engine/src/ast/identifiers.rs

@@ -90,6 +90,39 @@ mod global_id {
         /// A projector.
         Projector(ConcreteId),
     }
+
+    impl GlobalId {
+        /// Extracts the Crate info
+        pub fn krate(&self) -> String {
+            match self {
+                GlobalId::Concrete(concrete_id) | GlobalId::Projector(concrete_id) => {
+                    concrete_id.def_id.def_id.krate.clone()
+                }
+            }
+        }
+
+        /// Raw printing of identifier separated by underscore. Used for testing
+        pub fn to_debug_string(&self) -> String {
+            match self {
+                GlobalId::Concrete(concrete_id) => concrete_id
+                    .def_id
+                    .def_id
+                    .clone()
+                    .path
+                    .into_iter()
+                    .map(|def| match def.clone().data {
+                        hax_frontend_exporter::DefPathItem::ValueNs(s)
+                        | hax_frontend_exporter::DefPathItem::MacroNs(s)
+                        | hax_frontend_exporter::DefPathItem::TypeNs(s) => s.clone(),
+                        hax_frontend_exporter::DefPathItem::Impl => "impl".to_string(),
+                        other => unimplemented!("{other:?}"),
+                    })
+                    .collect::<Vec<String>>()
+                    .join("_"),
+                GlobalId::Projector(concrete_id) => todo!(),
+            }
+        }
+    }
 }
 
 /// Local identifier