Skip to content
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

Draft: more for Revm #551

Open
wants to merge 5 commits into
base: main
Choose a base branch
from
Open

Draft: more for Revm #551

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
5 commits
Select commit Hold shift + click to select a range
9e45db4
proof: add gas clone
clarus May 24, 2024
8371711
proof: add default for Gas.t
clarus May 24, 2024
6f6a623
feat: wrap instead of panic mode for overflow
clarus May 25, 2024
844ca0e
proof: beginning of handling of closure traits
clarus May 26, 2024
38e12ee
fix: fix translation of constructors without parameters
clarus May 26, 2024
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
  •  
  •  
  •  
110 changes: 46 additions & 64 deletions CoqOfRust/CoqOfRust.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -39,69 +39,51 @@ Parameter pointer_coercion : string -> Value.t -> Value.t.
(** We replace assembly blocks by this special axiom. *)
Parameter InlineAssembly : Value.t.

(* Require CoqOfRust.std.arch.
Require CoqOfRust.std.ascii.
Require CoqOfRust.std.assert_matches.
Require CoqOfRust.std.async_iter.
Require CoqOfRust.std.backtrace.
Require CoqOfRust.std.char.
Require CoqOfRust.std.collections.
Require CoqOfRust.std.env.
Require CoqOfRust.std.f64.
Require CoqOfRust.std.ffi.
Require CoqOfRust.std.fs.
Require CoqOfRust.std.future.
Require CoqOfRust.std.hash.
Require CoqOfRust.std.hint.
Require CoqOfRust.std.intrinsics.
Require CoqOfRust.std.io.
(* Require CoqOfRust.std.iter. *)
(* Require CoqOfRust.std.iter_type. *)
(* Require CoqOfRust.std.net. *)
Require CoqOfRust.std.ops.
Require CoqOfRust.std.os.
Require CoqOfRust.std.panic.
Require CoqOfRust.std.panicking.
Require CoqOfRust.std.path.
Require CoqOfRust.std.pin.
Require CoqOfRust.std.prelude.
Require CoqOfRust.std.process.
Require CoqOfRust.std.simd.
Require CoqOfRust.std.str.
Require CoqOfRust.std.sync.
Require CoqOfRust.std.task.
Require CoqOfRust.std.thread.
Parameter UnsupportedLiteral : Value.t.

Module std.
Export CoqOfRust.std.arch.
Export CoqOfRust.std.ascii.
Export CoqOfRust.std.backtrace.
Export CoqOfRust.std.char.
Export CoqOfRust.std.collections.
Export CoqOfRust.std.env.
Export CoqOfRust.std.f64.
Export CoqOfRust.std.ffi.
Export CoqOfRust.std.fs.
Export CoqOfRust.std.future.
Export CoqOfRust.std.hash.
Export CoqOfRust.std.hint.
Export CoqOfRust.std.intrinsics.
Export CoqOfRust.std.io.
(* Export CoqOfRust.std.iter. *)
(* Export CoqOfRust.std.net. *)
Export CoqOfRust.std.ops.
Export CoqOfRust.std.os.
Export CoqOfRust.std.panic.
Export CoqOfRust.std.panicking.
Export CoqOfRust.std.path.
Export CoqOfRust.std.pin.
Export CoqOfRust.std.prelude.
Export CoqOfRust.std.process.
Export CoqOfRust.std.simd.
Export CoqOfRust.std.str.
Export CoqOfRust.std.sync.
Export CoqOfRust.std.task.
Export CoqOfRust.std.thread.
End std. *)
(** There is an automatic instanciation of the function traits for closures and functions. *)
Module FunctionTraitAutomaticImpl.
Axiom FunctionImplementsFn :
forall (Args : list Ty.t) (Output : Ty.t),
M.IsTraitInstance
"core::ops::function::Fn"
(Ty.function Args Output)
(* Trait polymorphic types *) [Ty.tuple Args]
(* Instance *) [ ("call", InstanceField.Method (fun τ α =>
match τ, α with
| [], [self; Value.Tuple args] =>
let* self := M.read self in
M.call_closure self args
| _, _ => M.impossible
end
)) ].

Parameter UnsupportedLiteral : Value.t.
Axiom FunctionImplementsFnMut :
forall (Args : list Ty.t) (Output : Ty.t),
M.IsTraitInstance
"core::ops::function::FnMut"
(Ty.function Args Output)
(* Trait polymorphic types *) [Ty.tuple Args]
(* Instance *) [ ("call_mut", InstanceField.Method (fun τ α =>
match τ, α with
| [], [self; Value.Tuple args] =>
let* self := M.read self in
M.call_closure self args
| _, _ => M.impossible
end
)) ].

