Merge pull request #685 from formal-land/andreadlm@update-links-for-revm-eof-body

Update links for revm eof body

Author: clarus

CoqOfRust/alloc/vec/links/mod.v

@@ -4,6 +4,7 @@ Require Import links.M.
 Require core.links.clone.
 Require core.links.default.
 Require core.ops.links.deref.
+Require core.ops.links.index.
 
 Import Run.
 
@@ -78,9 +79,7 @@ Module Impl_alloc_vec_Vec_T_A.
   Definition Self := Vec.t.
 
   (*
-    pub const fn new() -> Self {
-      Vec { buf: RawVec::new(), len: 0 }
-    }
+    pub const fn new() -> Self 
   *)
   Instance run_new {T A : Set} `{Link T} `{Link A} : 
     Run.Trait (vec.Impl_alloc_vec_Vec_T_alloc_alloc_Global.new (Φ T)) [] [] [] (Self T A).
@@ -102,3 +101,20 @@ Module Impl_alloc_vec_Vec_T_A.
     Run.Trait (vec.Impl_alloc_vec_Vec_T_A.len (Φ T) (Φ A)) [] [] [φ self] Usize.t.
   Admitted.
 End Impl_alloc_vec_Vec_T_A.
+
+Module Impl_core_ops_index_Index_where_core_slice_index_SliceIndex_I_slice_T_where_core_alloc_Allocator_A_I_for_alloc_vec_Vec_T_A.
+  Definition Self := Vec.t.
+  
+  (*
+    fn index(&self, index: I) -> &Self::Output
+  *)
+  Instance run_index {T I A Output : Set} `{Link T} `{Link I} `{Link A} `{Link Output} 
+      {self : Ref.t Pointer.Kind.Ref (Self T A)}
+      {index : I} : 
+    Run.Trait (vec.Impl_core_ops_index_Index_where_core_slice_index_SliceIndex_I_slice_T_where_core_alloc_Allocator_A_I_for_alloc_vec_Vec_T_A.index (Φ T) (Φ I) (Φ A)) [] [Φ I] [φ self; φ index] (Ref.t Pointer.Kind.Ref Output).
+  Admitted.
+
+  Definition run {T I A Output : Set} `{Link T} `{Link I} `{Link A} `{Link Output} : 
+    index.Index.Run (Self T A) I Output.
+  Admitted.
+End Impl_core_ops_index_Index_where_core_slice_index_SliceIndex_I_slice_T_where_core_alloc_Allocator_A_I_for_alloc_vec_Vec_T_A.

CoqOfRust/core/links/cmp.v

@@ -2,6 +2,7 @@ Require Import CoqOfRust.CoqOfRust.
 Require Import links.M.
 Require Import core.cmp.
 Require Import core.intrinsics.
+Require Import core.links.option.
 Require core.ops.links.function.
 Require Import core.links.intrinsics.
 Require Export core.links.cmpOrdering.
@@ -182,4 +183,63 @@ Module Impl_Ord_for_u64.
       exact run_clamp.
     }
   Defined.
