From fe52fe136cac01a60c00096754ec1f1f7788550e Mon Sep 17 00:00:00 2001 From: Guillaume Claret Date: Thu, 10 Apr 2025 15:34:59 +0200 Subject: [PATCH] experiment --- CoqOfRust/core/convert/links/num.v | 5 +- CoqOfRust/core/links/array.v | 4 +- CoqOfRust/core/links/hint.v | 1 - CoqOfRust/core/links/result.v | 1 + CoqOfRust/links/M.v | 103 ++++++++++++++---- .../instructions/links/i256.v | 22 ---- .../instructions/links/system.v | 1 + .../interpreter/links/stack.v | 2 + .../links/instruction_result.v | 2 +- 9 files changed, 88 insertions(+), 53 deletions(-) diff --git a/CoqOfRust/core/convert/links/num.v b/CoqOfRust/core/convert/links/num.v index 32b267ec5..10e79da16 100644 --- a/CoqOfRust/core/convert/links/num.v +++ b/CoqOfRust/core/convert/links/num.v @@ -18,10 +18,9 @@ Module Impl_TryFrom_u64_for_usize. } { constructor. run_symbolic. - instantiate (1 := Result.Ok _). - with_strategy transparent [φ] reflexivity. + all: admit. } - Defined. + Admitted. Instance run : TryFrom.Run Self U64.t TryFromIntError.t := { TryFrom.try_from := run_try_from; diff --git a/CoqOfRust/core/links/array.v b/CoqOfRust/core/links/array.v index 0baea651c..b9eedb63d 100644 --- a/CoqOfRust/core/links/array.v +++ b/CoqOfRust/core/links/array.v @@ -60,7 +60,7 @@ Proof. Qed. Smpl Add eapply of_value_with_4 : of_value. -Definition of_value_4 +Definition of_value_4 (value1' : Value.t) (H_value1' : OfValue.t value1') (value2' : Value.t) (value2 : OfValue.get_Set H_value1') @@ -76,7 +76,7 @@ Proof. eapply OfValue.Make with (A := t A {| Integer.value := 4 |}). apply of_value_with_4; eassumption. Defined. -Smpl Add eapply of_value_4 : of_value. +Smpl Add unshelve eapply of_value_4; try smpl of_value : of_value. (** This lemma is useful when the [repeat_nat] construct (used to build array with repetition) appears and to switch it with the [φ] on its parameters. *) diff --git a/CoqOfRust/core/links/hint.v b/CoqOfRust/core/links/hint.v index 7aac4c573..3d52dcc6b 100644 --- a/CoqOfRust/core/links/hint.v +++ b/CoqOfRust/core/links/hint.v @@ -7,5 +7,4 @@ Instance run_unreachable_unchecked : Run.Trait hint.unreachable_unchecked [] [] [] Empty_set. Proof. constructor. - run_symbolic. Admitted. diff --git a/CoqOfRust/core/links/result.v b/CoqOfRust/core/links/result.v index 3428a9c62..9d285f0ba 100644 --- a/CoqOfRust/core/links/result.v +++ b/CoqOfRust/core/links/result.v @@ -1,6 +1,7 @@ Require Import CoqOfRust.CoqOfRust. Require Import links.M. Require Import core.result. + Module Result. Inductive t {T E : Set} : Set := | Ok : T -> t diff --git a/CoqOfRust/links/M.v b/CoqOfRust/links/M.v index 71f2aacf8..e7974ac4c 100644 --- a/CoqOfRust/links/M.v +++ b/CoqOfRust/links/M.v @@ -20,6 +20,13 @@ Arguments Φ _ {_}. Global Opaque φ. +Module WrappedLink. + Record t : Type := { + A : Set; + H : Link A; + }. +End WrappedLink. + Smpl Create of_ty. Module OfTy. @@ -877,6 +884,17 @@ Module Run. {{ k (SuccessOrPanic.to_value value_inter) 🔽 R, Output }} ) -> {{ LowM.CallClosure ty closure args k 🔽 R, Output }} + | CallClosureWrapped + (ty : Ty.t) (f : list Value.t -> M) (args : list Value.t) (k : Value.t + Exception.t -> M) + (wrapped_link : WrappedLink.t) : + let Output' : Set := wrapped_link.(WrappedLink.A) in + let _ := wrapped_link.(WrappedLink.H) in + let closure := Value.Closure (existS (_, _) f) in + {{ f args 🔽 Output', Output' }} -> + (forall (value_inter : SuccessOrPanic.t Output'), + {{ k (SuccessOrPanic.to_value value_inter) 🔽 R, Output }} + ) -> + {{ LowM.CallClosure ty closure args k 🔽 R, Output }} | CallLogicalOp (op : LogicalOp.t) (lhs : bool) (rhs : M) (k : Value.t + Exception.t -> M) : {{ rhs 🔽 R, bool }} -> @@ -893,6 +911,16 @@ Module Run. {{ k (Output.to_value value_inter) 🔽 R, Output }} ) -> {{ LowM.Let ty e k 🔽 R, Output }} + | LetWrapped + (ty : Ty.t) (e : M) (k : Value.t + Exception.t -> M) + (wrapped_link : WrappedLink.t) : + let Output' : Set := wrapped_link.(WrappedLink.A) in + let _ := wrapped_link.(WrappedLink.H) in + {{ e 🔽 R, Output' }} -> + (forall (value_inter : Output.t R Output'), + {{ k (Output.to_value value_inter) 🔽 R, Output }} + ) -> + {{ LowM.Let ty e k 🔽 R, Output }} | Loop (ty : Ty.t) (body : M) (k : Value.t + Exception.t -> M) (of_ty : OfTy.t ty) : @@ -1068,6 +1096,15 @@ Proof. | H : forall _ : SuccessOrPanic.t Output', _ |- _ => apply (H output') end. } + { (* CallClosureWrapped *) + eapply LowM.Call. { + exact (evaluate _ _ _ _ _ run). + } + intros output'; eapply evaluate. + match goal with + | H : forall _ : SuccessOrPanic.t Output', _ |- _ => apply (H output') + end. + } { (* CallLogicalOp *) match goal with | H : forall _ : Output.t _ bool, _ |- _ => rename H into H_k @@ -1111,6 +1148,15 @@ Proof. | H : forall _ : Output.t _ Output', _ |- _ => apply (H output') end. } + { (* LetWrapped *) + eapply LowM.Let. { + exact (evaluate _ _ _ _ _ run). + } + intros output'; eapply evaluate. + match goal with + | H : forall _ : Output.t _ Output', _ |- _ => apply (H output') + end. + } { (* Loop *) eapply LowM.Loop. { exact (evaluate _ _ _ _ _ run). @@ -1244,8 +1290,8 @@ Ltac run_symbolic_closure := ]. Ltac run_symbolic_closure_auto := - unshelve eapply Run.CallClosure; [ - now repeat smpl of_ty | + unshelve eapply Run.CallClosureWrapped; [ + econstructor; shelve | try prepare_call; ( ( @@ -1354,9 +1400,6 @@ Ltac rewrite_cast_integer := |] end. -Ltac run_symbolic_let := - unshelve eapply Run.Let; [repeat smpl of_ty | | cbn; intros []]. - Ltac run_symbolic_loop := unshelve eapply Run.Loop; [ smpl of_ty | @@ -1364,6 +1407,8 @@ Ltac run_symbolic_loop := cbn; intros [] ]. +Smpl Create run_symbolic. + Ltac run_symbolic_one_step_immediate := match goal with | |- {{ _ 🔽 _, _ }} => @@ -1380,31 +1425,41 @@ Ltac run_symbolic_one_step_immediate := run_symbolic_get_trait_method || run_symbolic_closure_auto || run_symbolic_logical_op || - run_symbolic_let || run_sub_pointer || run_symbolic_loop || - fold @LowM.let_ + fold @LowM.let_ || + smpl run_symbolic end. -Smpl Create run_symbolic. +Ltac run_symbolic_inner := + (run_symbolic_one_step_immediate; run_symbolic_inner) || + (unshelve eapply Run.LetWrapped; [ + econstructor; shelve | + run_symbolic_inner | + cbn; intros []; + run_symbolic_inner + ]) || + match goal with + | |- context[match Output.Exception.to_exception ?exception with _ => _ end] => + destruct exception; run_symbolic_inner + end || + match goal with + | |- {{ ?expression 🔽 _, _ }} => + match expression with + | context [match ?expression with _ => _ end] => + destruct expression; run_symbolic_inner + end + end || + (* We do our best to make progress, but can stop at any point to debug. *) + idtac. -(** We should use this tactic instead of the ones above, as this one calls all the others. *) Ltac run_symbolic := - progress (repeat ( - run_symbolic_one_step_immediate || - smpl run_symbolic || - match goal with - | |- context[match Output.Exception.to_exception ?exception with _ => _ end] => - destruct exception; run_symbolic - end || - match goal with - | |- {{ ?expression 🔽 _, _ }} => - match expression with - | context [match ?expression with _ => _ end] => - destruct expression; run_symbolic - end - end - )). + (unshelve (progress run_symbolic_inner)); + (* There might be remaining types for branches that are never reached. *) + try ( + exact Empty_set || + typeclasses eauto + ). Axiom is_discriminant_tuple_eq : forall diff --git a/CoqOfRust/revm/revm_interpreter/instructions/links/i256.v b/CoqOfRust/revm/revm_interpreter/instructions/links/i256.v index f284a9000..3206d2e93 100644 --- a/CoqOfRust/revm/revm_interpreter/instructions/links/i256.v +++ b/CoqOfRust/revm/revm_interpreter/instructions/links/i256.v @@ -96,17 +96,6 @@ Instance run_MAX_POSITIVE_VALUE : Proof. constructor. run_symbolic. - with_strategy transparent [φ] apply ( - run_from_limbs - {| Integer.value := 256 |} - {| Integer.value := 4 |} - {| array.value := [ - {| Integer.value := _ |}; - {| Integer.value := _ |}; - {| Integer.value := _ |}; - {| Integer.value := _ |} - ] |} - ). Defined. (* pub const MIN_NEGATIVE_VALUE: U256 *) @@ -116,17 +105,6 @@ Instance run_MIN_NEGATIVE_VALUE : Proof. constructor. run_symbolic. - with_strategy transparent [φ] apply ( - run_from_limbs - {| Integer.value := 256 |} - {| Integer.value := 4 |} - {| array.value := [ - {| Integer.value := _ |}; - {| Integer.value := _ |}; - {| Integer.value := _ |}; - {| Integer.value := _ |} - ] |} - ). Defined. (* const FLIPH_BITMASK_U64: u64 *) diff --git a/CoqOfRust/revm/revm_interpreter/instructions/links/system.v b/CoqOfRust/revm/revm_interpreter/instructions/links/system.v index 6190f937e..7515fe852 100644 --- a/CoqOfRust/revm/revm_interpreter/instructions/links/system.v +++ b/CoqOfRust/revm/revm_interpreter/instructions/links/system.v @@ -45,6 +45,7 @@ Proof. destruct run_MemoryTrait_for_Memory. destruct (Impl_Into_for_From_T.run Impl_From_FixedBytes_32_for_U256.run). destruct (Impl_AsRef_for_Slice.run U8.t). + (* "synthetic" type appearing *) run_symbolic. Admitted. diff --git a/CoqOfRust/revm/revm_interpreter/interpreter/links/stack.v b/CoqOfRust/revm/revm_interpreter/interpreter/links/stack.v index e90b5e2e5..03cd8a658 100644 --- a/CoqOfRust/revm/revm_interpreter/interpreter/links/stack.v +++ b/CoqOfRust/revm/revm_interpreter/interpreter/links/stack.v @@ -203,6 +203,8 @@ Module Impl_Stack. Proof. constructor. run_symbolic. + Unshelve. + all: exact Empty_set || typeclasses eauto. Defined. (* pub fn peek(&self, no_from_top: usize) -> Result *) diff --git a/CoqOfRust/revm/revm_interpreter/links/instruction_result.v b/CoqOfRust/revm/revm_interpreter/links/instruction_result.v index f4429739f..bceeed977 100644 --- a/CoqOfRust/revm/revm_interpreter/links/instruction_result.v +++ b/CoqOfRust/revm/revm_interpreter/links/instruction_result.v @@ -711,7 +711,7 @@ Module Impl_InstructionResult. Proof. (* This is the only one that is fast in this file, for some reasons! *) constructor. - destruct self; run_symbolic. + run_symbolic. Defined. (* pub const fn is_revert(self) -> bool *)