diff --git a/CoqOfRust/M.v b/CoqOfRust/M.v index af1fbc53e..1ca78183b 100644 --- a/CoqOfRust/M.v +++ b/CoqOfRust/M.v @@ -13,7 +13,7 @@ Import List.ListNotations. Local Open Scope list. Local Open Scope string. -(** Activate the handling of modulo in `lia`. *) +(** Activate the handling of modulo in `lia`. *) Ltac Zify.zify_post_hook ::= Z.to_euclidean_division_equations. Inductive sigS {A : Type} (P : A -> Set) : Set := diff --git a/CoqOfRust/alloc/slice.v b/CoqOfRust/alloc/slice.v index 5efc959d1..d9a99b4b8 100644 --- a/CoqOfRust/alloc/slice.v +++ b/CoqOfRust/alloc/slice.v @@ -9,7 +9,7 @@ Module slice. let len = b.len(); let (b, alloc) = Box::into_raw_with_allocator(b); Vec::from_raw_parts_in(b as *mut T, len, len, alloc) - } + } } *) Definition into_vec (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M := diff --git a/CoqOfRust/blacklist.txt b/CoqOfRust/blacklist.txt index 3fa8abf08..7ca114cd7 100644 --- a/CoqOfRust/blacklist.txt +++ b/CoqOfRust/blacklist.txt @@ -16,7 +16,7 @@ core/iter/adapters/flatten.v core/net/ip_addr.v core/num/int_sqrt.v token-2022 -# Links that are not working yet +# Links that are not working yet move_sui/links/ -# We ignore the metering for now +# We ignore the metering for now move_sui/simulations/move_bytecode_verifier_meter/lib.v diff --git a/CoqOfRust/core/links/cmpOrdering.v b/CoqOfRust/core/links/cmpOrdering.v index 738d71f22..0eeba5ae5 100644 --- a/CoqOfRust/core/links/cmpOrdering.v +++ b/CoqOfRust/core/links/cmpOrdering.v @@ -54,4 +54,8 @@ Module Ordering. Definition of_value_Greater : OfValue.t (Value.StructTuple "core::cmp::Ordering::Greater" []). Proof. eapply OfValue.Make with (value := Greater); reflexivity. Defined. Smpl Add apply of_value_Greater : of_value. + + Module Impl_PartialOrd_for_Ordering. + + End Impl_PartialOrd_for_Ordering. End Ordering. diff --git a/CoqOfRust/core/links/intrinsics.v b/CoqOfRust/core/links/intrinsics.v index 33b93d98f..d1f202279 100644 --- a/CoqOfRust/core/links/intrinsics.v +++ b/CoqOfRust/core/links/intrinsics.v @@ -16,3 +16,20 @@ Instance run_saturating_add (integer_kind : IntegerKind.t) (x y : Integer.t inte (Integer.t integer_kind). Proof. Admitted. + +Instance run_sub_with_overflow + (x y : Integer.t IntegerKind.U64) : + Run.Trait + intrinsics.intrinsics.sub_with_overflow + [] + [ Φ (Integer.t IntegerKind.U64) ] + [ φ x; φ y ] + (Integer.t IntegerKind.U64 * bool). +Proof. +Admitted. + +Instance run_discriminant_value (ref : Ref.t Pointer.Kind.Ref Ordering.t) : + Run.Trait intrinsics.discriminant_value [] [Φ Ordering.t] [φ ref] + (Integer.t IntegerKind.I8). +Proof. +Admitted. \ No newline at end of file diff --git a/CoqOfRust/core/num/links/error.v b/CoqOfRust/core/num/links/error.v new file mode 100644 index 000000000..e0a07a857 --- /dev/null +++ b/CoqOfRust/core/num/links/error.v @@ -0,0 +1,26 @@ +Require Import CoqOfRust.CoqOfRust. +Require Import CoqOfRust.links.M. +Require Import core.convert.num. + +Module TryFromIntError. + + Inductive t : Set := TryFromIntError_Make. + + Instance TryFromIntError_IsLink : Link t := { + Φ := Ty.path "core::num::error::TryFromIntError"; + φ _ := Value.StructTuple "TryFromIntError" [] + }. + + Definition of_ty : OfTy.t (Ty.path "core::num::error::TryFromIntError"). + Proof. + eapply OfTy.Make with (A := t). + reflexivity. + Defined. + + Smpl Add apply of_ty : of_ty. + +End TryFromIntError. + +Module Impl_try_from_TryFromIntError. + +End Impl_try_from_TryFromIntError. \ No newline at end of file diff --git a/CoqOfRust/lib/lib.v b/CoqOfRust/lib/lib.v index 260d20111..c0b87c137 100644 --- a/CoqOfRust/lib/lib.v +++ b/CoqOfRust/lib/lib.v @@ -141,9 +141,19 @@ End UnOp. Module BinOp. Parameter bit_xor : Value.t -> Value.t -> Value.t. - Parameter bit_and : Value.t -> Value.t -> Value.t. - Parameter bit_or : Value.t -> Value.t -> Value.t. + + Definition bit_and (v1 v2 : Value.t) : Value.t := + match v1, v2 with + | Value.Bool b1, Value.Bool b2 => Value.Bool (andb b1 b2) + | Value.Integer kind1 z1, Value.Integer kind2 z2 => + if IntegerKind.eqb kind1 kind2 then + Value.Integer kind1 (Z.land z1 z2) + else Value.Error "Type error" + | _, _ => Value.Error "Type error" + end. + Parameter bit_or : Value.t -> Value.t -> Value.t. + Definition eq : Value.t -> Value.t -> M := M.are_equal. diff --git a/CoqOfRust/links/M.v b/CoqOfRust/links/M.v index 61aad26ea..812ce7d5a 100644 --- a/CoqOfRust/links/M.v +++ b/CoqOfRust/links/M.v @@ -3,7 +3,7 @@ Require Import CoqOfRust.CoqOfRust. Import List.ListNotations. Local Open Scope list. - + Axiom IsTraitAssociatedType_eq : forall (trait_name : string) @@ -114,6 +114,7 @@ Module PrimitiveEq. End PrimitiveEq. Module Bool. + Global Instance IsLink : Link bool := { Φ := Ty.path "bool"; φ b := Value.Bool b; diff --git a/CoqOfRust/revm/links/dependencies.v b/CoqOfRust/revm/links/dependencies.v index ccf10969f..41c05936f 100644 --- a/CoqOfRust/revm/links/dependencies.v +++ b/CoqOfRust/revm/links/dependencies.v @@ -246,12 +246,381 @@ Module B256. alloy_primitives.bits.links.fixed.FixedBytes.t {| Integer.value := 32 |}. End B256. -Module Address. - Definition t : Set := - alloy_primitives.bits.links.address.Address.t. -End Address. - -Module Bytes. - Definition t : Set := - alloy_primitives.links.bytes_.Bytes.t. -End Bytes. +Module ruint. + Module Impl_Uint. + (* Uint *) + Definition Self (BITS LIMBS : Usize.t) : Set := + Uint.t BITS LIMBS. + + Definition Self_ty (BITS LIMBS : Value.t) : Ty.t := + Ty.apply (Ty.path "ruint::Uint") [ BITS; LIMBS ] []. + + (* pub fn wrapping_add(self, rhs: Self) -> Self *) + Parameter wrapping_add : forall (BITS LIMBS : Value.t), PolymorphicFunction.t. + + Global Instance wrapping_add_IsAssociated : + forall (BITS LIMBS : Value.t), + M.IsAssociatedFunction.Trait + (Self_ty BITS LIMBS) + "wrapping_add" + (wrapping_add BITS LIMBS). + Admitted. + + Global Instance run_wrapping_add : + forall (BITS LIMBS : Usize.t), + forall (x1 x2 : Self BITS LIMBS), + Run.Trait + (wrapping_add (φ BITS) (φ LIMBS)) [] [] [ φ x1; φ x2 ] + (Self BITS LIMBS). + Admitted. + + (* pub const fn to_be_bytes(&self) -> [u8; BYTES] *) + Parameter to_be_bytes : forall (BITS LIMBS : Value.t), PolymorphicFunction.t. + + Global Instance to_be_bytes_IsAssociated : + forall (BITS LIMBS : Value.t), + M.IsAssociatedFunction.Trait + (Self_ty BITS LIMBS) + "to_be_bytes" + (to_be_bytes BITS LIMBS). + Admitted. + + Global Instance run_to_be_bytes : + forall (BITS LIMBS BYTES : Usize.t), + forall (x : Ref.t Pointer.Kind.Ref (Self BITS LIMBS)), + Run.Trait + (to_be_bytes (φ BITS) (φ LIMBS)) [ φ BYTES ] [] [ φ x ] + (array.t U8.t BYTES). + Admitted. + End Impl_Uint. + + Module Impl_bit_for_Uint. + Definition Self (BITS LIMBS : Usize.t) : Set := + Uint.t BITS LIMBS. + + Definition Self_ty (BITS LIMBS : Value.t) : Ty.t := + Ty.apply (Ty.path "ruint::Uint") [BITS; LIMBS] []. + + Parameter bit : forall (BITS LIMBS : Value.t), PolymorphicFunction.t. + + Global Instance bit_IsAssociated : + forall (BITS LIMBS : Value.t), + M.IsAssociatedFunction.Trait + (Self_ty BITS LIMBS) + "bit" + (bit BITS LIMBS). + Admitted. + + Global Instance run_bit : + forall (BITS LIMBS : Usize.t) + (input : Ref.t Pointer.Kind.Ref (Self BITS LIMBS)) + (index : Integer.t IntegerKind.Usize), + Run.Trait (bit (φ BITS) (φ LIMBS)) + [] + [] + [ φ input; φ index ] + bool. + Admitted. + + End Impl_bit_for_Uint. + + Module Impl_is_zero_Uint. + Definition Self (BITS LIMBS : Usize.t) : Set := + Uint.t BITS LIMBS. + + Definition Self_ty (BITS LIMBS : Value.t) : Ty.t := + Ty.apply (Ty.path "ruint::Uint") [ BITS; LIMBS ] []. + + Parameter is_zero : forall (BITS LIMBS : Value.t), PolymorphicFunction.t. + + Global Instance is_zero_IsAssociated : + forall (BITS LIMBS : Value.t), + M.IsAssociatedFunction.Trait + (Self_ty BITS LIMBS) + "is_zero" + (is_zero BITS LIMBS). + Admitted. + + Global Instance run_is_zero : + forall (BITS LIMBS : Usize.t) + (self : Ref.t Pointer.Kind.Ref (Self BITS LIMBS)), + Run.Trait (is_zero (φ BITS) (φ LIMBS)) [] [] [ Ref.IsLink.(φ) self ] bool. + Admitted. + End Impl_is_zero_Uint. + + Module Impl_from_Uint. + Definition Self (BITS LIMBS : Usize.t) : Set := + Uint.t BITS LIMBS. + + Definition Self_ty (BITS LIMBS : Value.t) : Ty.t := + Ty.apply (Ty.path "ruint::Uint") [ BITS; LIMBS ] []. + + (* pub const fn from(value: Usize.t) -> Self *) + Parameter from : forall (BITS LIMBS : Value.t), PolymorphicFunction.t. + + Global Instance from_IsAssociated : + forall (BITS LIMBS : Value.t), + M.IsAssociatedFunction.Trait + (Self_ty BITS LIMBS) + "from" + (from BITS LIMBS). + Admitted. + + Global Instance run_from : + forall (BITS LIMBS : Usize.t) (value : Usize.t), + Run.Trait (from (φ BITS) (φ LIMBS)) [] [] [ φ value ] (Self BITS LIMBS). + Admitted. + + Global Instance run_from_bool : + forall (BITS LIMBS : Usize.t) (value : bool), + Run.Trait (from (φ BITS) (φ LIMBS)) [] [ Φ bool ] [ φ value ] (Self BITS LIMBS). + Admitted. + + End Impl_from_Uint. + + Module Impl_PartialOrd_for_Uint. + Definition Self (BITS LIMBS : Value.t) : Ty.t := + Ty.apply (Ty.path "ruint::Uint") [ BITS; LIMBS ] []. + + Parameter lt : forall (BITS LIMBS : Value.t), PolymorphicFunction.t. + Parameter gt : forall (BITS LIMBS : Value.t), PolymorphicFunction.t. + + Axiom Implements : + forall (BITS LIMBS : Value.t) (trait_tys : list Ty.t), + M.IsTraitInstance + "core::cmp::PartialOrd" + [] + trait_tys + (Self BITS LIMBS) + [ ("lt", InstanceField.Method (lt BITS LIMBS)); ("gt", InstanceField.Method (gt BITS LIMBS)) ]. + + Definition run_lt : + forall (BITS LIMBS : Usize.t), + forall (x1 x2 : Ref.t Pointer.Kind.Ref (Uint.t BITS LIMBS)), + {{ lt (φ BITS) (φ LIMBS) [] [] [ φ x1; φ x2 ] 🔽 bool }}. + Admitted. + + Definition run_gt : + forall (BITS LIMBS : Usize.t), + forall (x1 x2 : Ref.t Pointer.Kind.Ref (Uint.t BITS LIMBS)), + {{ gt (φ BITS) (φ LIMBS) [] [] [ φ x1; φ x2 ] 🔽 bool }}. + Admitted. + + Definition run (BITS LIMBS : Value.t) : + PolymorphicFunction.t. + Proof. + exact (lt BITS LIMBS). + Defined. + End Impl_PartialOrd_for_Uint. + Module Impl_PartialEq_for_Uint. + Definition Self (BITS LIMBS : Value.t) : Ty.t := + Ty.apply (Ty.path "ruint::Uint") [BITS; LIMBS] []. + + Parameter eq : forall (BITS LIMBS : Value.t), PolymorphicFunction.t. + + Axiom Implements : + forall (BITS LIMBS : Value.t) (trait_tys : list Ty.t), + M.IsTraitInstance + "core::cmp::PartialEq" + (* Trait polymorphic consts *) [] + (* Trait polymorphic types *) trait_tys + (Self BITS LIMBS) + (* Instance *) [ ("eq", InstanceField.Method (eq BITS LIMBS)) ]. + + Definition run_eq : + forall (BITS LIMBS : Usize.t), + forall (x1 x2 : Ref.t Pointer.Kind.Ref (Uint.t BITS LIMBS)), + {{ eq (φ BITS) (φ LIMBS) [] [] [ φ x1; φ x2 ] 🔽 bool }}. + Admitted. + + Definition run (BITS LIMBS : Value.t) : + PolymorphicFunction.t. + Proof. + exact (eq BITS LIMBS). + Defined. + End Impl_PartialEq_for_Uint. + + + Module Impl_BitAnd_for_Uint. + Definition Self (BITS LIMBS : Value.t) : Ty.t := + Ty.apply (Ty.path "ruint::Uint") [BITS; LIMBS] []. + + Parameter bitand : forall (BITS LIMBS : Value.t), PolymorphicFunction.t. + + Axiom Implements : + forall (BITS LIMBS : Value.t), + M.IsTraitInstance + "core::ops::bit::BitAnd" + [] + [Ty.apply (Ty.path "ruint::Uint") [BITS; LIMBS] []] + (Self BITS LIMBS) + [("bitand", InstanceField.Method (bitand BITS LIMBS))]. + + Instance run_bitand : + forall (BITS LIMBS : Usize.t) + (x y : Uint.t BITS LIMBS), + Run.Trait (bitand (φ BITS) (φ LIMBS)) [] [] [ φ x; φ y ] (Uint.t BITS LIMBS). + Proof. + Admitted. + End Impl_BitAnd_for_Uint. + + Module Impl_BitOr_for_Uint. + Definition Self (BITS LIMBS : Value.t) : Ty.t := + Ty.apply (Ty.path "ruint::Uint") [BITS; LIMBS] []. + + Parameter bitor : forall (BITS LIMBS : Value.t), PolymorphicFunction.t. + + Axiom Implements : + forall (BITS LIMBS : Value.t), + M.IsTraitInstance + "core::ops::bit::BitOr" + [] + [Ty.apply (Ty.path "ruint::Uint") [BITS; LIMBS] []] + (Self BITS LIMBS) + [("bitor", InstanceField.Method (bitor BITS LIMBS))]. + + Instance run_bitor : + forall (BITS LIMBS : Usize.t) + (x y : Uint.t BITS LIMBS), + Run.Trait (bitor (φ BITS) (φ LIMBS)) [] [] [ φ x; φ y ] (Uint.t BITS LIMBS). + Proof. + Admitted. + End Impl_BitOr_for_Uint. + + Module Impl_BitXor_for_Uint. + Definition Self (BITS LIMBS : Value.t) : Ty.t := + Ty.apply (Ty.path "ruint::Uint") [BITS; LIMBS] []. + + Parameter bitxor : forall (BITS LIMBS : Value.t), PolymorphicFunction.t. + + Axiom Implements : + forall (BITS LIMBS : Value.t), + M.IsTraitInstance + "core::ops::bit::BitXor" + [] + [Ty.apply (Ty.path "ruint::Uint") [BITS; LIMBS] []] + (Self BITS LIMBS) + [("bitxor", InstanceField.Method (bitxor BITS LIMBS))]. + + Instance run_bitxor : + forall (BITS LIMBS : Usize.t) + (x y : Uint.t BITS LIMBS), + Run.Trait (bitxor (φ BITS) (φ LIMBS)) [] [] [ φ x; φ y ] (Uint.t BITS LIMBS). + Proof. + Admitted. + End Impl_BitXor_for_Uint. + + Module Impl_BitNot_for_Uint. + Definition Self (BITS LIMBS : Value.t) : Ty.t := + Ty.apply (Ty.path "ruint::Uint") [BITS; LIMBS] []. + + Parameter bitnot : forall (BITS LIMBS : Value.t), PolymorphicFunction.t. + + Axiom Implements : + forall (BITS LIMBS : Value.t), + M.IsTraitInstance + "core::ops::bit::Not" + [] + [] + (Self BITS LIMBS) + [("not", InstanceField.Method (bitnot BITS LIMBS))]. + + Instance run_bitnot : + forall (BITS LIMBS : Usize.t) + (x : Uint.t BITS LIMBS), + Run.Trait (bitnot (φ BITS) (φ LIMBS)) [] [] [ φ x ] (Uint.t BITS LIMBS). + Proof. + Admitted. + End Impl_BitNot_for_Uint. + Module Impl_ArithmeticShr_for_Uint. + Definition Self (BITS LIMBS : Value.t) : Ty.t := + Ty.apply (Ty.path "ruint::Uint") [ BITS; LIMBS ] []. + + Parameter arithmetic_shr : + forall (BITS LIMBS : Value.t), PolymorphicFunction.t. + + Axiom Implements : + forall (BITS LIMBS : Value.t), + IsAssociatedFunction.t (Self BITS LIMBS) "arithmetic_shr" (arithmetic_shr BITS LIMBS). + + Instance run_arithmetic_shr : + forall (BITS LIMBS : Usize.t) + (x1 : Uint.t BITS LIMBS) + (x2 : Integer.t IntegerKind.Usize), + Run.Trait (arithmetic_shr (φ BITS) (φ LIMBS)) [] [] [ φ x1; φ x2 ] (Uint.t BITS LIMBS). + Proof. + Admitted. + End Impl_ArithmeticShr_for_Uint. + + Module Impl_Shr_for_Uint. + Definition Self (BITS LIMBS : Value.t) : Ty.t := + Ty.apply (Ty.path "ruint::Uint") [ BITS; LIMBS ] []. + + Parameter shr : forall (BITS LIMBS : Value.t), PolymorphicFunction.t. + + Axiom Implements : + forall (BITS LIMBS : Value.t), + IsTraitInstance "core::ops::bit::Shr" + [] + [Ty.path "usize"] + (Self BITS LIMBS) + [("shr", InstanceField.Method (shr BITS LIMBS))]. + + Instance run_shr : + forall (BITS LIMBS : Usize.t) + (x1 : Uint.t BITS LIMBS) + (x2 : Integer.t IntegerKind.Usize), + Run.Trait (shr (φ BITS) (φ LIMBS)) [] [] [ φ x1; φ x2 ] (Uint.t BITS LIMBS). + Proof. + Admitted. + End Impl_Shr_for_Uint. + + Module Impl_Shl_for_Uint. + Definition Self (BITS LIMBS : Value.t) : Ty.t := + Ty.apply (Ty.path "ruint::Uint") [ BITS; LIMBS ] []. + + Parameter shl : forall (BITS LIMBS : Value.t), PolymorphicFunction.t. + + Axiom Implements : + forall (BITS LIMBS : Value.t), + IsTraitInstance "core::ops::bit::Shl" + [] + [Ty.path "usize"] + (Self BITS LIMBS) + [("shl", InstanceField.Method (shl BITS LIMBS))]. + + Instance run_shl : + forall (BITS LIMBS : Usize.t) + (x1 : Uint.t BITS LIMBS) + (x2 : Integer.t IntegerKind.Usize), + Run.Trait (shl (φ BITS) (φ LIMBS)) [] [] [ φ x1; φ x2 ] (Uint.t BITS LIMBS). + Proof. + Admitted. + End Impl_Shl_for_Uint. + + Module Impl_AsLimbs_Uint. + Definition Self (BITS LIMBS : Usize.t) : Set := + Uint.t BITS LIMBS. + + Parameter as_limbs : forall (BITS LIMBS : Value.t), PolymorphicFunction.t. + + Axiom Implements_AsLimbs : + forall (BITS LIMBS : Value.t), + IsAssociatedFunction.Trait + (Ty.apply (Ty.path "ruint::Uint") [BITS; LIMBS] []) + "as_limbs" + (as_limbs BITS LIMBS). + + Global Instance run_as_limbs : + forall (BITS LIMBS : Usize.t) + (x : Ref.t Pointer.Kind.Ref (Self BITS LIMBS)), + Run.Trait + (as_limbs (φ BITS) (φ LIMBS)) [] [] [ φ x ] + (Ref.t Pointer.Kind.Ref (array.t (Integer.t IntegerKind.U64) LIMBS)). + Admitted. + + End Impl_AsLimbs_Uint. + + + +End ruint. diff --git a/CoqOfRust/revm/revm_interpreter/instructions/i256.v b/CoqOfRust/revm/revm_interpreter/instructions/i256.v index 3c0e1e8b4..febeadacf 100644 --- a/CoqOfRust/revm/revm_interpreter/instructions/i256.v +++ b/CoqOfRust/revm/revm_interpreter/instructions/i256.v @@ -913,7 +913,7 @@ Module instructions. |))) | _, _, _ => M.impossible "wrong number of arguments" end. - + Global Instance Instance_IsFunction_i256_cmp : M.IsFunction.Trait "revm_interpreter::instructions::i256::i256_cmp" i256_cmp. Admitted. diff --git a/CoqOfRust/revm/revm_interpreter/instructions/links/bitwise.v b/CoqOfRust/revm/revm_interpreter/instructions/links/bitwise.v new file mode 100644 index 000000000..d039a9ad6 --- /dev/null +++ b/CoqOfRust/revm/revm_interpreter/instructions/links/bitwise.v @@ -0,0 +1,566 @@ +Require Import CoqOfRust.CoqOfRust. +Require Import CoqOfRust.links.M. +Require Import core.links.intrinsics. +Require Import core.cmp. +Require Import core.result. +Require Import core.convert.num. +Require Import revm.revm_context_interface.links.host. +Require Import revm.links.dependencies. +Import dependencies.ruint. +Require Import revm.revm_interpreter.links.gas. +Require Import revm.revm_interpreter.links.interpreter. +Require Import revm.revm_interpreter.links.interpreter_types. +Require Import revm.revm_interpreter.instructions.links.i256. +Require Import revm.revm_interpreter.instructions.bitwise. +Require Import revm.revm_interpreter.instructions.i256. +Require Import revm.revm_specification.links.hardfork. +Require Import core.num.links.error. +Import Impl_Gas. +Import Impl_SpecId. +Import Impl_AsLimbs_Uint. +Import convert.num.ptr_try_from_impls. +Import Impl_core_convert_TryFrom_usize_for_u64. +Import Impl_core_convert_TryFrom_u64_for_usize. + +(* +pub fn lt( + interpreter: &mut Interpreter, + _host: &mut H, +) +*) + +Instance run_lt + {WIRE H : Set} `{Link WIRE} `{Link H} + {WIRE_types : InterpreterTypes.Types.t} `{InterpreterTypes.Types.AreLinks WIRE_types} + (run_InterpreterTypes_for_WIRE : InterpreterTypes.Run WIRE WIRE_types) + (interpreter : Ref.t Pointer.Kind.MutRef (Interpreter.t WIRE WIRE_types)) + (_host : Ref.t Pointer.Kind.MutRef H) : + Run.Trait + instructions.bitwise.lt [] [ Φ WIRE; Φ H ] [ φ interpreter; φ _host ] + unit. +Proof. + constructor. + cbn. + eapply Run.Rewrite. { + repeat erewrite IsTraitAssociatedType_eq by apply run_InterpreterTypes_for_WIRE. + reflexivity. + } + destruct run_InterpreterTypes_for_WIRE. + destruct run_StackTrait_for_Stack. + run_symbolic. + + destruct run_LoopControl_for_Control. + run_symbolic. + + eapply Run.CallPrimitiveGetTraitMethod. + ++ specialize (dependencies.ruint.Impl_PartialOrd_for_Uint.run_lt + {| Integer.value := 256 |} + {| Integer.value := 4 |} + (Ref.cast_to Pointer.Kind.Ref value0) + (Ref.cast_to Pointer.Kind.Ref (Ref.immediate Pointer.Kind.Raw value))). + intros. + unfold dependencies.ruint.Impl_PartialOrd_for_Uint.Self in H3. + eapply IsTraitMethod.Defined. + - eapply dependencies.ruint.Impl_PartialOrd_for_Uint.Implements. + - simpl. reflexivity. + ++ run_symbolic. + constructor. + exact (dependencies.ruint.Impl_PartialOrd_for_Uint.run_lt + {| Integer.value := 256 |} + {| Integer.value := 4 |} + (Ref.cast_to Pointer.Kind.Ref (Ref.immediate Pointer.Kind.Raw value)) + (Ref.cast_to Pointer.Kind.Ref value0)). +Defined. + + +Instance run_gt + {WIRE H : Set} `{Link WIRE} `{Link H} + {WIRE_types : InterpreterTypes.Types.t} `{InterpreterTypes.Types.AreLinks WIRE_types} + (run_InterpreterTypes_for_WIRE : InterpreterTypes.Run WIRE WIRE_types) + (interpreter : Ref.t Pointer.Kind.MutRef (Interpreter.t WIRE WIRE_types)) + (_host : Ref.t Pointer.Kind.MutRef H) : + Run.Trait + instructions.bitwise.gt [] [ Φ WIRE; Φ H ] [ φ interpreter; φ _host ] + unit. +Proof. + constructor. + cbn. + eapply Run.Rewrite. { + repeat erewrite IsTraitAssociatedType_eq by apply run_InterpreterTypes_for_WIRE. + reflexivity. + } + destruct run_InterpreterTypes_for_WIRE. + destruct run_StackTrait_for_Stack. + run_symbolic. + + destruct run_LoopControl_for_Control. + run_symbolic. + + eapply Run.CallPrimitiveGetTraitMethod. + ++ specialize (dependencies.ruint.Impl_PartialOrd_for_Uint.run_gt + {| Integer.value := 256 |} + {| Integer.value := 4 |} + (Ref.cast_to Pointer.Kind.Ref value0) + (Ref.cast_to Pointer.Kind.Ref (Ref.immediate Pointer.Kind.Raw value))). + intros. + unfold dependencies.ruint.Impl_PartialOrd_for_Uint.Self in H3. + eapply IsTraitMethod.Defined. + - eapply dependencies.ruint.Impl_PartialOrd_for_Uint.Implements. + - simpl. reflexivity. + ++ run_symbolic. + constructor. + exact (dependencies.ruint.Impl_PartialOrd_for_Uint.run_gt + {| Integer.value := 256 |} + {| Integer.value := 4 |} + (Ref.cast_to Pointer.Kind.Ref (Ref.immediate Pointer.Kind.Raw value)) + (Ref.cast_to Pointer.Kind.Ref value0)). +Defined. + +Instance run_slt + {WIRE H : Set} `{Link WIRE} `{Link H} + {WIRE_types : InterpreterTypes.Types.t} `{InterpreterTypes.Types.AreLinks WIRE_types} + (run_InterpreterTypes_for_WIRE : InterpreterTypes.Run WIRE WIRE_types) + (interpreter : Ref.t Pointer.Kind.MutRef (Interpreter.t WIRE WIRE_types)) + (_host : Ref.t Pointer.Kind.MutRef H) : + Run.Trait + instructions.bitwise.slt [] [ Φ WIRE; Φ H ] [ φ interpreter; φ _host ] + unit. +Proof. + constructor. + cbn. + eapply Run.Rewrite. { + repeat erewrite IsTraitAssociatedType_eq by apply run_InterpreterTypes_for_WIRE. + reflexivity. + } + destruct run_InterpreterTypes_for_WIRE. + destruct run_StackTrait_for_Stack. + run_symbolic. + + destruct run_LoopControl_for_Control. + run_symbolic. + + eapply Run.CallPrimitiveGetTraitMethod. + ++ specialize (cmp.Impl_core_cmp_PartialEq_core_cmp_Ordering_for_core_cmp_Ordering.Implements). + intros. + unfold cmp.Impl_core_cmp_PartialEq_core_cmp_Ordering_for_core_cmp_Ordering.Self in H3. + eapply IsTraitMethod.Defined. + - eapply cmp.Impl_core_cmp_PartialEq_core_cmp_Ordering_for_core_cmp_Ordering.Implements. + - simpl. reflexivity. + ++ run_symbolic. + constructor. + run_symbolic. +Defined. + +Instance run_sgt + {WIRE H : Set} `{Link WIRE} `{Link H} + {WIRE_types : InterpreterTypes.Types.t} `{InterpreterTypes.Types.AreLinks WIRE_types} + (run_InterpreterTypes_for_WIRE : InterpreterTypes.Run WIRE WIRE_types) + (interpreter : Ref.t Pointer.Kind.MutRef (Interpreter.t WIRE WIRE_types)) + (_host : Ref.t Pointer.Kind.MutRef H) : + Run.Trait + instructions.bitwise.sgt [] [ Φ WIRE; Φ H ] [ φ interpreter; φ _host ] + unit. +Proof. + constructor. + cbn. + eapply Run.Rewrite. { + repeat erewrite IsTraitAssociatedType_eq by apply run_InterpreterTypes_for_WIRE. + reflexivity. + } + destruct run_InterpreterTypes_for_WIRE. + destruct run_StackTrait_for_Stack. + run_symbolic. + + destruct run_LoopControl_for_Control. + run_symbolic. + + eapply Run.CallPrimitiveGetTraitMethod. + ++ specialize (cmp.Impl_core_cmp_PartialEq_core_cmp_Ordering_for_core_cmp_Ordering.Implements). + intros. + unfold cmp.Impl_core_cmp_PartialEq_core_cmp_Ordering_for_core_cmp_Ordering.Self in H3. + eapply IsTraitMethod.Defined. + - eapply cmp.Impl_core_cmp_PartialEq_core_cmp_Ordering_for_core_cmp_Ordering.Implements. + - simpl. reflexivity. + ++ run_symbolic. + constructor. + run_symbolic. +Defined. + +Instance run_bitwise_eq + {WIRE H : Set} `{Link WIRE} `{Link H} + {WIRE_types : InterpreterTypes.Types.t} `{InterpreterTypes.Types.AreLinks WIRE_types} + (run_InterpreterTypes_for_WIRE : InterpreterTypes.Run WIRE WIRE_types) + (interpreter : Ref.t Pointer.Kind.MutRef (Interpreter.t WIRE WIRE_types)) + (_host : Ref.t Pointer.Kind.MutRef H) : + Run.Trait + instructions.bitwise.eq [] [ Φ WIRE; Φ H ] [ φ interpreter; φ _host ] + unit. +Proof. + constructor. + cbn. + eapply Run.Rewrite. { + repeat erewrite IsTraitAssociatedType_eq by apply run_InterpreterTypes_for_WIRE. + reflexivity. + } + destruct run_InterpreterTypes_for_WIRE. + destruct run_StackTrait_for_Stack. + + destruct run_LoopControl_for_Control. + run_symbolic. + eapply Run.CallPrimitiveGetTraitMethod. + ++ specialize (dependencies.ruint.Impl_PartialEq_for_Uint.Implements + (Value.Integer IntegerKind.Usize 256) + (Value.Integer IntegerKind.Usize 4)). + intros. + unfold dependencies.ruint.Impl_PartialEq_for_Uint.Self in H3. + eapply IsTraitMethod.Defined. + - eapply dependencies.ruint.Impl_PartialEq_for_Uint.Implements. + - simpl. reflexivity. + ++ run_symbolic. + constructor. + run_symbolic. + exact (dependencies.ruint.Impl_PartialEq_for_Uint.run_eq + {| Integer.value := 256 |} + {| Integer.value := 4 |} + (Ref.cast_to Pointer.Kind.Ref (Ref.immediate Pointer.Kind.Raw value)) + (Ref.cast_to Pointer.Kind.Ref value0)). +Defined. + +Instance run_bitwise_is_zero + {WIRE H : Set} `{Link WIRE} `{Link H} + {WIRE_types : InterpreterTypes.Types.t} `{InterpreterTypes.Types.AreLinks WIRE_types} + (run_InterpreterTypes_for_WIRE : InterpreterTypes.Run WIRE WIRE_types) + (interpreter : Ref.t Pointer.Kind.MutRef (Interpreter.t WIRE WIRE_types)) + (_host : Ref.t Pointer.Kind.MutRef H) : + Run.Trait + instructions.bitwise.iszero [] [ Φ WIRE; Φ H ] [ φ interpreter; φ _host ] + unit. +Proof. + constructor. + cbn. + eapply Run.Rewrite. { + repeat erewrite IsTraitAssociatedType_eq by apply run_InterpreterTypes_for_WIRE. + reflexivity. + } + destruct run_InterpreterTypes_for_WIRE. + destruct run_StackTrait_for_Stack. + destruct run_LoopControl_for_Control. + run_symbolic. +Qed. + +Instance run_bitwise_bitand + {WIRE H : Set} `{Link WIRE} `{Link H} + {WIRE_types : InterpreterTypes.Types.t} `{InterpreterTypes.Types.AreLinks WIRE_types} + (run_InterpreterTypes_for_WIRE : InterpreterTypes.Run WIRE WIRE_types) + (interpreter : Ref.t Pointer.Kind.MutRef (Interpreter.t WIRE WIRE_types)) + (_host : Ref.t Pointer.Kind.MutRef H) : + Run.Trait + instructions.bitwise.bitand [] [ Φ WIRE; Φ H ] [ φ interpreter; φ _host ] + unit. +Proof. + constructor. + cbn. + eapply Run.Rewrite. { + repeat erewrite IsTraitAssociatedType_eq by apply run_InterpreterTypes_for_WIRE. + reflexivity. + } + destruct run_InterpreterTypes_for_WIRE. + destruct run_StackTrait_for_Stack. + destruct run_LoopControl_for_Control. + run_symbolic. + + eapply Run.CallPrimitiveGetTraitMethod. + ++ eapply IsTraitMethod.Defined. + - specialize (dependencies.ruint.Impl_BitAnd_for_Uint.Implements + (Value.Integer IntegerKind.Usize 256) + (Value.Integer IntegerKind.Usize 4)). + intros. + unfold dependencies.ruint.Impl_BitAnd_for_Uint.Self in H3. + eapply dependencies.ruint.Impl_BitAnd_for_Uint.Implements. + - simpl. reflexivity. + ++ run_symbolic. + constructor. + run_symbolic. + destruct (dependencies.ruint.Impl_BitAnd_for_Uint.run_bitand + {| Integer.value := 256 |} + {| Integer.value := 4 |} + value + value1). + exact run_f0. +Defined. + +Instance run_bitwise_bitor + {WIRE H : Set} `{Link WIRE} `{Link H} + {WIRE_types : InterpreterTypes.Types.t} `{InterpreterTypes.Types.AreLinks WIRE_types} + (run_InterpreterTypes_for_WIRE : InterpreterTypes.Run WIRE WIRE_types) + (interpreter : Ref.t Pointer.Kind.MutRef (Interpreter.t WIRE WIRE_types)) + (_host : Ref.t Pointer.Kind.MutRef H) : + Run.Trait + instructions.bitwise.bitor [] [ Φ WIRE; Φ H ] [ φ interpreter; φ _host ] + unit. +Proof. + constructor. + cbn. + eapply Run.Rewrite. { + repeat erewrite IsTraitAssociatedType_eq by apply run_InterpreterTypes_for_WIRE. + reflexivity. + } + destruct run_InterpreterTypes_for_WIRE. + destruct run_StackTrait_for_Stack. + destruct run_LoopControl_for_Control. + run_symbolic. + + eapply Run.CallPrimitiveGetTraitMethod. + ++ eapply IsTraitMethod.Defined. + - specialize (dependencies.ruint.Impl_BitOr_for_Uint.Implements + (Value.Integer IntegerKind.Usize 256) + (Value.Integer IntegerKind.Usize 4)). + intros. + unfold dependencies.ruint.Impl_BitOr_for_Uint.Self in H3. + eapply dependencies.ruint.Impl_BitOr_for_Uint.Implements. + - simpl. reflexivity. + ++ run_symbolic. + constructor. + run_symbolic. + destruct (dependencies.ruint.Impl_BitOr_for_Uint.run_bitor + {| Integer.value := 256 |} + {| Integer.value := 4 |} + value + value1). + exact run_f0. +Defined. + +Instance run_bitwise_bitxor + {WIRE H : Set} `{Link WIRE} `{Link H} + {WIRE_types : InterpreterTypes.Types.t} `{InterpreterTypes.Types.AreLinks WIRE_types} + (run_InterpreterTypes_for_WIRE : InterpreterTypes.Run WIRE WIRE_types) + (interpreter : Ref.t Pointer.Kind.MutRef (Interpreter.t WIRE WIRE_types)) + (_host : Ref.t Pointer.Kind.MutRef H) : + Run.Trait + instructions.bitwise.bitxor [] [ Φ WIRE; Φ H ] [ φ interpreter; φ _host ] + unit. +Proof. + constructor. + cbn. + eapply Run.Rewrite. { + repeat erewrite IsTraitAssociatedType_eq by apply run_InterpreterTypes_for_WIRE. + reflexivity. + } + destruct run_InterpreterTypes_for_WIRE. + destruct run_StackTrait_for_Stack. + destruct run_LoopControl_for_Control. + run_symbolic. + + eapply Run.CallPrimitiveGetTraitMethod. + ++ eapply IsTraitMethod.Defined. + - specialize (dependencies.ruint.Impl_BitXor_for_Uint.Implements + (Value.Integer IntegerKind.Usize 256) + (Value.Integer IntegerKind.Usize 4)). + intros. + unfold dependencies.ruint.Impl_BitXor_for_Uint.Self in H3. + eapply dependencies.ruint.Impl_BitXor_for_Uint.Implements. + - simpl. reflexivity. + ++ run_symbolic. + constructor. + run_symbolic. + destruct (dependencies.ruint.Impl_BitXor_for_Uint.run_bitxor + {| Integer.value := 256 |} + {| Integer.value := 4 |} + value + value1). + exact run_f0. +Defined. + +Instance run_bitwise_not + {WIRE H : Set} `{Link WIRE} `{Link H} + {WIRE_types : InterpreterTypes.Types.t} `{InterpreterTypes.Types.AreLinks WIRE_types} + (run_InterpreterTypes_for_WIRE : InterpreterTypes.Run WIRE WIRE_types) + (interpreter : Ref.t Pointer.Kind.MutRef (Interpreter.t WIRE WIRE_types)) + (_host : Ref.t Pointer.Kind.MutRef H) : + Run.Trait + instructions.bitwise.not [] [ Φ WIRE; Φ H ] [ φ interpreter; φ _host ] + unit. +Proof. + constructor. + cbn. + eapply Run.Rewrite. { + repeat erewrite IsTraitAssociatedType_eq by apply run_InterpreterTypes_for_WIRE. + reflexivity. + } + destruct run_InterpreterTypes_for_WIRE. + destruct run_StackTrait_for_Stack. + destruct run_LoopControl_for_Control. + run_symbolic. + + eapply Run.CallPrimitiveGetTraitMethod. + ++ eapply IsTraitMethod.Defined. + - specialize (dependencies.ruint.Impl_BitNot_for_Uint.Implements + (Value.Integer IntegerKind.Usize 256) + (Value.Integer IntegerKind.Usize 4)). + intros. + unfold dependencies.ruint.Impl_BitNot_for_Uint.Self in H3. + eapply dependencies.ruint.Impl_BitNot_for_Uint.Implements. + - simpl. reflexivity. + ++ run_symbolic. + constructor. + run_symbolic. + destruct (dependencies.ruint.Impl_BitNot_for_Uint.run_bitnot + {| Integer.value := 256 |} + {| Integer.value := 4 |} + value0). + exact run_f0. +Defined. + +Instance run_bitwise_sar + {WIRE H : Set} `{Link WIRE} `{Link H} + {WIRE_types : InterpreterTypes.Types.t} `{InterpreterTypes.Types.AreLinks WIRE_types} + (run_InterpreterTypes_for_WIRE : InterpreterTypes.Run WIRE WIRE_types) + (interpreter : Ref.t Pointer.Kind.MutRef (Interpreter.t WIRE WIRE_types)) + (_host : Ref.t Pointer.Kind.MutRef H) : + Run.Trait + instructions.bitwise.sar [] [ Φ WIRE; Φ H ] [ φ interpreter; φ _host ] + unit. +Proof. + constructor. + cbn. + eapply Run.Rewrite. { + repeat erewrite IsTraitAssociatedType_eq by apply run_InterpreterTypes_for_WIRE. + reflexivity. + } + destruct run_InterpreterTypes_for_WIRE. + destruct run_StackTrait_for_Stack. + destruct run_LoopControl_for_Control. + destruct run_RuntimeFlag_for_RuntimeFlag. + run_symbolic. + - eapply Run.CallPrimitiveGetTraitMethod. + + eapply IsTraitMethod.Defined. + ++ specialize convert.num.ptr_try_from_impls.Impl_core_convert_TryFrom_u64_for_usize.Implements. + intros. + unfold convert.num.ptr_try_from_impls.Impl_core_convert_TryFrom_u64_for_usize.Self in H3. + eapply H3. + ++ simpl. reflexivity. + + run_symbolic. + ++ constructor. + +++ eapply Implements_AsLimbs. + ++ admit. + ++ constructor. + run_symbolic. + simpl. + cbn. + instantiate (1 := result.Result.Ok (cast_integer IntegerKind.Usize value1)). + reflexivity. + ++ admit. + - admit. + - admit. + - admit. + - admit. +reflexivity. + + +Admitted. + +Instance run_bitwise_shl + {WIRE H : Set} `{Link WIRE} `{Link H} + {WIRE_types : InterpreterTypes.Types.t} `{InterpreterTypes.Types.AreLinks WIRE_types} + (run_InterpreterTypes_for_WIRE : InterpreterTypes.Run WIRE WIRE_types) + (interpreter : Ref.t Pointer.Kind.MutRef (Interpreter.t WIRE WIRE_types)) + (_host : Ref.t Pointer.Kind.MutRef H) : + Run.Trait + instructions.bitwise.shl [] [ Φ WIRE; Φ H ] [ φ interpreter; φ _host ] + unit. +Proof. + constructor. + cbn. + eapply Run.Rewrite. { + repeat erewrite IsTraitAssociatedType_eq by apply run_InterpreterTypes_for_WIRE. + reflexivity. + } + destruct run_InterpreterTypes_for_WIRE. + destruct run_StackTrait_for_Stack. + destruct run_LoopControl_for_Control. + destruct run_RuntimeFlag_for_RuntimeFlag. + run_symbolic. + - constructor. + run_symbolic. + admit. + - admit. + - eapply Run.CallPrimitiveGetTraitMethod. + + eapply IsTraitMethod.Defined. + ++ apply dependencies.ruint.Impl_Shl_for_Uint.Implements. + ++ simpl. reflexivity. + + run_symbolic. + constructor. + destruct (dependencies.ruint.Impl_Shl_for_Uint.run_shl + {| Integer.value := 256 |} + {| Integer.value := 4 |} + value2 + value3). + exact run_f0. + - admit. +Admitted. + +Instance run_bitwise_shr + {WIRE H : Set} `{Link WIRE} `{Link H} + {WIRE_types : InterpreterTypes.Types.t} `{InterpreterTypes.Types.AreLinks WIRE_types} + (run_InterpreterTypes_for_WIRE : InterpreterTypes.Run WIRE WIRE_types) + (interpreter : Ref.t Pointer.Kind.MutRef (Interpreter.t WIRE WIRE_types)) + (_host : Ref.t Pointer.Kind.MutRef H) : + Run.Trait + instructions.bitwise.shr [] [ Φ WIRE; Φ H ] [ φ interpreter; φ _host ] + unit. +Proof. + constructor. + cbn. + eapply Run.Rewrite. { + repeat erewrite IsTraitAssociatedType_eq by apply run_InterpreterTypes_for_WIRE. + reflexivity. + } + destruct run_InterpreterTypes_for_WIRE. + destruct run_StackTrait_for_Stack. + destruct run_LoopControl_for_Control. + destruct run_RuntimeFlag_for_RuntimeFlag. + run_symbolic. + Print hardfork.Impl_revm_specification_hardfork_SpecId. + - constructor. + run_symbolic. + rewrite (hardfork.SpecId.cast_integer_eq IntegerKind.U8). + run_symbolic. + + eapply Run.Rewrite. { + rewrite hardfork.SpecId.cast_integer_eq. } + specialize (hardfork.SpecId.get_discriminant output). + intro. + set (discr_output := Integer.Build_t IntegerKind.U8 (SpecId.get_discriminant output mod 256)). + replace (SpecId.get_discriminant output mod 256) with discr_output.(Integer.value). + + admit. + + + simpl. + reflexivity. + - eapply Run.CallPrimitiveGetTraitMethod. + + eapply IsTraitMethod.Defined. + ++ specialize convert.num.ptr_try_from_impls.Impl_core_convert_TryFrom_u64_for_usize.Implements. + intros. + unfold convert.num.ptr_try_from_impls.Impl_core_convert_TryFrom_u64_for_usize.Self in H3. + eapply H3. + ++ simpl. reflexivity. + + run_symbolic. + ++ constructor. + apply dependencies.ruint.Impl_AsLimbs_Uint.Implements_AsLimbs. + ++ eapply Run.CallPrimitiveStateAlloc. + intro. + run_symbolic. + eapply Run.CallPrimitiveAreEqualBool. + +++ admit. + +++ simpl. reflexivity. + +++ intro. + admit. + ++ admit. + ++ admit. + ++ admit. + ++ admit. + ++ admit. + ++ admit. + ++ admit. + ++ admit. + ++ admit. +- eapply Run.CallPrimitiveGetTraitMethod. + + eapply IsTraitMethod.Defined. + ++ apply dependencies.ruint.Impl_Shr_for_Uint.Implements. + ++ simpl. reflexivity. + + run_symbolic. + constructor. + destruct (dependencies.ruint.Impl_Shr_for_Uint.run_shr + {| Integer.value := 256 |} + {| Integer.value := 4 |} + value2 + value3). + exact run_f0. + - admit. +Admitted. \ No newline at end of file diff --git a/CoqOfRust/revm/revm_interpreter/instructions/links/i256.v b/CoqOfRust/revm/revm_interpreter/instructions/links/i256.v index 754b38126..1113a5d2c 100644 --- a/CoqOfRust/revm/revm_interpreter/instructions/links/i256.v +++ b/CoqOfRust/revm/revm_interpreter/instructions/links/i256.v @@ -1 +1,71 @@ -(* Initial stub *) \ No newline at end of file +Require Import CoqOfRust.CoqOfRust. +Require Import CoqOfRust.links.M. +Require Import core.links.intrinsics. +Require Import core.cmp. +Require Import revm.links.dependencies. +Require Import revm.revm_context_interface.links.host. +Require Import revm.revm_interpreter.links.gas. +Require Import revm.revm_interpreter.instructions.bitwise. +Require Import revm.revm_interpreter.instructions.i256. + +Import Impl_Gas. + +Module Sign. + Inductive t : Set := + | Negative + | Zero + | Positive. + + Global Instance IsLink : Link t := { + Φ := Ty.path "revm_interpreter::instructions::i256::Sign"; + φ s := + match s with + | Negative => Value.StructTuple "revm_interpreter::instructions::i256::Sign::Negative" [] + | Zero => Value.StructTuple "revm_interpreter::instructions::i256::Sign::Zero" [] + | Positive => Value.StructTuple "revm_interpreter::instructions::i256::Sign::Positive" [] + end + }. + + Definition of_ty : OfTy.t (Ty.path "revm_interpreter::instructions::i256::Sign"). + Proof. + eapply OfTy.Make with (A := t); reflexivity. + Defined. + Smpl Add simple apply of_ty : of_ty. + + Lemma of_value_with_Negative : + Value.StructTuple "revm_interpreter::instructions::i256::Sign::Negative" [] = + φ Negative. + Proof. + reflexivity. + Qed. + Smpl Add simple apply of_value_with_Negative : of_value. + + Lemma of_value_with_Zero : + Value.StructTuple "revm_interpreter::instructions::i256::Sign::Zero" [] = + φ Zero. + Proof. + reflexivity. + Qed. + Smpl Add simple apply of_value_with_Zero : of_value. + + Lemma of_value_with_Positive : + Value.StructTuple "revm_interpreter::instructions::i256::Sign::Positive" [] = + φ Positive. + Proof. + reflexivity. + Qed. + Smpl Add simple apply of_value_with_Positive : of_value. +End Sign. + +Instance run_i256_sign (first : Ref.t Pointer.Kind.MutRef U256.t) : + Run.Trait instructions.i256.i256_sign [] [] + [Ref.IsLink.(φ) (Ref.cast_to Pointer.Kind.Ref first)] + Sign.t. +Proof. +Admitted. + +(* pub fn i256_cmp(first: &U256, second: &U256) -> Ordering *) +Instance run_i256_cmp (first second : Ref.t Pointer.Kind.Ref dependencies.U256.t) : + Run.Trait instructions.i256.i256_cmp [] [] [ φ first; φ second ] cmpOrdering.Ordering.t. +Proof. +Admitted. diff --git a/CoqOfRust/revm/revm_interpreter/links/interpreter_types.v b/CoqOfRust/revm/revm_interpreter/links/interpreter_types.v index 5285add5b..1de8877d8 100644 --- a/CoqOfRust/revm/revm_interpreter/links/interpreter_types.v +++ b/CoqOfRust/revm/revm_interpreter/links/interpreter_types.v @@ -12,6 +12,9 @@ Require Import revm.revm_interpreter.interpreter_types. Require Import revm.revm_specification.links.hardfork. Require Import revm.links.dependencies. +Import alloy_primitives.bits.links.address. +Import alloy_primitives.links.bytes_. + (* pub trait StackTrait { fn len(&self) -> usize; @@ -768,4 +771,4 @@ Module InterpreterTypes. "RuntimeFlag" (Φ types.(Types.RuntimeFlag)); run_RuntimeFlag_for_RuntimeFlag : RuntimeFlag.Run types.(Types.RuntimeFlag); }. -End InterpreterTypes. +End InterpreterTypes. \ No newline at end of file