Skip to content

Revm links: more instructions + type annotations for constructors #726

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 2 commits into from
Apr 30, 2025
Merged

Revm links: more instructions + type annotations for constructors #726

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
ce771a7
revm: handle more instructions for links
clarus Apr 18, 2025
3aaedad
feat: add type annotations for constructors
clarus Apr 30, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
The table of contents is too big for display.
Diff view
Diff view
  •  
  •  
  •  
23 changes: 12 additions & 11 deletions CoqOfRust/M.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -180,8 +180,8 @@ Module Value.
| String : string -> t
| Tuple : list t -> t
| Array : list t -> t
| StructRecord : string -> list (string * t) -> t
| StructTuple : string -> list t -> t
| StructRecord : string -> list t -> list Ty.t ->list (string * t) -> t
| StructTuple : string -> list t -> list Ty.t -> list t -> t
| Pointer : Pointer.t t -> t
(** The two existential types of the closure must be [Value.t] and [M]. We
cannot enforce this constraint there yet, but we will do when defining the
Expand Down Expand Up @@ -214,7 +214,7 @@ Module Value.
end
| Pointer.Index.StructRecord constructor field =>
match value with
| StructRecord c fields =>
| StructRecord c _ _ fields =>
if String.eqb c constructor then
List.assoc fields field
else
Expand All @@ -223,7 +223,7 @@ Module Value.
end
| Pointer.Index.StructTuple constructor index =>
match value with
| StructTuple c fields =>
| StructTuple c _ _ fields =>
if String.eqb c constructor then
List.nth_error fields (Z.to_nat index)
else
Expand Down Expand Up @@ -254,18 +254,18 @@ Module Value.
end
| Pointer.Index.StructRecord constructor field =>
match value with
| StructRecord c fields =>
| StructRecord c consts tys fields =>
if String.eqb c constructor then
Some (StructRecord c (List.assoc_replace fields field update))
Some (StructRecord c consts tys (List.assoc_replace fields field update))
else
None
| _ => None
end
| Pointer.Index.StructTuple constructor index =>
match value with
| StructTuple c fields =>
| StructTuple c consts tys fields =>
if String.eqb c constructor then
Some (StructTuple c (List.replace_at fields (Z.to_nat index) update))
Some (StructTuple c consts tys (List.replace_at fields (Z.to_nat index) update))
else
None
| _ => None
Expand Down Expand Up @@ -860,7 +860,7 @@ Definition is_struct_tuple (value : Value.t) (constructor : string) : M :=
let* value := deref value in
let* value := read value in
match value with
| Value.StructTuple current_constructor _ =>
| Value.StructTuple current_constructor _ _ _ =>
if String.eqb current_constructor constructor then
pure (Value.Tuple [])
else
Expand All @@ -882,9 +882,10 @@ Parameter cast : Ty.t -> Value.t -> Value.t.
Definition closure (f : list Value.t -> M) : Value.t :=
Value.Closure (existS (_, _) f).

Definition constructor_as_closure (constructor : string) : Value.t :=
Definition constructor_as_closure (constructor : string) (consts : list Value.t) (tys : list Ty.t) :
Value.t :=
closure (fun args =>
pure (Value.StructTuple constructor args)).
pure (Value.StructTuple constructor consts tys args)).

Parameter struct_record_update : Value.t -> list (string * Value.t) -> Value.t.

