Skip to content

Commit

Permalink
Merge pull request #649 from formal-land/guillaume-claret@have-immuta…
Browse files Browse the repository at this point in the history 
…ble-runs-of-links

Draft: links: more proofs
  • Loading branch information
@clarus
clarus authored Jan 27, 2025
2 parents a7a00dd + ce582bd commit 661d887
Show file tree
Hide file tree
Showing 548 changed files with 8,928 additions and 117,429 deletions.
7 changes: 4 additions & 3 deletions CoqOfRust/M.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -266,7 +266,7 @@ Module Primitive.
| StateWrite (pointer : Pointer.t Value.t) (value : Value.t)
| GetSubPointer (pointer : Pointer.t Value.t) (index : Pointer.Index.t)
| AreEqual (value1 value2 : Value.t)
| GetFunction (path : string) (generic_tys : list Ty.t)
| GetFunction (path : string) (generic_consts : list Value.t) (generic_tys : list Ty.t)
| GetAssociatedFunction (ty : Ty.t) (name : string) (generic_tys : list Ty.t)
| GetTraitMethod
(trait : string)
Expand Down Expand Up @@ -604,8 +604,9 @@ Definition are_equal (value1 value2 : Value.t) : M :=

Parameter get_constant : string -> M.

Definition get_function (path : string) (generic_tys : list Ty.t) : M :=
call_primitive (Primitive.GetFunction path generic_tys).
Definition get_function (path : string) (generic_consts : list Value.t) (generic_tys : list Ty.t) :
M :=
call_primitive (Primitive.GetFunction path generic_consts generic_tys).

