refactor(lean): move hax_lib and rust_primitives into their own dir

lean/CoreModels.lean

@@ -1,3 +1,5 @@
 import CoreModels.Command
 import CoreModels.Core
 import CoreModels.Alloc
+import CoreModels.HaxLib
+import CoreModels.RustPrimitives

lean/CoreModels/Alloc/Funs.lean

@@ -3,11 +3,11 @@
 import Aeneas
 import CoreModels.Core.TypesPrologue
 import CoreModels.Core.Types
-import CoreModels.Core.TypesExternal
+import CoreModels.RustPrimitives.Types
 import CoreModels.Alloc.Types
-import CoreModels.Core.FunsExternal
+import CoreModels.RustPrimitives.Funs
 import CoreModels.Core.Funs
--- (alloc-side externals live in parent Aeneas.FunsExternal)
+-- (alloc-side externals live in parent CoreModels.RustPrimitives)
 open CoreModels Aeneas
 open Aeneas.Std hiding namespace core alloc
 open Result ControlFlow Error

lean/CoreModels/Alloc/Types.lean

@@ -3,8 +3,8 @@
 import Aeneas
 import CoreModels.Core.TypesPrologue
 import CoreModels.Core.Types
-import CoreModels.Core.TypesExternal
--- (alloc-side externals live in parent Aeneas.FunsExternal)
+import CoreModels.RustPrimitives.Types
+-- (alloc-side externals live in parent CoreModels.RustPrimitives)
 open CoreModels Aeneas
 open Aeneas.Std hiding namespace core alloc
 open Result ControlFlow Error

lean/CoreModels/Core/FunsPrologue.lean

@@ -78,6 +78,45 @@ instance Isize.Insts.CoreCmpPartialOrdIsize : cmp.PartialOrd Isize Isize := mkIP
 abbrev ops.range.Range.Insts.CoreIterTraitsIteratorIterator.next :=
   @IteratorRange.next
 
+/-- [core::cmp::impls::{core::cmp::PartialOrd<&0 (B)> for &1 (A)}::lt]:
+    Source: '/rustc/library/core/src/cmp.rs', lines 2133:8-2133:40
+    Name pattern: [core::cmp::impls::{core::cmp::PartialOrd<&'1 @A, &'0 @B>}::lt]
+    Visibility: public -/
+@[rust_fun "core::cmp::impls::{core::cmp::PartialOrd<&'1 @A, &'0 @B>}::lt"]
+def Shared1A.Insts.CoreCmpPartialOrdShared0B.lt
+  {A : Type} {B : Type} (PartialOrdInst : cmp.PartialOrd A B) :
+  A → B → Result Bool := fun a b => do
+  let o ← PartialOrdInst.partial_cmp a b
+  match o with
+  | some cmp.Ordering.Less => ok true
+  | _ => ok false
+
+/-- [core::cmp::impls::{core::cmp::PartialOrd<&0 (B)> for &1 (A)}::gt]:
+    Source: '/rustc/library/core/src/cmp.rs', lines 2141:8-2141:40
+    Name pattern: [core::cmp::impls::{core::cmp::PartialOrd<&'1 @A, &'0 @B>}::gt]
+    Visibility: public -/
+@[rust_fun "core::cmp::impls::{core::cmp::PartialOrd<&'1 @A, &'0 @B>}::gt"]
+def Shared1A.Insts.CoreCmpPartialOrdShared0B.gt
+  {A : Type} {B : Type} (PartialOrdInst : cmp.PartialOrd A B) :
+  A → B → Result Bool := fun a b => do
+  let o ← PartialOrdInst.partial_cmp a b
+  match o with
+  | some cmp.Ordering.Greater => ok true
+  | _ => ok false
+
+/-- [core::slice::cmp::{core::cmp::PartialEq<[U]> for [T]}::eq]:
+    Source: '/rustc/library/core/src/slice/cmp.rs', lines 18:4-18:37
+    Name pattern: [core::slice::cmp::{core::cmp::PartialEq<[@T], [@U]>}::eq]
+    Visibility: public -/
+@[rust_fun "core::slice::cmp::{core::cmp::PartialEq<[@T], [@U]>}::eq"]
+def Slice.Insts.CoreCmpPartialEqSlice.eq
+  {T : Type} {U : Type} (cmpPartialEqInst : cmp.PartialEq T U) :
+  Slice T → Slice U → Result Bool := fun s1 s2 =>
+  if s1.length ≠ s2.length then ok false
+  else do
+    let rs ← (s1.val.zip s2.val).mapM (fun p => cmpPartialEqInst.eq p.1 p.2)
+    ok (rs.all id)
+
 /-! ## Slice -/
 
 def slice.Slice.len {T : Type u} (v : Aeneas.Std.Slice T) : Aeneas.Std.Result Usize :=

