Skip to content

Commit 4e4c40d

Browse files
maximebuysemaximebuyse
authored
Merge pull request #11 from cryspen/lean-restructure
refactor(lean): move hax_lib and rust_primitives into their own dir
2 parents ccae446 + 4ccbc7d commit 4e4c40d

13 files changed

Lines changed: 233 additions & 217 deletions

File tree

‎lean/CoreModels.lean‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,5 @@
11
import CoreModels.Command
22
import CoreModels.Core
33
import CoreModels.Alloc
4+
import CoreModels.HaxLib
5+
import CoreModels.RustPrimitives

‎lean/CoreModels/Alloc/Funs.lean‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -3,11 +3,11 @@
33
import Aeneas
44
import CoreModels.Core.TypesPrologue
55
import CoreModels.Core.Types
6-
import CoreModels.Core.TypesExternal
6+
import CoreModels.RustPrimitives.Types
77
import CoreModels.Alloc.Types
8-
import CoreModels.Core.FunsExternal
8+
import CoreModels.RustPrimitives.Funs
99
import CoreModels.Core.Funs
10-
-- (alloc-side externals live in parent Aeneas.FunsExternal)
10+
-- (alloc-side externals live in parent CoreModels.RustPrimitives)
1111
open CoreModels Aeneas
1212
open Aeneas.Std hiding namespace core alloc
1313
open Result ControlFlow Error

‎lean/CoreModels/Alloc/Types.lean‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -3,8 +3,8 @@
33
import Aeneas
44
import CoreModels.Core.TypesPrologue
55
import CoreModels.Core.Types
6-
import CoreModels.Core.TypesExternal
7-
-- (alloc-side externals live in parent Aeneas.FunsExternal)
6+
import CoreModels.RustPrimitives.Types
7+
-- (alloc-side externals live in parent CoreModels.RustPrimitives)
88
open CoreModels Aeneas
99
open Aeneas.Std hiding namespace core alloc
1010
open Result ControlFlow Error

‎lean/CoreModels/Core/Funs.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -5,7 +5,7 @@ import CoreModels.Core.FunsPrologue
55
import CoreModels.Command
66
import CoreModels.Core.TypesPrologue
77
import CoreModels.Core.Types
8-
import CoreModels.Core.FunsExternal
8+
import CoreModels.RustPrimitives.Funs
99
open CoreModels Aeneas
1010
open Aeneas.Std hiding namespace core alloc
1111
open Result ControlFlow Error

‎lean/CoreModels/Core/FunsPrologue.lean‎

Lines changed: 39 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -78,6 +78,45 @@ instance Isize.Insts.CoreCmpPartialOrdIsize : cmp.PartialOrd Isize Isize := mkIP
7878
abbrev ops.range.Range.Insts.CoreIterTraitsIteratorIterator.next :=
7979
@IteratorRange.next
8080

81+
/-- [core::cmp::impls::{core::cmp::PartialOrd<&0 (B)> for &1 (A)}::lt]:
82+
Source: '/rustc/library/core/src/cmp.rs', lines 2133:8-2133:40
83+
Name pattern: [core::cmp::impls::{core::cmp::PartialOrd<&'1 @A, &'0 @B>}::lt]
84+
Visibility: public -/
85+
@[rust_fun "core::cmp::impls::{core::cmp::PartialOrd<&'1 @A, &'0 @B>}::lt"]
86+
def Shared1A.Insts.CoreCmpPartialOrdShared0B.lt
87+
{A : Type} {B : Type} (PartialOrdInst : cmp.PartialOrd A B) :
88+
A → B → Result Bool := fun a b => do
89+
let o ← PartialOrdInst.partial_cmp a b
90+
match o with
91+
| some cmp.Ordering.Less => ok true
92+
| _ => ok false
93+
94+
/-- [core::cmp::impls::{core::cmp::PartialOrd<&0 (B)> for &1 (A)}::gt]:
95+
Source: '/rustc/library/core/src/cmp.rs', lines 2141:8-2141:40
96+
Name pattern: [core::cmp::impls::{core::cmp::PartialOrd<&'1 @A, &'0 @B>}::gt]
97+
Visibility: public -/
98+
@[rust_fun "core::cmp::impls::{core::cmp::PartialOrd<&'1 @A, &'0 @B>}::gt"]
99+
def Shared1A.Insts.CoreCmpPartialOrdShared0B.gt
100+
{A : Type} {B : Type} (PartialOrdInst : cmp.PartialOrd A B) :
101+
A → B → Result Bool := fun a b => do
102+
let o ← PartialOrdInst.partial_cmp a b
103+
match o with
104+
| some cmp.Ordering.Greater => ok true
105+
| _ => ok false
106+
107+
/-- [core::slice::cmp::{core::cmp::PartialEq<[U]> for [T]}::eq]:
108+
Source: '/rustc/library/core/src/slice/cmp.rs', lines 18:4-18:37
109+
Name pattern: [core::slice::cmp::{core::cmp::PartialEq<[@T], [@U]>}::eq]
110+
Visibility: public -/
111+
@[rust_fun "core::slice::cmp::{core::cmp::PartialEq<[@T], [@U]>}::eq"]
112+
def Slice.Insts.CoreCmpPartialEqSlice.eq
113+
{T : Type} {U : Type} (cmpPartialEqInst : cmp.PartialEq T U) :
114+
Slice T → Slice U → Result Bool := fun s1 s2 =>
115+
if s1.length ≠ s2.length then ok false
116+
else do
117+
let rs ← (s1.val.zip s2.val).mapM (fun p => cmpPartialEqInst.eq p.1 p.2)
118+
ok (rs.all id)
119+
81120
/-! ## Slice -/
82121