Definition get_associated_function
(ty : Ty.t)
Expand Down
47 changes: 25 additions & 22 deletions CoqOfRust/alloc/alloc.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -124,14 +124,14 @@ Module alloc.
let~ _ :=
M.alloc (|
M.call_closure (|
M.get_function (| "core::ptr::read_volatile", [ Ty.path "u8" ] |),
M.get_function (| "core::ptr::read_volatile", [], [ Ty.path "u8" ] |),
[ M.read (| M.get_constant (| "alloc::alloc::__rust_no_alloc_shim_is_unstable" |) |)
]
|)
|) in
M.alloc (|
M.call_closure (|
M.get_function (| "alloc::alloc::__rust_alloc", [] |),
M.get_function (| "alloc::alloc::__rust_alloc", [], [] |),
[
M.call_closure (|
M.get_associated_function (| Ty.path "core::alloc::layout::Layout", "size", [] |),
Expand Down Expand Up @@ -166,7 +166,7 @@ Module alloc.
(let ptr := M.alloc (| ptr |) in
let layout := M.alloc (| layout |) in
M.call_closure (|
M.get_function (| "alloc::alloc::__rust_dealloc", [] |),
M.get_function (| "alloc::alloc::__rust_dealloc", [], [] |),
[
M.read (| ptr |);
M.call_closure (|
Expand Down Expand Up @@ -197,7 +197,7 @@ Module alloc.
let layout := M.alloc (| layout |) in
let new_size := M.alloc (| new_size |) in
M.call_closure (|
M.get_function (| "alloc::alloc::__rust_realloc", [] |),
M.get_function (| "alloc::alloc::__rust_realloc", [], [] |),
[
M.read (| ptr |);
M.call_closure (|
Expand Down Expand Up @@ -236,14 +236,14 @@ Module alloc.
let~ _ :=
M.alloc (|
M.call_closure (|
M.get_function (| "core::ptr::read_volatile", [ Ty.path "u8" ] |),
M.get_function (| "core::ptr::read_volatile", [], [ Ty.path "u8" ] |),
[ M.read (| M.get_constant (| "alloc::alloc::__rust_no_alloc_shim_is_unstable" |) |)
]
|)
|) in
M.alloc (|
M.call_closure (|
M.get_function (| "alloc::alloc::__rust_alloc_zeroed", [] |),
M.get_function (| "alloc::alloc::__rust_alloc_zeroed", [], [] |),
[
M.call_closure (|
M.get_associated_function (| Ty.path "core::alloc::layout::Layout", "size", [] |),
Expand Down Expand Up @@ -356,15 +356,15 @@ Module alloc.
|) in
M.alloc (|
M.call_closure (|
M.get_function (| "alloc::alloc::alloc_zeroed", [] |),
M.get_function (| "alloc::alloc::alloc_zeroed", [], [] |),
[ M.read (| layout |) ]
|)
|)));
fun γ =>
ltac:(M.monadic
(M.alloc (|
M.call_closure (|
M.get_function (| "alloc::alloc::alloc", [] |),
M.get_function (| "alloc::alloc::alloc", [], [] |),
[ M.read (| layout |) ]
|)
|)))
Expand Down Expand Up @@ -619,7 +619,7 @@ Module alloc.
M.alloc (|
M.never_to_any (|
M.call_closure (|
M.get_function (| "core::panicking::panic_fmt", [] |),
M.get_function (| "core::panicking::panic_fmt", [], [] |),
[
M.call_closure (|
M.get_associated_function (|
Expand Down Expand Up @@ -719,7 +719,7 @@ Module alloc.
let~ _ :=
M.alloc (|
M.call_closure (|
M.get_function (| "core::hint::assert_unchecked", [] |),
M.get_function (| "core::hint::assert_unchecked", [], [] |),
[
BinOp.ge (|
M.read (| new_size |),
Expand All @@ -738,7 +738,7 @@ Module alloc.
let~ raw_ptr :=
M.alloc (|
M.call_closure (|
M.get_function (| "alloc::alloc::realloc", [] |),
M.get_function (| "alloc::alloc::realloc", [], [] |),
[
M.call_closure (|
M.get_associated_function (|
Expand Down Expand Up @@ -1039,6 +1039,7 @@ Module alloc.
M.call_closure (|
M.get_function (|
"core::intrinsics::copy_nonoverlapping",
[],
[ Ty.path "u8" ]
|),
[
Expand Down Expand Up @@ -1175,7 +1176,7 @@ Module alloc.
let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
M.alloc (|
M.call_closure (|
M.get_function (| "alloc::alloc::dealloc", [] |),
M.get_function (| "alloc::alloc::dealloc", [], [] |),
[
M.call_closure (|
M.get_associated_function (|
Expand Down Expand Up @@ -1361,7 +1362,7 @@ Module alloc.
M.alloc (|
M.never_to_any (|
M.call_closure (|
M.get_function (| "core::panicking::panic_fmt", [] |),
M.get_function (| "core::panicking::panic_fmt", [], [] |),
[
M.call_closure (|
M.get_associated_function (|
Expand Down Expand Up @@ -1480,7 +1481,7 @@ Module alloc.
let~ _ :=
M.alloc (|
M.call_closure (|
M.get_function (| "core::hint::assert_unchecked", [] |),
M.get_function (| "core::hint::assert_unchecked", [], [] |),
[
BinOp.le (|
M.read (| new_size |),
Expand All @@ -1499,7 +1500,7 @@ Module alloc.
let~ raw_ptr :=
M.alloc (|
M.call_closure (|
M.get_function (| "alloc::alloc::realloc", [] |),
M.get_function (| "alloc::alloc::realloc", [], [] |),
[
M.call_closure (|
M.get_associated_function (|
Expand Down Expand Up @@ -1757,6 +1758,7 @@ Module alloc.
M.call_closure (|
M.get_function (|
"core::intrinsics::copy_nonoverlapping",
[],
[ Ty.path "u8" ]
|),
[
Expand Down Expand Up @@ -1893,7 +1895,7 @@ Module alloc.
M.alloc (|
M.never_to_any (|
M.call_closure (|
M.get_function (| "alloc::alloc::handle_alloc_error", [] |),
M.get_function (| "alloc::alloc::handle_alloc_error", [], [] |),
[ M.read (| layout |) ]
|)
|)
Expand Down Expand Up @@ -1941,6 +1943,7 @@ Module alloc.
M.call_closure (|
M.get_function (|
"core::intrinsics::const_eval_select",
[],
[
Ty.tuple [ Ty.path "core::alloc::layout::Layout" ];
Ty.function [ Ty.path "core::alloc::layout::Layout" ] (Ty.path "never");
Expand All @@ -1950,8 +1953,8 @@ Module alloc.
|),
[
Value.Tuple [ M.read (| layout |) ];
M.get_function (| "alloc::alloc::handle_alloc_error.ct_error", [] |);
M.get_function (| "alloc::alloc::handle_alloc_error.rt_error", [] |)
M.get_function (| "alloc::alloc::handle_alloc_error.ct_error", [], [] |);
M.get_function (| "alloc::alloc::handle_alloc_error.rt_error", [], [] |)
]
|)))
| _, _, _ => M.impossible "wrong number of arguments"
Expand All @@ -1977,7 +1980,7 @@ Module alloc.
fun γ =>
ltac:(M.monadic
(M.call_closure (|
M.get_function (| "core::panicking::panic_fmt", [] |),
M.get_function (| "core::panicking::panic_fmt", [], [] |),
[
M.call_closure (|
M.get_associated_function (|
Expand Down Expand Up @@ -2013,7 +2016,7 @@ Module alloc.
ltac:(M.monadic
(let layout := M.alloc (| layout |) in
M.call_closure (|
M.get_function (| "alloc::alloc::__rust_alloc_error_handler", [] |),
M.get_function (| "alloc::alloc::__rust_alloc_error_handler", [], [] |),
[
M.call_closure (|
M.get_associated_function (| Ty.path "core::alloc::layout::Layout", "size", [] |),
Expand Down Expand Up @@ -2079,7 +2082,7 @@ Module alloc.
let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
M.alloc (|
M.call_closure (|
M.get_function (| "core::panicking::panic_fmt", [] |),
M.get_function (| "core::panicking::panic_fmt", [], [] |),
[
M.call_closure (|
M.get_associated_function (|
Expand Down Expand Up @@ -2117,7 +2120,7 @@ Module alloc.
ltac:(M.monadic
(M.alloc (|
M.call_closure (|
M.get_function (| "core::panicking::panic_nounwind_fmt", [] |),
M.get_function (| "core::panicking::panic_nounwind_fmt", [], [] |),
[
M.call_closure (|
M.get_associated_function (|
Expand Down
2 changes: 1 addition & 1 deletion CoqOfRust/alloc/borrow.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -457,7 +457,7 @@ Module borrow.
M.alloc (|
M.never_to_any (|
M.call_closure (|
M.get_function (| "core::panicking::panic", [] |),
M.get_function (| "core::panicking::panic", [], [] |),
[
M.read (|
Value.String
Expand Down
23 changes: 14 additions & 9 deletions CoqOfRust/alloc/boxed.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -577,7 +577,7 @@ Module boxed.
M.alloc (|
M.never_to_any (|
M.call_closure (|
M.get_function (| "alloc::alloc::handle_alloc_error", [] |),
M.get_function (| "alloc::alloc::handle_alloc_error", [], [] |),
[ M.read (| layout |) ]
|)
|)
Expand Down Expand Up @@ -893,7 +893,7 @@ Module boxed.
M.alloc (|
M.never_to_any (|
M.call_closure (|
M.get_function (| "alloc::alloc::handle_alloc_error", [] |),
M.get_function (| "alloc::alloc::handle_alloc_error", [], [] |),
[ M.read (| layout |) ]
|)
|)
Expand Down Expand Up @@ -1473,7 +1473,7 @@ Module boxed.
let~ alloc :=
M.alloc (|
M.call_closure (|
M.get_function (| "core::ptr::read", [ A ] |),
M.get_function (| "core::ptr::read", [], [ A ] |),
[
M.SubPointer.get_struct_tuple_field (|
M.call_closure (|
Expand Down Expand Up @@ -3742,7 +3742,7 @@ Module boxed.
|) in
M.alloc (|
M.call_closure (|
M.get_function (| "alloc::str::from_boxed_utf8_unchecked", [] |),
M.get_function (| "alloc::str::from_boxed_utf8_unchecked", [], [] |),
[ M.read (| buf |) ]
|)
|)
Expand Down Expand Up @@ -4505,7 +4505,7 @@ Module boxed.
let~ _ :=
M.alloc (|
M.call_closure (|
M.get_function (| "core::intrinsics::copy_nonoverlapping", [ T ] |),
M.get_function (| "core::intrinsics::copy_nonoverlapping", [], [ T ] |),
[
M.call_closure (|
M.get_associated_function (|
Expand Down Expand Up @@ -4734,7 +4734,7 @@ Module boxed.
ltac:(M.monadic
(let s := M.alloc (| s |) in
M.call_closure (|
M.get_function (| "alloc::str::from_boxed_utf8_unchecked", [] |),
M.get_function (| "alloc::str::from_boxed_utf8_unchecked", [], [] |),
[
M.call_closure (|
M.get_trait_method (|
Expand Down Expand Up @@ -5050,6 +5050,7 @@ Module boxed.
M.call_closure (|
M.get_function (|
"core::panicking::assert_failed",
[],
[ Ty.path "usize"; Ty.path "usize" ]
|),
[
Expand Down Expand Up @@ -5179,6 +5180,7 @@ Module boxed.
M.call_closure (|
M.get_function (|
"alloc::boxed::boxed_slice_as_array_unchecked",
[ N ],
[ T; Ty.path "alloc::alloc::Global" ]
|),
[ M.read (| boxed_slice |) ]
Expand Down Expand Up @@ -5295,6 +5297,7 @@ Module boxed.
M.call_closure (|
M.get_function (|
"alloc::boxed::boxed_slice_as_array_unchecked",
[ N ],
[ T; Ty.path "alloc::alloc::Global" ]
|),
[ M.read (| boxed_slice |) ]
Expand Down Expand Up @@ -5449,7 +5452,7 @@ Module boxed.
M.alloc (|
M.never_to_any (|
M.call_closure (|
M.get_function (| "core::panicking::panic", [] |),
M.get_function (| "core::panicking::panic", [], [] |),
[ M.read (| Value.String "assertion failed: self.is::<T>()" |)
]
|)
Expand Down Expand Up @@ -5645,7 +5648,7 @@ Module boxed.
M.alloc (|
M.never_to_any (|
M.call_closure (|
M.get_function (| "core::panicking::panic", [] |),
M.get_function (| "core::panicking::panic", [], [] |),
[ M.read (| Value.String "assertion failed: self.is::<T>()" |)
]
|)
Expand Down Expand Up @@ -5857,7 +5860,7 @@ Module boxed.
M.alloc (|
M.never_to_any (|
M.call_closure (|
M.get_function (| "core::panicking::panic", [] |),
M.get_function (| "core::panicking::panic", [], [] |),
[ M.read (| Value.String "assertion failed: self.is::<T>()" |)
]
|)
Expand Down Expand Up @@ -8013,6 +8016,7 @@ Module boxed.
M.call_closure (|
M.get_function (|
"core::intrinsics::transmute",
[],
[
Ty.apply
(Ty.path "alloc::boxed::Box")
Expand Down Expand Up @@ -8159,6 +8163,7 @@ Module boxed.
M.call_closure (|
M.get_function (|
"core::intrinsics::transmute",
[],
[
Ty.apply
(Ty.path "alloc::boxed::Box")
Expand Down
Loading

0 comments on commit 661d887

Please sign in to comment.