Skip to content

Commit 0593ef6

Browse files
clarusclarus
committed
wip
1 parent b0d4569 commit 0593ef6

File tree

5 files changed

+320
-32
lines changed

5 files changed

+320
-32
lines changed

‎CoqOfRust/links/M.v‎

Lines changed: 4 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -1008,8 +1008,7 @@ Module Primitive.
10081008
| GetSubPointer {A : Set} `{Link A} {index : Pointer.Index.t}
10091009
(ref_core : Ref.Core.t A) (runner : SubPointer.Runner.t A index) :
10101010
let _ := runner.(SubPointer.Runner.H_Sub_A) in
1011-
t (Ref.Core.t runner.(SubPointer.Runner.Sub_A))
1012-
| AreEqual {A : Set} `{Link A} (x y : A) : t bool.
1011+
t (Ref.Core.t runner.(SubPointer.Runner.Sub_A)).
10131012
End Primitive.
10141013

10151014
Module LowM.
@@ -1018,14 +1017,14 @@ Module LowM.
10181017
Inductive t (R Output : Set) : Set :=
10191018
| Pure (value : Output.t R Output)
10201019
| CallPrimitive {A : Set} (primitive : Primitive.t A) (k : A -> t R Output)
1021-
| Call {A : Set} `{Link A} {e : M} (run : {{ e 🔽 A, A }}) (k : SuccessOrPanic.t A -> t R Output)
1020+
| Call {A : Set} (e : t A A) (k : SuccessOrPanic.t A -> t R Output)
10221021
| LetAlloc {A : Set} `{Link A}
10231022
(e : t R A)
10241023
(k : Output.t R (Ref.t Pointer.Kind.Raw A) -> t R Output)
10251024
| Loop {A : Set} (body : t R A) (k : Output.t R A -> t R Output).
10261025
Arguments Pure {_ _}.
10271026
Arguments CallPrimitive {_ _ _}.
1028-
Arguments Call {_ _ _ _ _}.
1027+
Arguments Call {_ _ _}.
10291028
Arguments LetAlloc {_ _ _ _}.
10301029
Arguments Loop {_ _ _}.
10311030
End LowM.
@@ -1124,7 +1123,7 @@ Proof.
11241123
}
11251124
{ (* CallClosure *)
11261125
eapply (LowM.Call (A := Output')). {
1127-
exact run.
1126+
exact (evaluate _ _ _ _ _ run).
11281127
}
11291128
intros output'; eapply evaluate.
11301129
match goal with

‎CoqOfRust/revm/revm_interpreter/instructions/simulations/arithmetic.v‎

Lines changed: 83 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,89 @@
11
Require Import CoqOfRust.CoqOfRust.
22
Require Import CoqOfRust.links.M.
33
Require Import CoqOfRust.simulations.M.
4-
Import simulations.M.Notations.
5-
Require Import revm.links.dependencies.
4+
Require Import revm.revm_interpreter.links.interpreter.
5+
Require Import revm.revm_interpreter.links.interpreter_types.
6+
Require Import revm.revm_interpreter.simulations.gas.
7+
Require Import revm.revm_interpreter.simulations.interpreter_types.
8+
Require Import revm.revm_interpreter.instructions.links.arithmetic.
9+
10+
Import Impl_Gas.
11+
12+
Instance run_add Stack
13+
{WIRE H : Set} `{Link WIRE} `{Link H}
14+
{WIRE_types : InterpreterTypes.Types.t} `{InterpreterTypes.Types.AreLinks WIRE_types}
15+
`(run_InterpreterTypes_for_WIRE : InterpreterTypes.Run WIRE WIRE_types)
16+
(interpreter : Ref.t Pointer.Kind.MutRef (Interpreter.t WIRE WIRE_types))
17+
(_host : Ref.t Pointer.Kind.MutRef H) :
18+
Run.Trait Stack (links.arithmetic.run_add _ interpreter _host).
19+
Proof.
20+
constructor.
21+
destruct run_InterpreterTypes_for_WIRE.
22+
destruct run_StackTrait_for_Stack, run_LoopControl_for_Control.
23+
(* destruct popn_top as [? []].
24+
destruct gas as [? []].
25+
destruct set_instruction_result as [? []]. *)
26+
Time simulate.
27+
{ Time simulate_destruct; simulate.
28+
match goal with
29+
| H : _ |- Run.Trait ?Stack (_ ?x1 ?x2) =>
30+
apply (H Stack x1 x2)
31+
end.
32+
}
33+
progress cbn in *.
34+
idtac.
35+
(* destruct link; cbn in *.
36+
destruct run_StackTrait_for_Stack, run_LoopControl_for_Control; cbn in *. *)
37+
generalize set_instruction_result; clear; intros.
38+
match goal with
39+
| |- Run.Trait _ (?f _ _) =>
40+
set (f' := f) in |- *
41+
end.
42+
destruct WIRE_types; cbn in *.
43+
destruct link, run_LoopControl_for_Control, set_instruction_result0; cbn in *.
44+
progress fold f' in set_instruction_result.
45+
unfold InterpreterTypes.Types.IsLinkControl in *; cbn in *.
46+
with_strategy transparent [Φ φ] apply set_instruction_result.
47+
progress fold f' in set_instruction_result.
48+
apply set_instruction_result.
49+
match goal with
50+
| H : forall _ _ _, ?f _ _ _ = _ |- _ =>
51+
specialize (H _ _ _ eq_refl)
52+
end.
53+
Check set_instruction_result.
54+
refine (set_instruction_result _ _ _).
55+
best.
56+
match goal with.
57+
dependent apply set_instruction_result.
58+
epose proof (set_instruction_result Stack
59+
(* ((Ref.cast_to Pointer.Kind.MutRef
60+
{|
61+
Ref.core :=
62+
SubPointer.Runner.apply interpreter.(Ref.core)
63+
Interpreter.get_control
64+
|})) *)
65+
(* instruction_result.InstructionResult.OutOfGas *)
66+
).
67+
apply H5.
68+
apply set_instruction_result.
69+
typeclasses eauto.
70+
match goal with
71+
| |- context[if ?condition then _ else _] =>
72+
let condition' := eval cbv in condition in
73+
change condition with condition'
74+
end.
75+
Time match goal with
76+
| |- context[if ?condition then _ else _] =>
77+
destruct condition
78+
end.
79+
{ Show.
80+
simulate_reduce.
81+
82+
}
83+
4: { intros. apply Impl_Gas.run_record_cost.
84+
cbn in output.
85+
Show.
86+
687
(*
788
Require Import revm.interpreter.links.interpreter.
889
Require Import revm.interpreter.interpreter.links.instruction_result.

‎CoqOfRust/revm/revm_interpreter/simulations/gas.v‎

Lines changed: 15 additions & 20 deletions
Original file line numberDiff line numberDiff line change
@@ -15,7 +15,7 @@ Module Impl_MemoryGas.
1515
MemoryGas.t.
1616

1717
Instance run_new Stack :
18-
Run.Trait Stack (links.M.evaluate Impl_MemoryGas.run_new.(Run.run_f)).
18+
Run.Trait Stack Impl_MemoryGas.run_new.
1919
Proof.
2020
constructor.
2121
simulate.
@@ -46,7 +46,7 @@ Module Impl_Gas.
4646
}
4747
*)
4848
Instance run_new Stack (limit : U64.t) :
49-
Run.Trait Stack (links.M.evaluate (Impl_Gas.run_new limit).(Run.run_f)).
49+
Run.Trait Stack (Impl_Gas.run_new limit).
5050
Proof.
5151
constructor.
5252
simulate.
@@ -75,7 +75,7 @@ Module Impl_Gas.
7575
}
7676
*)
7777
Instance run_new_spent Stack (limit : U64.t) :
78-
Run.Trait Stack (links.M.evaluate (Impl_Gas.run_new_spent limit).(Run.run_f)).
78+
Run.Trait Stack (Impl_Gas.run_new_spent limit).
7979
Proof.
8080
constructor.
8181
simulate.
@@ -101,27 +101,12 @@ Module Impl_Gas.
101101
Instance run_limit Stack
102102
(self : Ref.t Pointer.Kind.Ref Self)
103103
(H_self : Stack.CanAccess.t Stack self.(Ref.core)) :
104-
Run.Trait Stack (links.M.evaluate (Impl_Gas.run_limit self).(Run.run_f)).
104+
Run.Trait Stack (Impl_Gas.run_limit self).
105105
Proof.
106106
constructor.
107107
simulate.
108108
Defined.
109109

110-
Lemma limit_eq (self : Self) :
111-
let Stack := [Self] in
112-
let ref_self: Ref.t Pointer.Kind.Ref Self :=
113-
{| Ref.core := Ref.Core.Mutable 0%nat [] φ Some (fun _ => Some) |} in
114-
M.evaluate (
115-
run_limit
116-
[Self]
117-
ref_self
118-
ltac:(apply (Stack.CanAccess.Mutable (A := Gas.t) Stack 0 []))
119-
).(Run.simulation) self =
120-
(Output.Success self.(Gas.limit), self).
121-
Proof.
122-
reflexivity.
123-
Qed.
124-
125110
(*
126111
pub fn erase_cost(&mut self, returned: u64) {
127112
self.remaining += returned;
@@ -131,9 +116,19 @@ Module Impl_Gas.
131116
(self : Ref.t Pointer.Kind.Ref Self)
132117
(H_self : Stack.CanAccess.t Stack self.(Ref.core))
133118
(returned : U64.t) :
134-
Run.Trait Stack (links.M.evaluate (Impl_Gas.run_erase_cost self returned).(Run.run_f)).
119+
Run.Trait Stack (Impl_Gas.run_erase_cost self returned).
135120
Proof.
136121
constructor.
137122
simulate.
138123
Defined.
124+
125+
Instance run_record_cost Stack
126+
(self : Ref.t Pointer.Kind.MutRef Self)
127+
(* (H_self : Stack.CanAccess.t Stack self.(Ref.core)) *)
128+
(cost : U64.t) :
129+
Run.Trait Stack (Impl_Gas.run_record_cost self cost).
130+
Proof.
131+
constructor.
132+
simulate.
133+
Admitted.
139134
End Impl_Gas.

‎CoqOfRust/revm/revm_interpreter/simulations/interpreter_types.v‎

Lines changed: 65 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,65 @@
1+
Require Import CoqOfRust.CoqOfRust.
2+
Require Import CoqOfRust.links.M.
3+
Require Import CoqOfRust.simulations.M.
4+
Require Import revm.revm_interpreter.links.instruction_result.
5+
Require Import revm.revm_interpreter.links.interpreter_types.
6+
7+
Module StackTrait.
8+
Record Run (Self : Set) `{Link Self} (link : StackTrait.Run Self) : Set := {
9+
len Stack self :
10+
Run.Trait Stack (link.(StackTrait.len).(TraitMethod.run) self);
11+
is_empty Stack self :
12+
Run.Trait Stack (link.(StackTrait.is_empty).(TraitMethod.run) self);
13+
push Stack self value :
14+
Run.Trait Stack (link.(StackTrait.push).(TraitMethod.run) self value);
15+
push_b256 Stack self value :
16+
Run.Trait Stack (link.(StackTrait.push_b256).(TraitMethod.run) self value);
17+
popn Stack N self :
18+
Run.Trait Stack (link.(StackTrait.popn).(TraitMethod.run) N self);
19+
popn_top Stack POPN self :
20+
Run.Trait Stack (link.(StackTrait.popn_top).(TraitMethod.run) POPN self);
21+
top Stack self :
22+
Run.Trait Stack (link.(StackTrait.top).(TraitMethod.run) self);
23+
pop Stack self :
24+
Run.Trait Stack (link.(StackTrait.pop).(TraitMethod.run) self);
25+
pop_address Stack self :
26+
Run.Trait Stack (link.(StackTrait.pop_address).(TraitMethod.run) self);
27+
exchange Stack self n m :
28+
Run.Trait Stack (link.(StackTrait.exchange).(TraitMethod.run) self n m);
29+
dup Stack self n :
30+
Run.Trait Stack (link.(StackTrait.dup).(TraitMethod.run) self n);
31+
}.
32+
End StackTrait.
33+
34+
Module LoopControl.
35+
Record Run (Self : Set) `{Link Self} (link : LoopControl.Run Self) : Set := {
36+
set_instruction_result Stack self result :
37+
Run.Trait Stack (link.(LoopControl.set_instruction_result).(TraitMethod.run) self result);
38+
set_next_action Stack self action result :
39+
Run.Trait Stack (link.(LoopControl.set_next_action).(TraitMethod.run) self action result);
40+
gas Stack self :
41+
Run.Trait Stack (link.(LoopControl.gas).(TraitMethod.run) self);
42+
instruction_result Stack self :
43+
Run.Trait Stack (link.(LoopControl.instruction_result).(TraitMethod.run) self);
44+
take_next_action Stack self :
45+
Run.Trait Stack (link.(LoopControl.take_next_action).(TraitMethod.run) self);
46+
}.
47+
End LoopControl.
48+
49+
Module InterpreterTypes.
50+
Class Run
51+
(Self : Set) `{Link Self}
52+
(types : InterpreterTypes.Types.t) `{InterpreterTypes.Types.AreLinks types}
53+
(link : InterpreterTypes.Run Self types) :
54+
Set :=
55+
{
56+
run_StackTrait_for_Stack :
57+
StackTrait.Run
58+
types.(InterpreterTypes.Types.Stack)
59+
link.(InterpreterTypes.run_StackTrait_for_Stack);
60+
run_LoopControl_for_Control :
61+
LoopControl.Run
62+
types.(InterpreterTypes.Types.Control)
63+
link.(InterpreterTypes.run_LoopControl_for_Control);
64+
}.
65+
End InterpreterTypes.

0 commit comments

Comments
 (0)