-End Impl_Ord_for_u64.
+End Impl_Ord_for_u64.
+
+Module PartialOrd.
+  (*
+    pub trait PartialOrd<Rhs: ?Sized = Self>: PartialEq<Rhs> {
+      fn partial_cmp(&self, other: &Rhs) -> Option<Ordering>;
+      fn lt(&self, other: &Rhs) -> bool;
+      fn le(&self, other: &Rhs) -> bool;
+      fn gt(&self, other: &Rhs) -> bool;
+      fn ge(&self, other: &Rhs) -> bool;
+    }
+  *)
+  Definition Run_partial_cmp (Self Rhs : Set) `{Link Self} `{Link Rhs} : Set :=
+    {partial_cmp  @
+      IsTraitMethod.t "core::cmp::PartialOrd" [] [] (Φ Self) "partial_cmp" partial_cmp  *
+      forall (self : Ref.t Pointer.Kind.Ref Self) (other: Ref.t Pointer.Kind.Ref Rhs),
+        {{ partial_cmp  [] [] [φ self; φ other] 🔽 option Ordering.t }}
+    }.
+
+  Definition Run_lt (Self Rhs : Set) `{Link Self} `{Link Rhs} : Set :=
+    {lt  @
+      IsTraitMethod.t "core::cmp::PartialOrd" [] [] (Φ Self) "lt" lt  *
+      forall (self : Ref.t Pointer.Kind.Ref Self) (other: Ref.t Pointer.Kind.Ref Rhs),
+        {{ lt  [] [] [φ self; φ other] 🔽 bool }}
+    }.
+
+  Definition Run_le (Self Rhs : Set) `{Link Self} `{Link Rhs} : Set :=
+    {le  @
+      IsTraitMethod.t "core::cmp::PartialOrd" [] [] (Φ Self) "le" le  *
+      forall (self : Ref.t Pointer.Kind.Ref Self) (other: Ref.t Pointer.Kind.Ref Rhs),
+        {{ le  [] [] [φ self; φ other] 🔽 bool }}
+    }.
+
+  Definition Run_gt (Self Rhs : Set) `{Link Self} `{Link Rhs} : Set :=
+    {gt  @
+      IsTraitMethod.t "core::cmp::PartialOrd" [] [] (Φ Self) "gt" gt  *
+      forall (self : Ref.t Pointer.Kind.Ref Self) (other: Ref.t Pointer.Kind.Ref Rhs),
+        {{ gt  [] [] [φ self; φ other] 🔽 bool }}
+    }.
+
+  Definition Run_ge (Self Rhs : Set) `{Link Self} `{Link Rhs} : Set :=
+    {ge  @
+      IsTraitMethod.t "core::cmp::PartialOrd" [] [] (Φ Self) "ge" ge  *
+      forall (self : Ref.t Pointer.Kind.Ref Self) (other: Ref.t Pointer.Kind.Ref Rhs),
+        {{ ge  [] [] [φ self; φ other] 🔽 bool }}
+    }.
+
+  Record Run (Self Rhs : Set) `{Link Self} `{Link Rhs} : Set := {
+    partial_cmp : Run_partial_cmp Self Rhs;
+    lt : Run_lt Self Rhs;
+    le : Run_le Self Rhs;
+    gt : Run_gt Self Rhs;
+    ge : Run_ge Self Rhs;
+  }.
+
+  (* Instance run_partial_cmp {Self Rhs : Set} `{Link Self} `{Link Rhs}
+      (self : Ref.t Pointer.Kind.Ref Self) (other : Ref.t Pointer.Kind.Ref Rhs) :
+    Run.Trait cmp.Impl_core_cmp_PartialOrd_for_core_cmp_Ordering.partial_cmp [] [] [φ self; φ other] (option Ordering.t).
+  Admitted. *)
+End PartialOrd.

CoqOfRust/core/links/result.v

@@ -2,12 +2,17 @@ Require Import CoqOfRust.CoqOfRust.
 Require Import links.M.
 
 Module Result.