Expand Down
74 changes: 67 additions & 7 deletions CoqOfRust/alloc/alloc.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -82,7 +82,7 @@ Module alloc.
(* Default *)
Definition default (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
match ε, τ, α with
| [], [], [] => ltac:(M.monadic (Value.StructTuple "alloc::alloc::Global" []))
| [], [], [] => ltac:(M.monadic (Value.StructTuple "alloc::alloc::Global" [] [] []))
| _, _, _ => M.impossible "wrong number of arguments"
end.

Expand Down Expand Up @@ -442,6 +442,14 @@ Module alloc.
M.alloc (|
Value.StructTuple
"core::result::Result::Ok"
[]
[
Ty.apply
(Ty.path "core::ptr::non_null::NonNull")
[]
[ Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ] ];
Ty.path "core::alloc::AllocError"
]
[
M.call_closure (|
Ty.apply
Expand Down Expand Up @@ -624,7 +632,7 @@ Module alloc.
|),
[ M.read (| raw_ptr |) ]
|);
Value.StructTuple "core::alloc::AllocError" []
Value.StructTuple "core::alloc::AllocError" [] [] []
]
|)
]
Expand Down Expand Up @@ -709,6 +717,14 @@ Module alloc.
M.alloc (|
Value.StructTuple
"core::result::Result::Ok"
[]
[
Ty.apply
(Ty.path "core::ptr::non_null::NonNull")
[]
[ Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ] ];
Ty.path "core::alloc::AllocError"
]
[
M.call_closure (|
Ty.apply
Expand Down Expand Up @@ -1172,7 +1188,7 @@ Module alloc.
|),
[ M.read (| raw_ptr |) ]
|);
Value.StructTuple "core::alloc::AllocError" []
Value.StructTuple "core::alloc::AllocError" [] [] []
]
|)
]
Expand Down Expand Up @@ -1304,6 +1320,14 @@ Module alloc.
M.alloc (|
Value.StructTuple
"core::result::Result::Ok"
[]
[
Ty.apply
(Ty.path "core::ptr::non_null::NonNull")
[]
[ Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ] ];
Ty.path "core::alloc::AllocError"
]
[
M.call_closure (|
Ty.apply
Expand Down Expand Up @@ -1552,7 +1576,17 @@ Module alloc.
|)
|) in
M.alloc (|
Value.StructTuple "core::result::Result::Ok" [ M.read (| new_ptr |) ]
Value.StructTuple
"core::result::Result::Ok"
[]
[
Ty.apply
(Ty.path "core::ptr::non_null::NonNull")
[]
[ Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ] ];
Ty.path "core::alloc::AllocError"
]
[ M.read (| new_ptr |) ]
|)))
]
|)
Expand Down Expand Up @@ -2010,6 +2044,14 @@ Module alloc.
M.alloc (|
Value.StructTuple
"core::result::Result::Ok"
[]
[
Ty.apply
(Ty.path "core::ptr::non_null::NonNull")
[]
[ Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ] ];
Ty.path "core::alloc::AllocError"
]
[
M.call_closure (|
Ty.apply
Expand Down Expand Up @@ -2236,7 +2278,7 @@ Module alloc.
|),
[ M.read (| raw_ptr |) ]
|);
Value.StructTuple "core::alloc::AllocError" []
Value.StructTuple "core::alloc::AllocError" [] [] []
]
|)
]
Expand Down Expand Up @@ -2321,6 +2363,14 @@ Module alloc.
M.alloc (|
Value.StructTuple
"core::result::Result::Ok"
[]
[
Ty.apply
(Ty.path "core::ptr::non_null::NonNull")
[]
[ Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ] ];
Ty.path "core::alloc::AllocError"
]
[
M.call_closure (|
Ty.apply
Expand Down Expand Up @@ -2571,7 +2621,17 @@ Module alloc.
|)
|) in
M.alloc (|
Value.StructTuple "core::result::Result::Ok" [ M.read (| new_ptr |) ]
Value.StructTuple
"core::result::Result::Ok"
[]
[
Ty.apply
(Ty.path "core::ptr::non_null::NonNull")
[]
[ Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ] ];
Ty.path "core::alloc::AllocError"
]
[ M.read (| new_ptr |) ]
|)))
]
|)
Expand Down Expand Up @@ -2652,7 +2712,7 @@ Module alloc.
[
M.borrow (|
Pointer.Kind.Ref,
M.alloc (| Value.StructTuple "alloc::alloc::Global" [] |)
M.alloc (| Value.StructTuple "alloc::alloc::Global" [] [] [] |)
|);
M.read (| layout |)
]
Expand Down
14 changes: 14 additions & 0 deletions CoqOfRust/alloc/borrow.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -217,6 +217,8 @@ Module borrow.
M.alloc (|
Value.StructTuple
"alloc::borrow::Cow::Borrowed"
[]
[ B ]
[ M.borrow (| Pointer.Kind.Ref, M.deref (| M.read (| b |) |) |) ]
|)));
fun γ =>
Expand Down Expand Up @@ -248,6 +250,8 @@ Module borrow.
M.alloc (|
Value.StructTuple
"alloc::borrow::Cow::Owned"
[]
[ B ]
[
M.call_closure (|
Ty.associated_in_trait "alloc::borrow::ToOwned" [] [] B "Owned",
Expand Down Expand Up @@ -528,6 +532,8 @@ Module borrow.
M.deref (| M.read (| self |) |),
Value.StructTuple
"alloc::borrow::Cow::Owned"
[]
[ B ]
[
M.call_closure (|
Ty.associated_in_trait
Expand Down Expand Up @@ -1297,6 +1303,8 @@ Module borrow.
ltac:(M.monadic
(Value.StructTuple
"alloc::borrow::Cow::Owned"
[]
[ B ]
[
M.call_closure (|
Ty.associated_in_trait "alloc::borrow::ToOwned" [] [] B "Owned",
Expand Down Expand Up @@ -1596,6 +1604,8 @@ Module borrow.
M.deref (| M.read (| self |) |),
Value.StructTuple
"alloc::borrow::Cow::Borrowed"
[]
[ Ty.path "str" ]
[ M.borrow (| Pointer.Kind.Ref, M.deref (| M.read (| rhs |) |) |) ]
|)
|)));
Expand Down Expand Up @@ -1724,6 +1734,8 @@ Module borrow.
M.deref (| M.read (| self |) |),
Value.StructTuple
"alloc::borrow::Cow::Owned"
[]
[ Ty.path "str" ]
[ M.read (| s |) ]
|)
|) in
Expand Down Expand Up @@ -2018,6 +2030,8 @@ Module borrow.
M.deref (| M.read (| self |) |),
Value.StructTuple
"alloc::borrow::Cow::Owned"
[]
[ Ty.path "str" ]
[ M.read (| s |) ]
|)
|) in
Expand Down
Loading
Loading