Skip to content

Commit e95bf5f

Browse files
clarusclarus
authored
Merge pull request #539 from formal-land/guillaume-claret@add-core
Add translation of the core library
2 parents a683cda + eddc0ea commit e95bf5f

File tree

211 files changed

+726271
-153
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

211 files changed

+726271
-153
lines changed

‎CoqOfRust/CoqOfRust.v

Lines changed: 0 additions & 86 deletions
Original file line numberDiff line numberDiff line change
@@ -39,92 +39,6 @@ Parameter pointer_coercion : string -> Value.t -> Value.t.
3939
(** We replace assembly blocks by this special axiom. *)
4040
Parameter InlineAssembly : Value.t.
4141

42-
(* Require CoqOfRust.alloc.alloc.
43-
Require CoqOfRust.alloc.borrow.
44-
Require CoqOfRust.alloc.boxed.
45-
Require CoqOfRust.alloc.collections.
46-
Require CoqOfRust.alloc.fmt.
47-
Require CoqOfRust.alloc.rc.
48-
Require CoqOfRust.alloc.slice.
49-
Require CoqOfRust.alloc.str.
50-
Require CoqOfRust.alloc.string.
51-
Require CoqOfRust.alloc.sync.
52-
Require CoqOfRust.alloc.vec.
53-
54-
Module alloc.
55-
Export CoqOfRust.alloc.alloc.
56-
Export CoqOfRust.alloc.borrow.
57-
Export CoqOfRust.alloc.boxed.
58-
Export CoqOfRust.alloc.collections.
59-
Export CoqOfRust.alloc.fmt.
60-
Export CoqOfRust.alloc.rc.
61-
Export CoqOfRust.alloc.slice.
62-
Export CoqOfRust.alloc.str.
63-
Export CoqOfRust.alloc.string.
64-
Export CoqOfRust.alloc.sync.
65-
Export CoqOfRust.alloc.vec.
66-
End alloc. *)
67-
68-
(* Require CoqOfRust.core.alloc.
69-
Require CoqOfRust.core.any.
70-
Require CoqOfRust.core.array.
71-
Require CoqOfRust.core.cell.
72-
Require CoqOfRust.core.char.
73-
Require CoqOfRust.core.clone.
74-
Require CoqOfRust.core.cmp.
75-
Require CoqOfRust.core.convert.*)
76-
Require CoqOfRust.core.default.
77-
(*Require CoqOfRust.core.error.
78-
Require CoqOfRust.core.f32.
79-
Require CoqOfRust.core.fmt.
80-
Require CoqOfRust.core.hash.
81-
Require CoqOfRust.core.intrinsics.
82-
Require CoqOfRust.core.iter.
83-
Require CoqOfRust.core.marker.
84-
Require CoqOfRust.core.mem.
85-
Require CoqOfRust.core.num.
86-
Require CoqOfRust.core.ops.*)
87-
Require CoqOfRust.core.option.
88-
(*Require CoqOfRust.core.panic.
89-
Require CoqOfRust.core.panicking.
90-
Require CoqOfRust.core.primitive.
91-
Require CoqOfRust.core.ptr.
92-
Require CoqOfRust.core.result.
93-
Require CoqOfRust.core.slice.
94-
Require CoqOfRust.core.str.
95-
Require CoqOfRust.core.time.*)
96-
97-
Module core.
98-
(*Export CoqOfRust.core.alloc.
99-
Export CoqOfRust.core.any.
100-
Export CoqOfRust.core.array.
101-
Export CoqOfRust.core.cell.
102-
Export CoqOfRust.core.char.
103-
Export CoqOfRust.core.clone.
104-
Export CoqOfRust.core.cmp.
105-
Export CoqOfRust.core.convert.*)
106-
Export CoqOfRust.core.default.
107-
(*Export CoqOfRust.core.error.
108-
Export CoqOfRust.core.f32.
109-
Export CoqOfRust.core.fmt.
110-
Export CoqOfRust.core.hash.
111-
Export CoqOfRust.core.intrinsics.
112-
Export CoqOfRust.core.iter.
113-
Export CoqOfRust.core.marker.
114-
Export CoqOfRust.core.mem.
115-
Export CoqOfRust.core.num.
116-
Export CoqOfRust.core.ops.*)
117-
Export CoqOfRust.core.option.
118-
(*Export CoqOfRust.core.panic.
119-
Export CoqOfRust.core.panicking.
120-
Export CoqOfRust.core.primitive.
121-
Export CoqOfRust.core.ptr.
122-
Export CoqOfRust.core.result.
123-
Export CoqOfRust.core.slice.
124-
Export CoqOfRust.core.str.
125-
Export CoqOfRust.core.time.*)
126-
End core.
127-
12842
(* Require CoqOfRust.std.arch.
12943
Require CoqOfRust.std.ascii.
13044
Require CoqOfRust.std.assert_matches.

‎CoqOfRust/blacklist.txt

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,11 @@
11
alloc/boxed.v
2+
core/any.v
3+
core/array/mod.v
4+
core/cmp/bytewise.v
5+
core/error.v
6+
core/escape.v
7+
core/iter/adapters/flatten.v
8+
core/net/ip_addr.v
29
examples/default/examples/ink_contracts/proofs/erc20.v
310
examples/axiomatized/examples/custom/provided_method.v
411
examples/axiomatized/examples/rust_book/traits/traits.v

‎CoqOfRust/core/alloc/global.v

Lines changed: 198 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,198 @@
1+
(* Generated by coq-of-rust *)
2+
Require Import CoqOfRust.CoqOfRust.
3+
4+
Module alloc.
5+
Module global.
6+
(* Trait *)
7+
Module GlobalAlloc.
8+
Definition alloc_zeroed (Self : Ty.t) (τ : list Ty.t) (α : list Value.t) : M :=
9+
match τ, α with
10+
| [], [ self; layout ] =>
11+
ltac:(M.monadic
12+
(let self := M.alloc (| self |) in
13+
let layout := M.alloc (| layout |) in
14+
M.read (|
15+
let size :=
16+
M.alloc (|
17+
M.call_closure (|
18+
M.get_associated_function (|
19+
Ty.path "core::alloc::layout::Layout",
20+
"size",
21+
[]
22+
|),
23+
[ layout ]
24+
|)
25+
|) in
26+
let ptr :=
27+
M.alloc (|
28+
M.call_closure (|
29+
M.get_trait_method (|
30+
"core::alloc::global::GlobalAlloc",
31+
Self,
32+
[],
33+
"alloc",
34+
[]
35+
|),
36+
[ M.read (| self |); M.read (| layout |) ]
37+
|)
38+
|) in
39+
let _ :=
40+
M.match_operator (|
41+
M.alloc (| Value.Tuple [] |),
42+
[
43+
fun γ =>
44+
ltac:(M.monadic
45+
(let γ :=
46+
M.use
47+
(M.alloc (|
48+
UnOp.Pure.not
49+
(M.call_closure (|
50+
M.get_associated_function (|
51+
Ty.apply (Ty.path "*mut") [ Ty.path "u8" ],
52+
"is_null",
53+
[]
54+
|),
55+
[ M.read (| ptr |) ]
56+
|))
57+
|)) in
58+
let _ :=
59+
M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
60+
let _ :=
61+
M.alloc (|
62+
M.call_closure (|
63+
M.get_function (|
64+
"core::intrinsics::write_bytes",
65+
[ Ty.path "u8" ]
66+
|),
67+
[ M.read (| ptr |); Value.Integer Integer.U8 0; M.read (| size |) ]
68+
|)
69+
|) in
70+
M.alloc (| Value.Tuple [] |)));
71+
fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
72+
]
73+
|) in
74+
ptr
75+
|)))
76+
| _, _ => M.impossible
77+
end.
78+
79+
Axiom ProvidedMethod_alloc_zeroed :
80+
M.IsProvidedMethod "core::alloc::global::GlobalAlloc" "alloc_zeroed" alloc_zeroed.
81+
Definition realloc (Self : Ty.t) (τ : list Ty.t) (α : list Value.t) : M :=
82+
match τ, α with
83+
| [], [ self; ptr; layout; new_size ] =>
84+
ltac:(M.monadic
85+
(let self := M.alloc (| self |) in
86+
let ptr := M.alloc (| ptr |) in
87+
let layout := M.alloc (| layout |) in
88+
let new_size := M.alloc (| new_size |) in
89+
M.read (|
90+
let new_layout :=
91+
M.alloc (|
92+
M.call_closure (|
93+
M.get_associated_function (|
94+
Ty.path "core::alloc::layout::Layout",
95+
"from_size_align_unchecked",
96+
[]
97+
|),
98+
[
99+
M.read (| new_size |);
100+
M.call_closure (|
101+
M.get_associated_function (|
102+
Ty.path "core::alloc::layout::Layout",
103+
"align",
104+
[]
105+
|),
106+
[ layout ]
107+
|)
108+
]
109+
|)
110+
|) in
111+
let new_ptr :=
112+
M.alloc (|
113+
M.call_closure (|
114+
M.get_trait_method (|
115+
"core::alloc::global::GlobalAlloc",
116+
Self,
117+
[],
118+
"alloc",
119+
[]
120+
|),
121+
[ M.read (| self |); M.read (| new_layout |) ]
122+
|)
123+
|) in
124+
let _ :=
125+
M.match_operator (|
126+
M.alloc (| Value.Tuple [] |),
127+
[
128+
fun γ =>
129+
ltac:(M.monadic
130+
(let γ :=
131+
M.use
132+
(M.alloc (|
133+
UnOp.Pure.not
134+
(M.call_closure (|
135+
M.get_associated_function (|
136+
Ty.apply (Ty.path "*mut") [ Ty.path "u8" ],
137+
"is_null",
138+
[]
139+
|),
140+
[ M.read (| new_ptr |) ]
141+
|))
142+
|)) in
143+
let _ :=
144+
M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
145+
let _ :=
146+
M.alloc (|
147+
M.call_closure (|
148+
M.get_function (|
149+
"core::intrinsics::copy_nonoverlapping",
150+
[ Ty.path "u8" ]
151+
|),
152+
[
153+
(* MutToConstPointer *) M.pointer_coercion (M.read (| ptr |));
154+
M.read (| new_ptr |);
155+
M.call_closure (|
156+
M.get_function (| "core::cmp::min", [ Ty.path "usize" ] |),
157+
[
158+
M.call_closure (|
159+
M.get_associated_function (|
160+
Ty.path "core::alloc::layout::Layout",
161+
"size",
162+
[]
163+
|),
164+
[ layout ]
165+
|);
166+
M.read (| new_size |)
167+
]
168+
|)
169+
]
170+
|)
171+
|) in
172+
let _ :=
173+
M.alloc (|
174+
M.call_closure (|
175+
M.get_trait_method (|
176+
"core::alloc::global::GlobalAlloc",
177+
Self,
178+
[],
179+
"dealloc",
180+
[]
181+
|),
182+
[ M.read (| self |); M.read (| ptr |); M.read (| layout |) ]
183+
|)
184+
|) in
185+
M.alloc (| Value.Tuple [] |)));
186+
fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
187+
]
188+
|) in
189+
new_ptr
190+
|)))
191+
| _, _ => M.impossible
192+
end.
193+
194+
Axiom ProvidedMethod_realloc :
195+
M.IsProvidedMethod "core::alloc::global::GlobalAlloc" "realloc" realloc.
196+
End GlobalAlloc.
197+
End global.
198+
End alloc.

0 commit comments

Comments
 (0)