feat: minor improvements to translate ink_contracts/multisig.rs

formal-land · Jan 2, 2024 · 99f21d0 · 99f21d0
1 parent d812943
commit 99f21d0
Show file tree

Hide file tree

Showing 40 changed files with 2,159 additions and 2,111 deletions.
diff --git a/CoqOfRust/CoqOfRust.v b/CoqOfRust/CoqOfRust.v
@@ -846,170 +846,6 @@ Module Impl_Slice.
   End Impl_Slice.
 End Impl_Slice.
 
-(* TODO: this is only a temporary implementation,
-         it needs to be rewritten when all std files will be fixed *)
-Module Impl_Iterator_for_Slice_Iter.
-  Section Impl_Iterator_for_Slice_Iter.
-  Context {A : Set}.
-
-  Definition Self := core.slice.iter.Iter.t A.
-
-  Definition Item := A.
-
-  Parameter next : mut_ref Self -> M (core.option.Option.t A).
-
-  Global Instance Method_next : Notations.Dot "next" := {
-    Notations.dot := next;
-  }.
-  End Impl_Iterator_for_Slice_Iter.
-End Impl_Iterator_for_Slice_Iter.
-
-(* TODO: this is only a temporary implementation,
-         it needs to be rewritten when all std files will be fixed *)
-(* this should be replaced with a generic instance of IntoIterator for Iterator *)
-Module Impl_IntoIterator_for_Slice_Iter.
-  Section Impl_IntoIterator_for_Slice_Iter.
-  Context {A : Set}.
-  Definition I := core.slice.iter.Iter.t A.
-
-  Definition Self := I.
-
-  Definition Item := A.
-  Definition IntoIter := I.
-
-  Parameter into_iter : Self -> M IntoIter.
-
-  Global Instance Method_into_iter :
-    Notations.Dot "into_iter" := {
-    Notations.dot := into_iter;
-  }.
-  End Impl_IntoIterator_for_Slice_Iter.
-End Impl_IntoIterator_for_Slice_Iter.
-
-(* TODO: this is only a temporary implementation,
-         it needs to be rewritten when all std files will be fixed *)
-Module Impl_Iterator_for_Slice_IterMut.
-  Section Impl_Iterator_for_Slice_IterMut.
-  Context {A : Set}.
-
-  Definition Self := core.slice.IterMut.t A.
-
-  Definition Item := A.
-
-  Parameter next : mut_ref Self -> M (core.option.Option.t A).
-
-  Global Instance Method_next : Notations.Dot "next" := {
-    Notations.dot := next;
-  }.
-  End Impl_Iterator_for_Slice_IterMut.
-End Impl_Iterator_for_Slice_IterMut.
-
-(* TODO: this is only a temporary implementation,
-         it needs to be rewritten when all std files will be fixed *)
-(* this should be replaced with a generic instance of IntoIterator for Iterator *)
-Module Impl_IntoIterator_for_Slice_IterMut.
-  Section Impl_IntoIterator_for_Slice_IterMut.
-  Context {A : Set}.
-  Definition I := core.slice.IterMut.t A.
-
-  Definition Self := I.
-
-  Definition Item := A.
-  Definition IntoIter := I.
-
-  Parameter into_iter : Self -> M IntoIter.
-
-  Global Instance Method_into_iter :
-    Notations.Dot "into_iter" := {
-    Notations.dot := into_iter;
-  }.
-  End Impl_IntoIterator_for_Slice_IterMut.
-End Impl_IntoIterator_for_Slice_IterMut.
-
-Module Impl_IntoIter_for_Vec.
-  Section Impl_IntoIter_for_Vec.
-  Context {T (* A *) : Set}.
-(*   Context `{alloc.Allocator.Trait A}. *)
-  Definition Self := alloc.vec.Vec T alloc.vec.Vec.Default.A.
-
-  Definition Item := T.
-  Definition IntoIter := alloc.vec.into_iter.IntoIter T None (* (Some A) *).
-
-  Parameter into_iter : Self -> M IntoIter.
-
-(* TODO: uncomment after fixing iter_type.v *)
-(*   Global Instance IntoIter_for_Vec :
-    std.iter_type.IntoIterator Self Item IntoIter := {
-    into_iter := into_iter;
-  }. *)
-  Global Instance Method_into_iter :
-    Notations.Dot "into_iter" := {
-    Notations.dot := into_iter;
-  }.
-  End Impl_IntoIter_for_Vec.
-End Impl_IntoIter_for_Vec.
-
-(* TODO: this is only a temporary implementation,
-         it needs to be rewritten when all std files will be fixed *)
-Module Impl_Iterator_for_Vec_IntoIter.
-  Section Impl_Iterator_for_Vec_IntoIter.
-  Context {T (* A *) : Set}.
-(*   Context `{alloc.Allocator.Trait A}. *)
-  Definition Self := alloc.vec.into_iter.IntoIter T None (* (Some A) *).
-
-  Definition Item := T.
-
-  Parameter next : mut_ref Self -> M (core.option.Option.t T).
-
-  Global Instance Method_next : Notations.Dot "next" := {
-    Notations.dot := next;
-  }.
-  End Impl_Iterator_for_Vec_IntoIter.
-End Impl_Iterator_for_Vec_IntoIter.
-
-(* TODO: this is only a temporary implementation,
-         it needs to be rewritten when all std files will be fixed *)
-Module Impl_IntoIter_for_Vec_IntoIter.
-  Section Impl_IntoIter_for_Vec_IntoIter.
-  Context {T (* A *) : Set}.
-(*   Context `{alloc.Allocator.Trait A}. *)
-  Definition Self := alloc.vec.into_iter.IntoIter T None (* (Some A) *).
-
-  Definition Item := T.
-  Definition IntoIter := alloc.vec.into_iter.IntoIter T None (* (Some A) *).
-
-  Definition into_iter (self : Self) : M IntoIter := M.pure self.
-
-  Global Instance Method_into_iter :
-    Notations.Dot "into_iter" := {
-    Notations.dot := into_iter;
-  }.
-  End Impl_IntoIter_for_Vec_IntoIter.
-End Impl_IntoIter_for_Vec_IntoIter.
-
-(* TODO: a temporary implementation providing methods,
-         which can be called in Rust on Vec,
-         but only after applying a coercion *)
-Module Temp_Impl_for_Vec.
-  Section Temp_Impl_for_Vec.
-  Context {T : Set}.
-
-  Definition Self := alloc.vec.Vec T alloc.vec.Vec.Default.A.
-
-  Parameter iter : ref Self -> M (core.slice.iter.Iter.t T).
-  Parameter iter_mut :
-    ref Self -> M (core.slice.IterMut.t T).
-
-  Global Instance Method_iter : Notations.Dot "iter" := {
-    Notations.dot := iter;
-  }.
-
-  Global Instance Method_iter_mut : Notations.Dot "iter_mut" := {
-    Notations.dot := iter_mut;
-  }.
-  End Temp_Impl_for_Vec.
-End Temp_Impl_for_Vec.
-
 Module Impl_Debug_for_Vec.
   Section Impl_Debug_for_Vec.
   Context {T A : Set}.
@@ -1123,6 +959,18 @@ Module Impl_Iterator_for_RangeInclusive_Z.
 (*   Impl_Iterator_for_Range.Method_next (A := Z). *)
 End Impl_Iterator_for_RangeInclusive_Z.
 
+Module CheckedArith.
+  Module u32.
+    (* pub const fn checked_add(self, rhs: Self) -> Option<Self> *)
+    Parameter checked_add : u32.t -> u32.t -> M (core.option.Option.t u32.t).
+
+    Global Instance AF_checked_add :
+      Notations.DoubleColon u32.t "checked_add" := {
+      Notations.double_colon := checked_add;
+    }.
+  End u32.
+End CheckedArith.
+
 (* a hint for eauto to automatically solve Sigma goals *)
 Global Hint Resolve existT : core.
 

diff --git a/CoqOfRust/M.v b/CoqOfRust/M.v
@@ -248,27 +248,27 @@ Definition catch_return {A : Set} (body : M A) : M A :=
       end
     ).
 
-Definition catch_continue (body : M unit) : M unit :=
+Definition catch_continue (body : M (Val unit)) : M (Val unit) :=
   catch
     body
     (fun exception =>
       match exception with
-      | Exception.Continue => pure tt
+      | Exception.Continue => alloc tt
       | _ => raise exception
       end
     ).
 
-Definition catch_break (body : M unit) : M unit :=
+Definition catch_break (body : M (Val unit)) : M (Val unit) :=
   catch
     body
     (fun exception =>
       match exception with
-      | Exception.Break => pure tt
+      | Exception.Break => alloc tt
       | _ => raise exception
       end
     ).
 
-Definition loop (body : M unit) : M unit :=
+Definition loop (body : M (Val unit)) : M (Val unit) :=
   LowM.Loop
     (catch_continue body)
     (fun result =>

diff --git a/CoqOfRust/alloc/vec.v b/CoqOfRust/alloc/vec.v
@@ -128,16 +128,43 @@ Section Impl_Vec.
 
   Parameter new : M Self.
 
-  Global Instance AssociatedFunction_new :
+  Global Instance AF_new :
     Notations.DoubleColon Self "new" := {
     Notations.double_colon := new;
   }.
 
-  Parameter push : Self -> T -> M unit.
+  Parameter push : mut_ref Self -> T -> M unit.
 
-  Global Instance Method_push :
-    Notations.Dot "push" := {
-    Notations.dot := push;
+  Global Instance AF_push :
+    Notations.DoubleColon Self "push" := {
+    Notations.double_colon := push;
+  }.
+
+  (* pub fn dedup(&mut self) *)
+  Parameter dedup :
+    forall {H0 : core.cmp.PartialEq.Trait T (Rhs := T)},
+    mut_ref Self -> M unit.
+
+  Global Instance AF_dedup {H0 : core.cmp.PartialEq.Trait T} :
+    Notations.DoubleColon Self "dedup" := {
+    Notations.double_colon := dedup (H0 := H0);
+  }.
+
+  (* pub fn len(&self) -> usize *)
+  Parameter len : ref Self -> M usize.t.
+
+  Global Instance AF_len :
+    Notations.DoubleColon Self "len" := {
+    Notations.double_colon := len;
+  }.
+
+  (* pub fn swap_remove(&mut self, index: usize) -> T *)
+  Parameter swap_remove :
+    mut_ref Self -> usize.t -> M T.
+
+  Global Instance AF_swap_remove :
+    Notations.DoubleColon Self "swap_remove" := {
+    Notations.double_colon := swap_remove;
   }.
 
   Global Instance I_Default {ℋ_0 : default.Default.Trait T} :

diff --git a/CoqOfRust/core/fmt.v b/CoqOfRust/core/fmt.v
@@ -118,10 +118,10 @@ Module ImplFormatter.
   *)
   Parameter debug_tuple_field1_finish :
     forall {T : Set} `{core.fmt.Debug.Trait T},
-    M.Val (core.fmt.Formatter.t) ->
-    M.Val (ref str.t) ->
-    M.Val T ->
-    M (M.Val ltac:(Result)).
+    mut_ref core.fmt.Formatter.t ->
+    ref str.t ->
+    ref T ->
+    M ltac:(Result).
 
   Global Instance Formatter_debug_tuple_field1_finish
     {T : Set} `{core.fmt.Debug.Trait T} :