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 work on the simulations for the gas file #678

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

Draft: more work on the simulations for the gas file #678

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
e2b6bc7
simulations: evaluation of a function with a reference and a sub-pointer
clarus Mar 4, 2025
d9b317a
simulations: special case for the stack with a single element
clarus Mar 5, 2025
568527d
simulations: add a definition for write
clarus Mar 5, 2025
6be7148
simulations: compile the beginning of the gas file
clarus Mar 11, 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
  •  
  •  
  •  
29 changes: 18 additions & 11 deletions CoqOfRust/M.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -131,7 +131,9 @@ Module Pointer.

Module Core.
Inductive t (Value : Set) : Set :=
| Immediate (value : Value)
(** The immediate value is optional in case with have a sub-pointer of an immediate pointer for
an enum case that is not the current one. *)
| Immediate (value : option Value)
| Mutable {Address : Set} (address : Address) (path : Path.t).
Arguments Immediate {_}.
Arguments Mutable {_ _}.
Expand Down Expand Up @@ -301,13 +303,13 @@ Module LowM.
| Pure (value : A)
| CallPrimitive (primitive : Primitive.t) (k : Value.t -> t A)
| CallClosure (ty : Ty.t) (closure : Value.t) (args : list Value.t) (k : A -> t A)
| Let (ty : Ty.t) (e : t A) (k : A -> t A)
| LetAlloc (ty : Ty.t) (e : t A) (k : A -> t A)
| Loop (ty : Ty.t) (body : t A) (k : A -> t A)
| Impossible (message : string).
Arguments Pure {_}.
Arguments CallPrimitive {_}.
Arguments CallClosure {_}.
Arguments Let {_}.
Arguments LetAlloc {_}.
Arguments Loop {_}.
Arguments Impossible {_}.

Expand All @@ -318,8 +320,8 @@ Module LowM.
CallPrimitive primitive (fun v => let_ (k v) e2)
| CallClosure ty f args k =>
CallClosure ty f args (fun v => let_ (k v) e2)
| Let ty e k =>
Let ty e (fun v => let_ (k v) e2)
| LetAlloc ty e k =>
LetAlloc ty e (fun v => let_ (k v) e2)
| Loop ty body k =>
Loop ty body (fun v => let_ (k v) e2)
| Impossible message => Impossible message
Expand Down Expand Up @@ -362,7 +364,7 @@ Definition let_user (ty : Ty.t) (e1 : Value.t) (e2 : Value.t -> Value.t) : Value
e2 e1.

Definition let_user_monadic (ty : Ty.t) (e1 : M) (e2 : Value.t -> M) : M :=
LowM.Let ty e1 (fun v1 =>
LowM.LetAlloc ty e1 (fun v1 =>
match v1 with
| inl v1 => e2 v1
| inr error => LowM.Pure (inr error)
Expand Down Expand Up @@ -693,9 +695,14 @@ Definition get_trait_method

Definition catch (ty : option Ty.t) (body : M) (handler : Exception.t -> M) : M :=
(match ty with
| Some ty => LowM.Let ty
| Some ty => LowM.LetAlloc ty
| None => LowM.let_
end) body (fun result =>
end)
(match ty with
| Some _ => let* body := body in M.read body
| None => body
end)
(fun result =>
match result with
| inl v => LowM.Pure (inl v)
| inr exception => handler exception
Expand Down Expand Up @@ -910,13 +917,13 @@ Fixpoint run_constant (constant : M) : Value.t :=
| Primitive.StateAlloc value =>
Value.Pointer {|
Pointer.kind := Pointer.Kind.Raw;
Pointer.core := Pointer.Core.Immediate value;
Pointer.core := Pointer.Core.Immediate (Some value);
|}
| Primitive.StateRead pointer =>
match pointer with
| Value.Pointer {|
Pointer.kind := Pointer.Kind.Raw;
Pointer.core := Pointer.Core.Immediate value;
Pointer.core := Pointer.Core.Immediate (Some value);
|} =>
value
| _ => Value.Error "expected an immediate raw pointer"
Expand All @@ -925,7 +932,7 @@ Fixpoint run_constant (constant : M) : Value.t :=
end in
run_constant (k value)
| LowM.CallClosure _ _ _ _ => Value.Error "unexpected closure call"
| LowM.Let _ _ _ => Value.Error "unexpected let"
| LowM.LetAlloc _ _ _ => Value.Error "unexpected let-alloc"
| LowM.Loop _ _ _ => Value.Error "unexpected loop"
| LowM.Impossible _ => Value.Error "impossible"
end.
862 changes: 424 additions & 438 deletions CoqOfRust/alloc/alloc.v
View file
Open in desktop

Large diffs are not rendered by default.

Loading
Loading