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: Represent values only with their abstract version #542

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

Draft: Represent values only with their abstract version #542

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
dd3755d
feat: remove tag on integers and add revm translation
clarus May 4, 2024
1c082f0
wip: add A.t type
clarus May 5, 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
  •  
  •  
  •  
4 changes: 1 addition & 3 deletions CoqOfRust/CoqOfRust.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -34,10 +34,8 @@ Export List.ListNotations.
Require Export CoqOfRust.M.
Export M.Notations.

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

(** We replace assembly blocks by this special axiom. *)
Parameter InlineAssembly : Value.t.
Parameter InlineAssembly : A.t.

(* Require CoqOfRust.std.arch.
Require CoqOfRust.std.ascii.
Expand Down
158 changes: 97 additions & 61 deletions CoqOfRust/M.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -177,7 +177,7 @@ End Pointer.
Module Value.
Inductive t : Set :=
| Bool : bool -> t
| Integer : Integer.t -> Z -> t
| Integer : Z -> t
(** For now we do not know how to represent floats so we use a string *)
| Float : string -> t
| UnicodeChar : Z -> t
Expand Down Expand Up @@ -328,7 +328,7 @@ Module Value.
Definition eqb (v1 v2 : Value.t) : bool :=
match v1, v2 with
| Value.Bool b1, Value.Bool b2 => Bool.eqb b1 b2
| Value.Integer _ i1, Value.Integer _ i2 => Z.eqb i1 i2
| Value.Integer i1, Value.Integer i2 => Z.eqb i1 i2
| Value.Float f1, Value.Float f2 => String.eqb f1 f2
| Value.UnicodeChar c1, Value.UnicodeChar c2 => Z.eqb c1 c2
| Value.String s1, Value.String s2 => String.eqb s1 s2
Expand All @@ -354,17 +354,29 @@ Module Value.
Qed.
End Value.

Module A.
Inductive t : Set :=
(** We set [to_value] as implicit so that it does not appear when printing the expressions. *)
| Make {A : Set} {to_value : A -> Value.t} (value : A).

Definition to_value (v : t) : Value.t :=
match v with
| @Make _ to_value value => to_value value
end.
End A.

Module Primitive.
Inductive t : Set :=
| StateAlloc (value : Value.t)
| StateAlloc (value : A.t)
| StateRead {A : Set} {to_value : A -> Value.t}
(mutable : Pointer.Mutable.t Value.t to_value)
| StateWrite {A : Set} {to_value : A -> Value.t}
(mutable : Pointer.Mutable.t Value.t to_value)
(value : Value.t)
(value : A.t)
| GetSubPointer {A : Set} {to_value : A -> Value.t}
(mutable : Pointer.Mutable.t Value.t to_value)
(index : Pointer.Index.t)
| OfValue (value : Value.t)
| EnvRead
| GetFunction (path : string) (generic_tys : list Ty.t)
| GetAssociatedFunction (ty : Ty.t) (name : string) (generic_tys : list Ty.t)
Expand All @@ -379,8 +391,8 @@ End Primitive.
Module LowM.
Inductive t (A : Set) : Set :=
| Pure (value : A)
| CallPrimitive (primitive : Primitive.t) (k : Value.t -> t A)
| CallClosure (closure : Value.t) (args : list Value.t) (k : A -> t A)
| CallPrimitive (primitive : Primitive.t) (k : A.t -> t A)
| CallClosure (closure : A.t) (args : list A.t) (k : A -> t A)
| Loop (body : t A) (k : A -> t A)
| Impossible.
Arguments Pure {_}.
Expand All @@ -405,7 +417,7 @@ End LowM.
Module Exception.
Inductive t : Set :=
(** exceptions for Rust's `return` *)
| Return : Value.t -> t
| Return : A.t -> t
(** exceptions for Rust's `continue` *)
| Continue : t
(** exceptions for Rust's `break` *)
Expand All @@ -416,12 +428,12 @@ Module Exception.
End Exception.

Definition M : Set :=
LowM.t (Value.t + Exception.t).
LowM.t (A.t + Exception.t).

Definition pure (v : Value.t) : M :=
Definition pure (v : A.t) : M :=
LowM.Pure (inl v).

Definition let_ (e1 : M) (e2 : Value.t -> M) : M :=
Definition let_ (e1 : M) (e2 : A.t -> M) : M :=
LowM.let_ e1 (fun v1 =>
match v1 with
| inl v1 => e2 v1
Expand All @@ -430,8 +442,8 @@ Definition let_ (e1 : M) (e2 : Value.t -> M) : M :=

Module InstanceField.
Inductive t : Set :=
| Constant (constant : Value.t)
| Method (method : list Ty.t -> list Value.t -> M)
| Constant (constant : A.t)
| Method (method : list Ty.t -> list A.t -> M)
| Ty (ty : Ty.t).
End InstanceField.

Expand All @@ -451,21 +463,21 @@ Parameter IsAssociatedFunction :
forall
(Self : Ty.t)
(function_name : string)
(function : list Ty.t -> list Value.t -> M),
(function : list Ty.t -> list A.t -> M),
Prop.

Parameter IsAssociatedConstant :
forall
(Self : Ty.t)
(constant_name : string)
(constant : Value.t),
(constant : A.t),
Prop.

Parameter IsProvidedMethod :
forall
(trait_name : string)
(method_name : string)
(method : Ty.t -> list Ty.t -> list Value.t -> M),
(method : Ty.t -> list Ty.t -> list A.t -> M),
Prop.

Module Option.
Expand All @@ -487,7 +499,7 @@ End Option.
this markers can be translated to a regular monadic computation using
[M.monadic] tactic. Additionally, this parameter is used for the
definitions of "const".*)
Parameter run : M -> Value.t.
Parameter run : M -> A.t.

Module Notations.
Notation "'let-' a := b 'in' c" :=
Expand Down Expand Up @@ -554,10 +566,23 @@ Ltac monadic e :=
end
end.

Module MList.
Fixpoint map_aux (acc : list A.t) (l : list M) (k : list A.t -> M) : M :=
match l with
| [] => k (List.rev acc)
| e :: l =>
let* v := e in
map_aux (v :: acc) l k
end.

Definition map (l : list M) (k : list A.t -> M) : M :=
map_aux [] l k.
End MList.

Definition raise (exception : Exception.t) : M :=
LowM.Pure (inr exception).

Definition return_ (r : Value.t) : M :=
Definition return_ (r : A.t) : M :=
raise (Exception.Return r).

Definition continue : M :=
Expand All @@ -572,7 +597,7 @@ Definition break_match : M :=
Definition panic (message : string) : M :=
raise (Exception.Panic message).

Definition call_closure (f : Value.t) (args : list Value.t) : M :=
Definition call_closure (f : A.t) (args : list A.t) : M :=
LowM.CallClosure f args LowM.Pure.

Definition impossible : M :=
Expand All @@ -584,36 +609,41 @@ Definition call_primitive (primitive : Primitive.t) : M :=
(* Make it transparent *)
Arguments call_primitive /.

Definition alloc (v : Value.t) : M :=
Definition of_value (v : Value.t) : M :=
call_primitive (Primitive.OfValue v).

Definition alloc (v : A.t) : M :=
call_primitive (Primitive.StateAlloc v).

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

Definition write (r : Value.t) (update : Value.t) : M :=
match r with
Definition write (r : A.t) (update : A.t) : M :=
match A.to_value r with
| Value.Pointer (Pointer.Immediate _) => impossible
| Value.Pointer (Pointer.Mutable mutable) =>
call_primitive (Primitive.StateWrite mutable update)
| _ => impossible
end.

Definition copy (r : Value.t) : M :=
Definition copy (r : A.t) : M :=
let* v := read r in
alloc v.

(** If we cannot get the sub-pointer, due to a field that does not exist or to an out-of bound
access in an array, we do a [break_match]. *)
Definition get_sub_pointer (r : Value.t) (index : Pointer.Index.t) : M :=
match r with
Definition get_sub_pointer (r : A.t) (index : Pointer.Index.t) : M :=
match A.to_value r with
| Value.Pointer (Pointer.Immediate v) =>
match Value.read_path v [index] with
| Some v => alloc v
| Some v =>
let* v := of_value v in
alloc v
| None => break_match
end
| Value.Pointer (Pointer.Mutable mutable) =>
Expand Down Expand Up @@ -669,7 +699,9 @@ Definition catch_continue (body : M) : M :=
body
(fun exception =>
match exception with
| Exception.Continue => alloc (Value.Tuple [])
| Exception.Continue =>
let* tt := of_value (Value.Tuple []) in
alloc tt
| _ => raise exception
end
).
Expand All @@ -679,7 +711,9 @@ Definition catch_break (body : M) : M :=
body
(fun exception =>
match exception with
| Exception.Break => alloc (Value.Tuple [])
| Exception.Break =>
let* tt := of_value (Value.Tuple []) in
alloc tt
| _ => raise exception
end
).
Expand All @@ -691,8 +725,8 @@ Definition loop (body : M) : M :=
catch_break (LowM.Pure result)).

Fixpoint match_operator
(scrutinee : Value.t)
(arms : list (Value.t -> M)) :
(scrutinee : A.t)
(arms : list (A.t -> M)) :
M :=
match arms with
| nil => impossible
Expand All @@ -710,8 +744,8 @@ Fixpoint match_operator
(** Each arm must return a tuple of the free variables found in the pattern. If
no arms are valid, we raise an [Exception.BreakMatch]. *)
Fixpoint find_or_pattern_aux
(scrutinee : Value.t)
(arms : list (Value.t -> M)) :
(scrutinee : A.t)
(arms : list (A.t -> M)) :
M :=
match arms with
| nil => break_match
Expand All @@ -728,68 +762,70 @@ Fixpoint find_or_pattern_aux

(** The [body] must be a closure. *)
Definition find_or_pattern
(scrutinee : Value.t)
(arms : list (Value.t -> M))
(body : Value.t) :
(scrutinee : A.t)
(arms : list (A.t -> M))
(body : A.t) :
M :=
let* free_vars := find_or_pattern_aux scrutinee arms in
match free_vars with
| Value.Tuple free_vars => call_closure body free_vars
match A.to_value free_vars with
| Value.Tuple free_vars =>
MList.map (List.map of_value free_vars) (fun free_vars =>
call_closure body free_vars)
| _ => impossible
end.

Definition never_to_any (x : Value.t) : M :=
Definition never_to_any (x : A.t) : M :=
M.impossible.

Definition use (x : Value.t) : Value.t :=
Definition use (x : A.t) : A.t :=
x.

Module SubPointer.
Definition get_tuple_field (value : Value.t) (index : Z) : M :=
Definition get_tuple_field (value : A.t) (index : Z) : M :=
get_sub_pointer value (Pointer.Index.Tuple index).

Definition get_array_field (value : Value.t) (index : Value.t) : M :=
match index with
| Value.Integer Integer.Usize index =>
get_sub_pointer value (Pointer.Index.Array index)
Definition get_array_field (value : A.t) (index : A.t) : M :=
match A.to_value index with
| Value.Integer index => get_sub_pointer value (Pointer.Index.Array index)
| _ => impossible
end.

Definition get_struct_tuple_field (value : Value.t) (constructor : string) (index : Z) : M :=
Definition get_struct_tuple_field (value : A.t) (constructor : string) (index : Z) : M :=
get_sub_pointer value (Pointer.Index.StructTuple constructor index).

Definition get_struct_record_field (value : Value.t) (constructor field : string) : M :=
Definition get_struct_record_field (value : A.t) (constructor field : string) : M :=
get_sub_pointer value (Pointer.Index.StructRecord constructor field).

(** Get an element of a slice by index. *)
Parameter get_slice_index : Value.t -> Z -> M.
Parameter get_slice_index : A.t -> Z -> M.

(** Get an element of a slice by index counting from the end. *)
Parameter get_slice_rev_index : Value.t -> Z -> M.
Parameter get_slice_rev_index : A.t -> Z -> M.

(** For two indices n and k, get all elements of a slice without
the first n elements and without the last k elements. *)
Parameter get_slice_rest : Value.t -> Z -> Z -> M.
Parameter get_slice_rest : A.t -> Z -> Z -> M.
End SubPointer.

Definition is_constant_or_break_match (value expected_value : Value.t) : M :=
if Value.eqb value expected_value then
pure (Value.Tuple [])
Definition is_constant_or_break_match (value : A.t) (expected_value : Value.t) : M :=
if Value.eqb (A.to_value value) expected_value then
let* tt := of_value (Value.Tuple []) in
pure tt
else
break_match.

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

(** This function is explicitely called in the Rust AST, and should take two
types that are actually different but convertible, like different kinds of
integers. *)
Parameter rust_cast : Value.t -> Value.t.
Parameter rust_cast : A.t -> M.

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

Definition constructor_as_closure (constructor : string) : Value.t :=
Definition constructor_as_closure (constructor : string) : M :=
closure (fun args =>
pure (Value.StructTuple constructor args)).
of_value (Value.StructTuple constructor (List.map A.to_value args))).

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