83122
def slice.Slice.len {T : Type u} (v : Aeneas.Std.Slice T) : Aeneas.Std.Result Usize :=

‎lean/CoreModels/Core/Types.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@
33
import Aeneas
44
import CoreModels.Command
55
import CoreModels.Core.TypesPrologue
6-
import CoreModels.Core.TypesExternal
6+
import CoreModels.RustPrimitives.Types
77
open CoreModels Aeneas
88
open Aeneas.Std hiding namespace core alloc
99
open Result ControlFlow Error

‎lean/CoreModels/Core/TypesExternal.lean‎

Lines changed: 0 additions & 24 deletions
This file was deleted.

‎lean/CoreModels/HaxLib.lean‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
import CoreModels.HaxLib.Funs

‎lean/CoreModels/HaxLib/Funs.lean‎

Lines changed: 151 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,151 @@
1+
import Aeneas
2+
import CoreModels.Command
3+
import CoreModels.Core.TypesPrologue
4+
import CoreModels.Core.Types
5+
open Aeneas
6+
open Aeneas.Std hiding namespace core
7+
open Result ControlFlow Error
8+
set_option linter.dupNamespace false
9+
set_option linter.hashCommand false
10+
set_option linter.unusedVariables false
11+
12+
namespace CoreModels
13+
14+
namespace core
15+
16+
/-- [hax_lib::int::{core::cmp::PartialOrd<hax_lib::int::Int> for hax_lib::int::Int}::le]:
17+
Source: '/cargo/git/checkouts/hax-580ebeee043cdea1/492a34e/hax-lib/src/dummy.rs', lines 77:46-77:56
18+
Name pattern: [hax_lib::int::{core::cmp::PartialOrd<hax_lib::int::Int, hax_lib::int::Int>}::le]
19+
Visibility: public -/
20+
@[rust_fun
21+
"hax_lib::int::{core::cmp::PartialOrd<hax_lib::int::Int, hax_lib::int::Int>}::le"]
22+
def hax_lib.int.Int.Insts.CoreCmpPartialOrdInt.le
23+
: hax_lib.int.Int → hax_lib.int.Int → Result Bool :=
24+
fun a b => ok (decide (a ≤ b))
25+
26+
/-- [hax_lib::int::{core::ops::arith::Add<hax_lib::int::Int, hax_lib::int::Int> for hax_lib::int::Int}::add]:
27+
Source: '/cargo/git/checkouts/hax-580ebeee043cdea1/492a34e/hax-lib/src/dummy.rs', lines 92:8-92:49
28+
Name pattern: [hax_lib::int::{core::ops::arith::Add<hax_lib::int::Int, hax_lib::int::Int, hax_lib::int::Int>}::add]
29+
Visibility: public -/
30+
@[rust_fun
31+
"hax_lib::int::{core::ops::arith::Add<hax_lib::int::Int, hax_lib::int::Int, hax_lib::int::Int>}::add"]
32+
def hax_lib.int.Int.Insts.CoreOpsArithAddIntInt.add
33+
: hax_lib.int.Int → hax_lib.int.Int → Result hax_lib.int.Int := fun a b => ok (a + b)
34+
35+
/-- [hax_lib::int::{core::ops::arith::Sub<hax_lib::int::Int, hax_lib::int::Int> for hax_lib::int::Int}::sub]:
36+
Source: '/cargo/git/checkouts/hax-580ebeee043cdea1/492a34e/hax-lib/src/dummy.rs', lines 100:8-100:49
37+
Name pattern: [hax_lib::int::{core::ops::arith::Sub<hax_lib::int::Int, hax_lib::int::Int, hax_lib::int::Int>}::sub]
38+
Visibility: public -/
39+
@[rust_fun
40+
"hax_lib::int::{core::ops::arith::Sub<hax_lib::int::Int, hax_lib::int::Int, hax_lib::int::Int>}::sub"]
41+
def hax_lib.int.Int.Insts.CoreOpsArithSubIntInt.sub
42+
: hax_lib.int.Int → hax_lib.int.Int → Result hax_lib.int.Int := fun a b => ok (a - b)
43+
44+
/-- [hax_lib::int::{core::ops::arith::Mul<hax_lib::int::Int, hax_lib::int::Int> for hax_lib::int::Int}::mul]:
45+
Source: '/cargo/git/checkouts/hax-580ebeee043cdea1/492a34e/hax-lib/src/dummy.rs', lines 108:8-108:49
46+
Name pattern: [hax_lib::int::{core::ops::arith::Mul<hax_lib::int::Int, hax_lib::int::Int, hax_lib::int::Int>}::mul]
47+
Visibility: public -/
48+
@[rust_fun
49+
"hax_lib::int::{core::ops::arith::Mul<hax_lib::int::Int, hax_lib::int::Int, hax_lib::int::Int>}::mul"]
50+
def hax_lib.int.Int.Insts.CoreOpsArithMulIntInt.mul
51+
: hax_lib.int.Int → hax_lib.int.Int → Result hax_lib.int.Int := fun a b => ok (a * b)
52+
53+
/-- [hax_lib::int::{hax_lib::int::ToInt for u8}::to_int]:
54+
Source: '/cargo/git/checkouts/hax-580ebeee043cdea1/492a34e/hax-lib/src/dummy.rs', lines 155:16-155:38
55+
Name pattern: [hax_lib::int::{hax_lib::int::ToInt<u8>}::to_int]
56+
Visibility: public -/
57+
@[rust_fun "hax_lib::int::{hax_lib::int::ToInt<u8>}::to_int"]
58+
def hax_lib.U8.Insts.Hax_libIntToInt.to_int : Std.U8 → Result hax_lib.int.Int :=
59+
fun x => ok (x.val : Int)
60+
61+
/-- [hax_lib::int::{hax_lib::int::ToInt for u16}::to_int]:
62+
Source: '/cargo/git/checkouts/hax-580ebeee043cdea1/492a34e/hax-lib/src/dummy.rs', lines 155:16-155:38
63+
Name pattern: [hax_lib::int::{hax_lib::int::ToInt<u16>}::to_int]
64+
Visibility: public -/
65+
@[rust_fun "hax_lib::int::{hax_lib::int::ToInt<u16>}::to_int"]
66+
def hax_lib.U16.Insts.Hax_libIntToInt.to_int : Std.U16 → Result hax_lib.int.Int :=
67+
fun x => ok (x.val : Int)
68+
69+
/-- [hax_lib::int::{hax_lib::int::ToInt for u32}::to_int]:
70+
Source: '/cargo/git/checkouts/hax-580ebeee043cdea1/492a34e/hax-lib/src/dummy.rs', lines 155:16-155:38
71+
Name pattern: [hax_lib::int::{hax_lib::int::ToInt<u32>}::to_int]
72+
Visibility: public -/
73+
@[rust_fun "hax_lib::int::{hax_lib::int::ToInt<u32>}::to_int"]
74+
def hax_lib.U32.Insts.Hax_libIntToInt.to_int : Std.U32 → Result hax_lib.int.Int :=
75+
fun x => ok (x.val : Int)
76+
77+
/-- [hax_lib::int::{hax_lib::int::ToInt for u64}::to_int]:
78+
Source: '/cargo/git/checkouts/hax-580ebeee043cdea1/492a34e/hax-lib/src/dummy.rs', lines 155:16-155:38
79+
Name pattern: [hax_lib::int::{hax_lib::int::ToInt<u64>}::to_int]
80+
Visibility: public -/
81+
@[rust_fun "hax_lib::int::{hax_lib::int::ToInt<u64>}::to_int"]
82+
def hax_lib.U64.Insts.Hax_libIntToInt.to_int : Std.U64 → Result hax_lib.int.Int :=
83+
fun x => ok (x.val : Int)
84+
85+
/-- [hax_lib::int::{hax_lib::int::ToInt for u128}::to_int]:
86+
Source: '/cargo/git/checkouts/hax-580ebeee043cdea1/492a34e/hax-lib/src/dummy.rs', lines 155:16-155:38
87+
Name pattern: [hax_lib::int::{hax_lib::int::ToInt<u128>}::to_int]
88+
Visibility: public -/
89+
@[rust_fun "hax_lib::int::{hax_lib::int::ToInt<u128>}::to_int"]
90+
def hax_lib.U128.Insts.Hax_libIntToInt.to_int : Std.U128 → Result hax_lib.int.Int :=
91+
fun x => ok (x.val : Int)
92+
93+
/-- [hax_lib::int::{hax_lib::int::ToInt for usize}::to_int]:
94+
Source: '/cargo/git/checkouts/hax-580ebeee043cdea1/492a34e/hax-lib/src/dummy.rs', lines 155:16-155:38
95+
Name pattern: [hax_lib::int::{hax_lib::int::ToInt<usize>}::to_int]
96+
Visibility: public -/
97+
@[rust_fun "hax_lib::int::{hax_lib::int::ToInt<usize>}::to_int"]
98+
def hax_lib.Usize.Insts.Hax_libIntToInt.to_int : Std.Usize → Result hax_lib.int.Int :=
99+
fun x => ok (x.val : Int)
100+
101+
/-- [hax_lib::int::{hax_lib::int::ToInt for i8}::to_int]:
102+
Source: '/cargo/git/checkouts/hax-580ebeee043cdea1/492a34e/hax-lib/src/dummy.rs', lines 155:16-155:38
103+
Name pattern: [hax_lib::int::{hax_lib::int::ToInt<i8>}::to_int]
104+
Visibility: public -/
105+
@[rust_fun "hax_lib::int::{hax_lib::int::ToInt<i8>}::to_int"]
106+
def hax_lib.I8.Insts.Hax_libIntToInt.to_int : Std.I8 → Result hax_lib.int.Int :=
107+
fun x => ok x.val
108+
109+
/-- [hax_lib::int::{hax_lib::int::ToInt for i16}::to_int]:
110+
Source: '/cargo/git/checkouts/hax-580ebeee043cdea1/492a34e/hax-lib/src/dummy.rs', lines 155:16-155:38
111+
Name pattern: [hax_lib::int::{hax_lib::int::ToInt<i16>}::to_int]
112+
Visibility: public -/
113+
@[rust_fun "hax_lib::int::{hax_lib::int::ToInt<i16>}::to_int"]
114+
def hax_lib.I16.Insts.Hax_libIntToInt.to_int : Std.I16 → Result hax_lib.int.Int :=
115+
fun x => ok x.val
116+
117+
/-- [hax_lib::int::{hax_lib::int::ToInt for i32}::to_int]:
118+
Source: '/cargo/git/checkouts/hax-580ebeee043cdea1/492a34e/hax-lib/src/dummy.rs', lines 155:16-155:38
119+
Name pattern: [hax_lib::int::{hax_lib::int::ToInt<i32>}::to_int]
120+
Visibility: public -/
121+
@[rust_fun "hax_lib::int::{hax_lib::int::ToInt<i32>}::to_int"]
122+
def hax_lib.I32.Insts.Hax_libIntToInt.to_int : Std.I32 → Result hax_lib.int.Int :=
123+
fun x => ok x.val
124+
125+
/-- [hax_lib::int::{hax_lib::int::ToInt for i64}::to_int]:
126+
Source: '/cargo/git/checkouts/hax-580ebeee043cdea1/492a34e/hax-lib/src/dummy.rs', lines 155:16-155:38
127+
Name pattern: [hax_lib::int::{hax_lib::int::ToInt<i64>}::to_int]
128+
Visibility: public -/
129+
@[rust_fun "hax_lib::int::{hax_lib::int::ToInt<i64>}::to_int"]
130+
def hax_lib.I64.Insts.Hax_libIntToInt.to_int : Std.I64 → Result hax_lib.int.Int :=
131+
fun x => ok x.val
132+
133+
/-- [hax_lib::int::{hax_lib::int::ToInt for i128}::to_int]:
134+
Source: '/cargo/git/checkouts/hax-580ebeee043cdea1/492a34e/hax-lib/src/dummy.rs', lines 155:16-155:38
135+
Name pattern: [hax_lib::int::{hax_lib::int::ToInt<i128>}::to_int]
136+
Visibility: public -/
137+
@[rust_fun "hax_lib::int::{hax_lib::int::ToInt<i128>}::to_int"]
138+
def hax_lib.I128.Insts.Hax_libIntToInt.to_int : Std.I128 → Result hax_lib.int.Int :=
139+
fun x => ok x.val
140+
141+
/-- [hax_lib::int::{hax_lib::int::ToInt for isize}::to_int]:
142+
Source: '/cargo/git/checkouts/hax-580ebeee043cdea1/492a34e/hax-lib/src/dummy.rs', lines 155:16-155:38
143+
Name pattern: [hax_lib::int::{hax_lib::int::ToInt<isize>}::to_int]
144+
Visibility: public -/
145+
@[rust_fun "hax_lib::int::{hax_lib::int::ToInt<isize>}::to_int"]
146+
def hax_lib.Isize.Insts.Hax_libIntToInt.to_int : Std.Isize → Result hax_lib.int.Int :=
147+
fun x => ok x.val
148+
149+
end core
150+
151+
end CoreModels

‎lean/CoreModels/RustPrimitives.lean‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,2 @@
1+
import CoreModels.RustPrimitives.Types
2+
import CoreModels.RustPrimitives.Funs

0 commit comments

Comments
 (0)