lean/CoreModels/Core/Types.lean

@@ -3,7 +3,7 @@
 import Aeneas
 import CoreModels.Command
 import CoreModels.Core.TypesPrologue
-import CoreModels.Core.TypesExternal
+import CoreModels.RustPrimitives.Types
 open CoreModels Aeneas
 open Aeneas.Std hiding namespace core alloc
 open Result ControlFlow Error
@@ -524,73 +524,73 @@ structure num.error.ParseIntError where
   kind : num.error.IntErrorKind
 
 /-- [core_models::num::u8]
-    Source: 'core-models/src/core/num/mod.rs', lines 415:0-415:14
+    Source: 'core-models/src/core/num/mod.rs', lines 447:0-447:14
     Visibility: public -/
 @[reducible]
 def num.u8 := Unit
 
 /-- [core_models::num::u16]
-    Source: 'core-models/src/core/num/mod.rs', lines 418:0-418:15
+    Source: 'core-models/src/core/num/mod.rs', lines 450:0-450:15
     Visibility: public -/
 @[reducible]
 def num.u16 := Unit
 
 /-- [core_models::num::u32]
-    Source: 'core-models/src/core/num/mod.rs', lines 421:0-421:15
+    Source: 'core-models/src/core/num/mod.rs', lines 453:0-453:15
     Visibility: public -/
 @[reducible]
 def num.u32 := Unit
 
 /-- [core_models::num::u64]
-    Source: 'core-models/src/core/num/mod.rs', lines 424:0-424:15
+    Source: 'core-models/src/core/num/mod.rs', lines 456:0-456:15
     Visibility: public -/
 @[reducible]
 def num.u64 := Unit
 
 /-- [core_models::num::u128]
-    Source: 'core-models/src/core/num/mod.rs', lines 427:0-427:16
+    Source: 'core-models/src/core/num/mod.rs', lines 459:0-459:16
     Visibility: public -/
 @[reducible]
 def num.u128 := Unit
 
 /-- [core_models::num::usize]
-    Source: 'core-models/src/core/num/mod.rs', lines 430:0-430:17
+    Source: 'core-models/src/core/num/mod.rs', lines 462:0-462:17
     Visibility: public -/
 @[reducible]
 def num.usize := Unit
 
 /-- [core_models::num::i8]
-    Source: 'core-models/src/core/num/mod.rs', lines 433:0-433:14
+    Source: 'core-models/src/core/num/mod.rs', lines 465:0-465:14
     Visibility: public -/
 @[reducible]
 def num.i8 := Unit
 
 /-- [core_models::num::i16]
-    Source: 'core-models/src/core/num/mod.rs', lines 436:0-436:15
+    Source: 'core-models/src/core/num/mod.rs', lines 468:0-468:15
     Visibility: public -/
 @[reducible]
 def num.i16 := Unit
 
 /-- [core_models::num::i32]
-    Source: 'core-models/src/core/num/mod.rs', lines 439:0-439:15
+    Source: 'core-models/src/core/num/mod.rs', lines 471:0-471:15
     Visibility: public -/
 @[reducible]
 def num.i32 := Unit
 
 /-- [core_models::num::i64]
-    Source: 'core-models/src/core/num/mod.rs', lines 442:0-442:15
+    Source: 'core-models/src/core/num/mod.rs', lines 474:0-474:15
     Visibility: public -/
 @[reducible]
 def num.i64 := Unit
 
 /-- [core_models::num::i128]
-    Source: 'core-models/src/core/num/mod.rs', lines 445:0-445:16
+    Source: 'core-models/src/core/num/mod.rs', lines 477:0-477:16
     Visibility: public -/
 @[reducible]
 def num.i128 := Unit
 
 /-- [core_models::num::isize]