Axiom FunctionImplementsFnOnce :
forall (Args : list Ty.t) (Output : Ty.t),
M.IsTraitInstance
"core::ops::function::FnOnce"
(Ty.function Args Output)
(* Trait polymorphic types *) [Ty.tuple Args]
(* Instance *) [ ("call_once", InstanceField.Method (fun τ α =>
match τ, α with
| [], [self; Value.Tuple args] =>
M.call_closure self args
| _, _ => M.impossible
end
)) ].
End FunctionTraitAutomaticImpl.
65 changes: 57 additions & 8 deletions CoqOfRust/M.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -190,7 +190,7 @@ Module Value.
(** 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
semantics. *)
| Closure : {'(t, M) : Set * Set @ list t -> M} -> t
| Closure : {'(Value, M) : (Set * Set) @ list Value -> M} -> t
(** A special value that does not appear in the translation, but that we use
to implement primitive functions over values that are not total. We
statically know, from the fact that the source Rust code is well-typed,
Expand Down Expand Up @@ -357,8 +357,7 @@ End Value.
Module Primitive.
Inductive t : Set :=
| StateAlloc (value : Value.t)
| StateRead {A : Set} {to_value : A -> Value.t}
(mutable : Pointer.Mutable.t Value.t to_value)
| StateRead (pointer : Pointer.t Value.t)
| StateWrite {A : Set} {to_value : A -> Value.t}
(mutable : Pointer.Mutable.t Value.t to_value)
(value : Value.t)
Expand All @@ -381,11 +380,13 @@ Module LowM.
| Pure (value : A)
| CallPrimitive (primitive : Primitive.t) (k : Value.t -> t A)
| CallClosure (closure : Value.t) (args : list Value.t) (k : A -> t A)
| Let (e : t A) (k : A -> t A)
| Loop (body : t A) (k : A -> t A)
| Impossible.
Arguments Pure {_}.
Arguments CallPrimitive {_}.
Arguments CallClosure {_}.
Arguments Let {_}.
Arguments Loop {_}.
Arguments Impossible {_}.

Expand All @@ -396,6 +397,8 @@ Module LowM.
CallPrimitive primitive (fun v => let_ (k v) e2)
| CallClosure f args k =>
CallClosure f args (fun v => let_ (k v) e2)
| Let e k =>
Let e (fun v => let_ (k v) e2)
| Loop body k =>
Loop body (fun v => let_ (k v) e2)
| Impossible => Impossible
Expand Down Expand Up @@ -428,6 +431,16 @@ Definition let_ (e1 : M) (e2 : Value.t -> M) : M :=
| inr error => LowM.Pure (inr error)
end).

Definition let_user (e1 : Value.t) (e2 : Value.t -> Value.t) : Value.t :=
e2 e1.

Definition let_user_monadic (e1 : M) (e2 : Value.t -> M) : M :=
LowM.Let e1 (fun v1 =>
match v1 with
| inl v1 => e2 v1
| inr error => LowM.Pure (inr error)
end).

Module InstanceField.
Inductive t : Set :=
| Constant (constant : Value.t)
Expand Down Expand Up @@ -508,6 +521,14 @@ Module Notations.
(let_ b (fun a => c))
(at level 200, a pattern, b at level 100, c at level 200).

Notation "'let~' a := b 'in' c" :=
(let_user b (fun a => c))
(at level 200, b at level 100, a name).

Notation "'let*~' a := b 'in' c" :=
(let_user_monadic b (fun a => c))
(at level 200, b at level 100, a name).

Notation "e (| e1 , .. , en |)" :=
(run ((.. (e e1) ..) en))
(at level 100).
Expand All @@ -523,7 +544,7 @@ Import Notations.
explicit names for all intermediate computation results. *)
Ltac monadic e :=
lazymatch e with
| context ctxt [let v : _ := ?x in @?f v] =>
| context ctxt [let v := ?x in @?f v] =>
refine (let_ _ _);
[ monadic x
| let v' := fresh v in
Expand All @@ -541,6 +562,26 @@ Ltac monadic e :=
]
end
]
(* We uses the `let~` notation for lets that come from the source code, in order to keep this
abstraction barrier. *)
| context ctxt [let~ v := ?x in @?f v] =>
refine (let_user_monadic _ _);
[ monadic x
| let v' := fresh v in
intro v';
let y := (eval cbn beta in (f v')) in
lazymatch context ctxt [let v := x in y] with
| let _ := x in y => monadic y
| _ =>
refine (let_ _ _);
[ monadic y
| let w := fresh "v" in
intro w;
let z := context ctxt [w] in
monadic z
]
end
]
| context ctxt [run ?x] =>
lazymatch context ctxt [run x] with
| run x => monadic x
Expand Down Expand Up @@ -595,9 +636,7 @@ Definition alloc (v : Value.t) : M :=

Definition read (r : Value.t) : M :=
match r with
| Value.Pointer (Pointer.Immediate v) => LowM.Pure (inl v)
| Value.Pointer (Pointer.Mutable mutable) =>
call_primitive (Primitive.StateRead mutable)
| Value.Pointer pointer => call_primitive (Primitive.StateRead pointer)
| _ => impossible
end.

Expand Down Expand Up @@ -783,6 +822,16 @@ Definition is_constant_or_break_match (value expected_value : Value.t) : M :=
else
break_match.

Definition is_struct_tuple (value : Value.t) (constructor : string) : M :=
match value with
| Value.StructTuple current_constructor _ =>
if String.eqb current_constructor constructor then
pure (Value.Tuple [])
else
break_match
| _ => break_match
end.

Parameter pointer_coercion : Value.t -> Value.t.

(** This function is explicitely called in the Rust AST, and should take two
Expand All @@ -791,7 +840,7 @@ Parameter pointer_coercion : Value.t -> Value.t.
Parameter rust_cast : Value.t -> Value.t.

Definition closure (f : list Value.t -> M) : Value.t :=
Value.Closure (existS (Value.t, M) f).
Value.Closure (existS (_, _) f).

Definition constructor_as_closure (constructor : string) : Value.t :=
closure (fun args =>
Expand Down
Loading
Loading