-  Global Instance IsLink (A B : Set) (_ : Link A) (_ : Link B) : Link (A + B) := {
-    Φ := Ty.apply (Ty.path "core::result::Result") [] [Φ A; Φ B];
+  Inductive t {T E : Set} : Set :=
+  | Ok : T -> t
+  | Err : E -> t.
+  Arguments t : clear implicits.
+
+  Global Instance IsLink (T E : Set) `{Link T} `{Link E} : Link (t T E) := {
+    Φ := Ty.apply (Ty.path "core::result::Result") [] [Φ T; Φ E];
     φ x :=
       match x with
-      | inl x => Value.StructTuple "core::result::Result::Ok" [φ x]
-      | inr e => Value.StructTuple "core::result::Result::Err" [φ e]
+      | Ok x => Value.StructTuple "core::result::Result::Ok" [φ x]
+      | Err x => Value.StructTuple "core::result::Result::Err" [φ x]
       end;
   }.
 End Result.

CoqOfRust/core/ops/links/index.v

@@ -0,0 +1,33 @@
+Require Import CoqOfRust.CoqOfRust.
+Require Import links.M.
+
+(*
+  pub trait Index<Idx: ?Sized> {
+    type Output: ?Sized;
+
+    fn index(&self, index: Idx) -> &Self::Output;
+  }
+*)
+Module Index.
+  Definition run_index 
+      (Self : Set) `{Link Self} 
+      (Idx : Set) `{Link Idx} 
+      (Output : Set) `{Link Output} : Set :=
+    { index' @ 
+      IsTraitMethod.t "core::ops::index::Index" [] [Φ Idx] (Φ Self) "index" index' *
+      forall (self : Ref.t Pointer.Kind.Ref Self) (index : Idx),
+        {{ index' [] [] [φ self; φ index] 🔽 Ref.t Pointer.Kind.Ref Output }}
+    }.
+
+  Record Run
+      (Self : Set) `{Link Self}
+      (Idx : Set) `{Link Idx}
+      (Output : Set) `{Link Output} : 
+    Set := {
+      Output_IsAssociated :
+      IsTraitAssociatedType
+        "core::slice::index::SliceIndex" [] [Φ Idx] (Φ Self)
+        "Output" (Φ Output);
+      index : run_index Self Idx Output;
+  }.
+End Index.

CoqOfRust/core/ops/links/range.v

@@ -1,4 +1,5 @@
 Require Import CoqOfRust.CoqOfRust.
+Require Import core.links.cmp.
 Require Import links.M.
 
 (*
@@ -49,3 +50,64 @@ Module Bound.
       end;
   }.
 End Bound.
+
+(*
+  pub trait RangeBounds<T: ?Sized> {
+    fn start_bound(&self) -> Bound<&T>;
+    fn end_bound(&self) -> Bound<&T>;
+    fn contains<U>(&self, item: &U) -> bool
+    where
+        T: PartialOrd<U>,
+        U: ?Sized + PartialOrd<T>
+    fn is_empty(&self) -> bool
+    where
+        T: PartialOrd;
+  }
+*)
+Module RangeBounds.
+  Definition Run_start_bound (Self : Set) `{Link Self} 
+      (T : Set) `{Link T} : Set :=
+    {start_bound @
+      IsTraitMethod.t "core::ops::RangeBounds" [] [] (Φ Self) "start_bound" start_bound *
+      forall (self : Ref.t Pointer.Kind.Ref Self),
+        {{ start_bound [] [] [φ self] 🔽 Bound.t (Ref.t Pointer.Kind.Ref T) }}
+    }.
+
+  Definition Run_end_bound (Self : Set) `{Link Self} 
+      (T : Set) `{Link T} : Set :=
+    {end_bound @
+      IsTraitMethod.t "core::ops::RangeBounds" [] [] (Φ Self) "end_bound" end_bound *
+      forall (self : Ref.t Pointer.Kind.Ref Self),
+        {{ end_bound [] [] [φ self] 🔽 Bound.t (Ref.t Pointer.Kind.Ref T) }}
+    }.
+
+  Definition Run_contains (Self : Set) `{Link Self} 
+      (T : Set) `{Link T}  : Set :=
+    {contains @
+      IsTraitMethod.t "core::ops::RangeBounds" [] [] (Φ Self) "contains" contains *
+      forall 
+          (self : Ref.t Pointer.Kind.Ref Self)
+          (U : Set) `(Link U)
+          (item : Ref.t Pointer.Kind.Ref U)
+          (run_Ord_for_T : PartialOrd.Run T T)
+          (run_Ord_for_U : PartialOrd.Run U U),
+        {{ contains [] [] [φ self; φ item] 🔽 bool }}
+    }.
+
+  Definition Run_is_empty (Self : Set) `{Link Self} 
+      (T : Set) `{Link T} : Set :=
+    {is_empty @ 
+      IsTraitMethod.t "core::ops::RangeBounds" [] [] (Φ Self) "is_empty" is_empty *
+      forall (self : Ref.t Pointer.Kind.Ref Self)
+          (run_Ord_for_T : PartialOrd.Run T T),
+        {{ is_empty [] [] [φ self] 🔽 bool }}
+    }.
+
+  Record Run (Self : Set) `{Link Self} 
+      {T : Set} `{Link T} : Set := {
+    start_bound : Run_start_bound Self T;
+    end_bound : Run_end_bound Self T;
+    contains : Run_contains Self T;
+    is_empty : Run_is_empty Self T;
+  }.
+End RangeBounds.

CoqOfRust/revm/links/dependencies.v

@@ -2,6 +2,7 @@ Require Import CoqOfRust.CoqOfRust.
 Require Import CoqOfRust.links.M.
 Require Import core.convert.links.mod.
 Require Import core.links.array.
+Require Import core.ops.links.range.
 Require core.links.clone.
 Require core.links.default.
 Require Import ruint.links.lib.
@@ -119,6 +120,20 @@ Module alloy_primitives.
 
         Global Instance run_new : Run.Trait new [] [] [] Bytes.t.
         Admitted.
+
+        (* pub fn slice(&self, range: impl RangeBounds<usize>) -> Self *)
+        Parameter slice : PolymorphicFunction.t.
+
+        Global Instance AssociatedFunction_slice :
+          M.IsAssociatedFunction.Trait (Φ Self) "slice" slice.
+        Admitted.
+
+        Global Instance run_slice {A : Set} `{Link A} 
+          (self : Ref.t Pointer.Kind.Ref Self) 
+          (range : A) 
+          (run_RangeBounds_for_A : RangeBounds.Run A) :
+          Run.Trait slice [] [] [φ self; φ range] Self.
+        Admitted.
       End Impl_Bytes.
 
       Module Impl_Clone_for_Bytes.

CoqOfRust/revm/revm_bytecode/eof/links/body.v

@@ -4,6 +4,7 @@ Require Import alloc.links.alloc.
 Require Import alloc.vec.links.mod.
 Require core.links.clone.
 Require core.links.default.
+Require Import core.links.result.
 Require Import core.links.option.
 Require Import revm.links.dependencies.
 Require Export revm.revm_bytecode.eof.links.body_EofBody.
@@ -13,8 +14,6 @@ Require Import revm.revm_bytecode.links.eof.
 Require Import revm_bytecode.eof.body.
 Require Import core.slice.links.mod.
 
-Import Run.
-
 Module EofBody.
   Record t : Set := {
     types_section: Vec.t revm_bytecode.eof.links.types_section.TypesSection.t Global.t;
@@ -233,6 +232,7 @@ Module Impl_EofBody.
   Import Impl_alloc_vec_Vec_T_A.
   Import Impl_EofHeader.
   Import Impl_Slice.
+  Import Impl_core_ops_index_Index_where_core_slice_index_SliceIndex_I_slice_T_where_core_alloc_Allocator_A_I_for_alloc_vec_Vec_T_A.
 
   Definition Self : Set := EofBody.t.
 
@@ -243,8 +243,12 @@ Module Impl_EofBody.
     Run.Trait body.eof.body.Impl_revm_bytecode_eof_body_EofBody.code [] [] [φ self; φ index] (option alloy_primitives.links.bytes_.Bytes.t).
   Proof.
     constructor.
-    run_symbolic. 
+    destruct (vec.links.mod.Impl_core_ops_index_Index_where_core_slice_index_SliceIndex_I_slice_T_where_core_alloc_Allocator_A_I_for_alloc_vec_Vec_T_A.run (T := Usize.t) (I := Usize.t) (A := Global.t)) as [index' [H_index' run_index']].
+    destruct (vec.links.mod.Impl_Deref_for_Vec.run (T := Usize.t) (A := Global.t)).
+    destruct deref.
+    run_symbolic.
   Admitted.
+
 
   (*
     pub fn encode(&self, buffer: &mut Vec<u8>)
@@ -281,4 +285,10 @@ Module Impl_EofBody.
   (*
     pub fn decode(input: &Bytes, header: &EofHeader) -> Result<Self, EofDecodeError>
   *)
+  Instance run_decode (input : Ref.t Pointer.Kind.Ref alloy_primitives.links.bytes_.Bytes.t) (header : Ref.t Pointer.Kind.Ref EofHeader.t) :
+    Run.Trait body.eof.body.Impl_revm_bytecode_eof_body_EofBody.decode [] [] [φ input; φ header] (Result.t EofBody.t EofDecodeError.t).
+  Proof.  
+    constructor.
+    run_symbolic.
+  Admitted.
 End Impl_EofBody.

CoqOfRust/revm/revm_bytecode/eof/links/header.v

@@ -34,9 +34,15 @@ Module EofHeader.
 End EofHeader.
 
 Module Impl_EofHeader.
-
   Definition Self : Set := EofHeader.t.
 
+  (*
+    pub fn size(&self) -> usize
+  *)
+  Instance run_size (self : Ref.t Pointer.Kind.Ref Self) : 
+    Run.Trait header.eof.header.Impl_revm_bytecode_eof_header_EofHeader.size [] [] [φ self] Usize.t.
+  Admitted.
+
   (*
     pub fn encode(&self, buffer: &mut Vec<u8>)
   *)

CoqOfRust/revm/revm_bytecode/links/eof.v

@@ -22,3 +22,54 @@ Module Eof.
       ]
   }.
 End Eof.
+
+Module EofDecodeError.
+  Inductive t : Set :=
+  | MissingInput : t
+  | MissingBodyWithoutData : t
+  | DanglingData : t
+  | InvalidCodeInfo : t
+  | InvalidCodeInfoSize : t
+  | InvalidEOFMagicNumber : t
+  | InvalidEOFVersion : t
+  | InvalidTypesKind : t
+  | InvalidCodeKind : t
+  | InvalidTerminalByte : t
+  | InvalidDataKind : t
+  | InvalidKindAfterCode : t
+  | MismatchCodeAndInfoSize : t
+  | NonSizes : t
+  | ShortInputForSizes : t
+  | ZeroSize : t
+  | TooManyCodeSections : t
+  | ZeroCodeSections : t
+  | TooManyContainerSections : t
+  | InvalidEOFSize : t.
+
+  Global Instance IsLink : Link t := {
+    Φ := Ty.apply (Ty.path "revm_bytecode::eof::EofDecodeError") [] [];
+    φ x := 
+      match x with
+      | MissingInput => Value.StructTuple "revm_bytecode::eof::EofDecodeError::MissingInput" []
+      | MissingBodyWithoutData => Value.StructTuple "revm_bytecode::eof::EofDecodeError::MissingBodyWithoutData" []
+      | DanglingData => Value.StructTuple "revm_bytecode::eof::EofDecodeError::DanglingData" []
+      | InvalidCodeInfo => Value.StructTuple "revm_bytecode::eof::EofDecodeError::InvalidCodeInfo" []
+      | InvalidCodeInfoSize => Value.StructTuple "revm_bytecode::eof::EofDecodeError::InvalidCodeInfoSize" []
+      | InvalidEOFMagicNumber => Value.StructTuple "revm_bytecode::eof::EofDecodeError::InvalidEOFMagicNumber" []
+      | InvalidEOFVersion => Value.StructTuple "revm_bytecode::eof::EofDecodeError::InvalidEOFVersion" []
+      | InvalidTypesKind => Value.StructTuple "revm_bytecode::eof::EofDecodeError::InvalidTypesKind" []
+      | InvalidCodeKind => Value.StructTuple "revm_bytecode::eof::EofDecodeError::InvalidCodeKind" []
+      | InvalidTerminalByte => Value.StructTuple "revm_bytecode::eof::EofDecodeError::InvalidTerminalByte" []
+      | InvalidDataKind => Value.StructTuple "revm_bytecode::eof::EofDecodeError::InvalidDataKind" []
+      | InvalidKindAfterCode => Value.StructTuple "revm_bytecode::eof::EofDecodeError::InvalidKindAfterCode" []
+      | MismatchCodeAndInfoSize => Value.StructTuple "revm_bytecode::eof::EofDecodeError::MismatchCodeAndInfoSize" []
+      | NonSizes => Value.StructTuple "revm_bytecode::eof::EofDecodeError::NonSizes" []
+      | ShortInputForSizes => Value.StructTuple "revm_bytecode::eof::EofDecodeError::ShortInputForSizes" []
+      | ZeroSize => Value.StructTuple "revm_bytecode::eof::EofDecodeError::ZeroSize" []
+      | TooManyCodeSections => Value.StructTuple "revm_bytecode::eof::EofDecodeError::TooManyCodeSections" []
+      | ZeroCodeSections => Value.StructTuple "revm_bytecode::eof::EofDecodeError::ZeroCodeSections" []
+      | TooManyContainerSections => Value.StructTuple "revm_bytecode::eof::EofDecodeError::TooManyContainerSections" []
+      | InvalidEOFSize => Value.StructTuple "revm_bytecode::eof::EofDecodeError::InvalidEOFSize" []
+      end;
+  }.
+End EofDecodeError.