-    Source: 'core-models/src/core/num/mod.rs', lines 448:0-448:17
+    Source: 'core-models/src/core/num/mod.rs', lines 480:0-480:17
     Visibility: public -/
 @[reducible]
 def num.isize := Unit

lean/CoreModels/HaxLib.lean

@@ -0,0 +1 @@
+import CoreModels.HaxLib.Funs

lean/CoreModels/HaxLib/Funs.lean

@@ -0,0 +1,151 @@
+import Aeneas
+import CoreModels.Command
+import CoreModels.Core.TypesPrologue
+import CoreModels.Core.Types
+open Aeneas
+open Aeneas.Std hiding namespace core
+open Result ControlFlow Error
+set_option linter.dupNamespace false
+set_option linter.hashCommand false
+set_option linter.unusedVariables false
+
+namespace CoreModels
+
+namespace core
+
+/-- [hax_lib::int::{core::cmp::PartialOrd<hax_lib::int::Int> for hax_lib::int::Int}::le]:
+    Source: '/cargo/git/checkouts/hax-580ebeee043cdea1/492a34e/hax-lib/src/dummy.rs', lines 77:46-77:56
+    Name pattern: [hax_lib::int::{core::cmp::PartialOrd<hax_lib::int::Int, hax_lib::int::Int>}::le]
+    Visibility: public -/
+@[rust_fun
+  "hax_lib::int::{core::cmp::PartialOrd<hax_lib::int::Int, hax_lib::int::Int>}::le"]
+def hax_lib.int.Int.Insts.CoreCmpPartialOrdInt.le
+  : hax_lib.int.Int → hax_lib.int.Int → Result Bool :=
+  fun a b => ok (decide (a ≤ b))
+
+/-- [hax_lib::int::{core::ops::arith::Add<hax_lib::int::Int, hax_lib::int::Int> for hax_lib::int::Int}::add]:
+    Source: '/cargo/git/checkouts/hax-580ebeee043cdea1/492a34e/hax-lib/src/dummy.rs', lines 92:8-92:49
+    Name pattern: [hax_lib::int::{core::ops::arith::Add<hax_lib::int::Int, hax_lib::int::Int, hax_lib::int::Int>}::add]
+    Visibility: public -/
+@[rust_fun
+  "hax_lib::int::{core::ops::arith::Add<hax_lib::int::Int, hax_lib::int::Int, hax_lib::int::Int>}::add"]
+def hax_lib.int.Int.Insts.CoreOpsArithAddIntInt.add
+  : hax_lib.int.Int → hax_lib.int.Int → Result hax_lib.int.Int := fun a b => ok (a + b)
+
+/-- [hax_lib::int::{core::ops::arith::Sub<hax_lib::int::Int, hax_lib::int::Int> for hax_lib::int::Int}::sub]:
+    Source: '/cargo/git/checkouts/hax-580ebeee043cdea1/492a34e/hax-lib/src/dummy.rs', lines 100:8-100:49
+    Name pattern: [hax_lib::int::{core::ops::arith::Sub<hax_lib::int::Int, hax_lib::int::Int, hax_lib::int::Int>}::sub]
+    Visibility: public -/
+@[rust_fun
+  "hax_lib::int::{core::ops::arith::Sub<hax_lib::int::Int, hax_lib::int::Int, hax_lib::int::Int>}::sub"]
+def hax_lib.int.Int.Insts.CoreOpsArithSubIntInt.sub
+  : hax_lib.int.Int → hax_lib.int.Int → Result hax_lib.int.Int := fun a b => ok (a - b)
+
+/-- [hax_lib::int::{core::ops::arith::Mul<hax_lib::int::Int, hax_lib::int::Int> for hax_lib::int::Int}::mul]:
+    Source: '/cargo/git/checkouts/hax-580ebeee043cdea1/492a34e/hax-lib/src/dummy.rs', lines 108:8-108:49
+    Name pattern: [hax_lib::int::{core::ops::arith::Mul<hax_lib::int::Int, hax_lib::int::Int, hax_lib::int::Int>}::mul]
+    Visibility: public -/
+@[rust_fun
+  "hax_lib::int::{core::ops::arith::Mul<hax_lib::int::Int, hax_lib::int::Int, hax_lib::int::Int>}::mul"]
+def hax_lib.int.Int.Insts.CoreOpsArithMulIntInt.mul
+  : hax_lib.int.Int → hax_lib.int.Int → Result hax_lib.int.Int := fun a b => ok (a * b)
+
+/-- [hax_lib::int::{hax_lib::int::ToInt for u8}::to_int]:
+    Source: '/cargo/git/checkouts/hax-580ebeee043cdea1/492a34e/hax-lib/src/dummy.rs', lines 155:16-155:38
+    Name pattern: [hax_lib::int::{hax_lib::int::ToInt<u8>}::to_int]
+    Visibility: public -/
+@[rust_fun "hax_lib::int::{hax_lib::int::ToInt<u8>}::to_int"]
+def hax_lib.U8.Insts.Hax_libIntToInt.to_int : Std.U8 → Result hax_lib.int.Int :=
+  fun x => ok (x.val : Int)
+
+/-- [hax_lib::int::{hax_lib::int::ToInt for u16}::to_int]:
+    Source: '/cargo/git/checkouts/hax-580ebeee043cdea1/492a34e/hax-lib/src/dummy.rs', lines 155:16-155:38
+    Name pattern: [hax_lib::int::{hax_lib::int::ToInt<u16>}::to_int]
+    Visibility: public -/
+@[rust_fun "hax_lib::int::{hax_lib::int::ToInt<u16>}::to_int"]
+def hax_lib.U16.Insts.Hax_libIntToInt.to_int : Std.U16 → Result hax_lib.int.Int :=
+  fun x => ok (x.val : Int)
+
+/-- [hax_lib::int::{hax_lib::int::ToInt for u32}::to_int]:
+    Source: '/cargo/git/checkouts/hax-580ebeee043cdea1/492a34e/hax-lib/src/dummy.rs', lines 155:16-155:38
+    Name pattern: [hax_lib::int::{hax_lib::int::ToInt<u32>}::to_int]
+    Visibility: public -/
+@[rust_fun "hax_lib::int::{hax_lib::int::ToInt<u32>}::to_int"]
+def hax_lib.U32.Insts.Hax_libIntToInt.to_int : Std.U32 → Result hax_lib.int.Int :=
+  fun x => ok (x.val : Int)
+
+/-- [hax_lib::int::{hax_lib::int::ToInt for u64}::to_int]:
+    Source: '/cargo/git/checkouts/hax-580ebeee043cdea1/492a34e/hax-lib/src/dummy.rs', lines 155:16-155:38
+    Name pattern: [hax_lib::int::{hax_lib::int::ToInt<u64>}::to_int]
+    Visibility: public -/
+@[rust_fun "hax_lib::int::{hax_lib::int::ToInt<u64>}::to_int"]
+def hax_lib.U64.Insts.Hax_libIntToInt.to_int : Std.U64 → Result hax_lib.int.Int :=
+  fun x => ok (x.val : Int)
+
+/-- [hax_lib::int::{hax_lib::int::ToInt for u128}::to_int]:
+    Source: '/cargo/git/checkouts/hax-580ebeee043cdea1/492a34e/hax-lib/src/dummy.rs', lines 155:16-155:38
+    Name pattern: [hax_lib::int::{hax_lib::int::ToInt<u128>}::to_int]
+    Visibility: public -/
+@[rust_fun "hax_lib::int::{hax_lib::int::ToInt<u128>}::to_int"]
+def hax_lib.U128.Insts.Hax_libIntToInt.to_int : Std.U128 → Result hax_lib.int.Int :=
+  fun x => ok (x.val : Int)
+
+/-- [hax_lib::int::{hax_lib::int::ToInt for usize}::to_int]:
+    Source: '/cargo/git/checkouts/hax-580ebeee043cdea1/492a34e/hax-lib/src/dummy.rs', lines 155:16-155:38
+    Name pattern: [hax_lib::int::{hax_lib::int::ToInt<usize>}::to_int]
+    Visibility: public -/
+@[rust_fun "hax_lib::int::{hax_lib::int::ToInt<usize>}::to_int"]
+def hax_lib.Usize.Insts.Hax_libIntToInt.to_int : Std.Usize → Result hax_lib.int.Int :=
+  fun x => ok (x.val : Int)
+
+/-- [hax_lib::int::{hax_lib::int::ToInt for i8}::to_int]:
+    Source: '/cargo/git/checkouts/hax-580ebeee043cdea1/492a34e/hax-lib/src/dummy.rs', lines 155:16-155:38
+    Name pattern: [hax_lib::int::{hax_lib::int::ToInt<i8>}::to_int]
+    Visibility: public -/
+@[rust_fun "hax_lib::int::{hax_lib::int::ToInt<i8>}::to_int"]
+def hax_lib.I8.Insts.Hax_libIntToInt.to_int : Std.I8 → Result hax_lib.int.Int :=
+  fun x => ok x.val
+
+/-- [hax_lib::int::{hax_lib::int::ToInt for i16}::to_int]:
+    Source: '/cargo/git/checkouts/hax-580ebeee043cdea1/492a34e/hax-lib/src/dummy.rs', lines 155:16-155:38
+    Name pattern: [hax_lib::int::{hax_lib::int::ToInt<i16>}::to_int]
+    Visibility: public -/
+@[rust_fun "hax_lib::int::{hax_lib::int::ToInt<i16>}::to_int"]
+def hax_lib.I16.Insts.Hax_libIntToInt.to_int : Std.I16 → Result hax_lib.int.Int :=
+  fun x => ok x.val
+
+/-- [hax_lib::int::{hax_lib::int::ToInt for i32}::to_int]:
+    Source: '/cargo/git/checkouts/hax-580ebeee043cdea1/492a34e/hax-lib/src/dummy.rs', lines 155:16-155:38
+    Name pattern: [hax_lib::int::{hax_lib::int::ToInt<i32>}::to_int]
+    Visibility: public -/
+@[rust_fun "hax_lib::int::{hax_lib::int::ToInt<i32>}::to_int"]
+def hax_lib.I32.Insts.Hax_libIntToInt.to_int : Std.I32 → Result hax_lib.int.Int :=
+  fun x => ok x.val
+
+/-- [hax_lib::int::{hax_lib::int::ToInt for i64}::to_int]:
+    Source: '/cargo/git/checkouts/hax-580ebeee043cdea1/492a34e/hax-lib/src/dummy.rs', lines 155:16-155:38
+    Name pattern: [hax_lib::int::{hax_lib::int::ToInt<i64>}::to_int]
+    Visibility: public -/
+@[rust_fun "hax_lib::int::{hax_lib::int::ToInt<i64>}::to_int"]
+def hax_lib.I64.Insts.Hax_libIntToInt.to_int : Std.I64 → Result hax_lib.int.Int :=
+  fun x => ok x.val
+
+/-- [hax_lib::int::{hax_lib::int::ToInt for i128}::to_int]:
+    Source: '/cargo/git/checkouts/hax-580ebeee043cdea1/492a34e/hax-lib/src/dummy.rs', lines 155:16-155:38
+    Name pattern: [hax_lib::int::{hax_lib::int::ToInt<i128>}::to_int]
+    Visibility: public -/
+@[rust_fun "hax_lib::int::{hax_lib::int::ToInt<i128>}::to_int"]
+def hax_lib.I128.Insts.Hax_libIntToInt.to_int : Std.I128 → Result hax_lib.int.Int :=
+  fun x => ok x.val
+
+/-- [hax_lib::int::{hax_lib::int::ToInt for isize}::to_int]:
+    Source: '/cargo/git/checkouts/hax-580ebeee043cdea1/492a34e/hax-lib/src/dummy.rs', lines 155:16-155:38
+    Name pattern: [hax_lib::int::{hax_lib::int::ToInt<isize>}::to_int]
+    Visibility: public -/
+@[rust_fun "hax_lib::int::{hax_lib::int::ToInt<isize>}::to_int"]
+def hax_lib.Isize.Insts.Hax_libIntToInt.to_int : Std.Isize → Result hax_lib.int.Int :=
+  fun x => ok x.val
+
+end core
+
+end CoreModels

lean/CoreModels/RustPrimitives.lean

@@ -0,0 +1,2 @@
+import CoreModels.RustPrimitives.Types
+import CoreModels.RustPrimitives.Funs