Merge pull request #64 from AeneasVerif/son/merge_back

Merge the forward/backward functions

2 files changed, 129 insertions, 147 deletions

diff --git a/tests/fstar/traits/Primitives.fst b/tests/fstar/traits/Primitives.fst
index a3ffbde4..fca80829 100644
--- a/tests/fstar/traits/Primitives.fst
+++ b/tests/fstar/traits/Primitives.fst
@@ -55,8 +55,7 @@ type string = string
 let is_zero (n: nat) : bool = n = 0
 let decrease (n: nat{n > 0}) : nat = n - 1
 
-let core_mem_replace (a : Type0) (x : a) (y : a) : a = x
-let core_mem_replace_back (a : Type0) (x : a) (y : a) : a = y
+let core_mem_replace (a : Type0) (x : a) (y : a) : a & a = (x, x)
 
 // We don't really use raw pointers for now
 type mut_raw_ptr (t : Type0) = { v : t }
@@ -477,8 +476,7 @@ noeq type core_ops_index_Index (self idx : Type0) = {
 // Trait declaration: [core::ops::index::IndexMut]
 noeq type core_ops_index_IndexMut (self idx : Type0) = {
   indexInst : core_ops_index_Index self idx;
-  index_mut : self → idx → result indexInst.output;
-  index_mut_back : self → idx → indexInst.output → result self;
+  index_mut : self → idx → result (indexInst.output & (indexInst.output → result self));
 }
 
 // Trait declaration [core::ops::deref::Deref]
@@ -490,8 +488,7 @@ noeq type core_ops_deref_Deref (self : Type0) = {
 // Trait declaration [core::ops::deref::DerefMut]
 noeq type core_ops_deref_DerefMut (self : Type0) = {
   derefInst : core_ops_deref_Deref self;
-  deref_mut : self → result derefInst.target;
-  deref_mut_back : self → derefInst.target → result self;
+  deref_mut : self → result (derefInst.target & (derefInst.target → result self));
 }
 
 type core_ops_range_Range (a : Type0) = {
@@ -502,8 +499,8 @@ type core_ops_range_Range (a : Type0) = {
 (*** [alloc] *)
 
 let alloc_boxed_Box_deref (t : Type0) (x : t) : result t = Return x
-let alloc_boxed_Box_deref_mut (t : Type0) (x : t) : result t = Return x
-let alloc_boxed_Box_deref_mut_back (t : Type) (_ : t) (x : t) : result t = Return x
+let alloc_boxed_Box_deref_mut (t : Type0) (x : t) : result (t & (t -> result t)) =
+  Return (x, (fun x -> Return x))
 
 // Trait instance
 let alloc_boxed_Box_coreopsDerefInst (self : Type0) : core_ops_deref_Deref self = {
@@ -515,7 +512,6 @@ let alloc_boxed_Box_coreopsDerefInst (self : Type0) : core_ops_deref_Deref self
 let alloc_boxed_Box_coreopsDerefMutInst (self : Type0) : core_ops_deref_DerefMut self = {
   derefInst = alloc_boxed_Box_coreopsDerefInst self;
   deref_mut = alloc_boxed_Box_deref_mut self;
-  deref_mut_back = alloc_boxed_Box_deref_mut_back self;
 }
 
 (*** Array *)
@@ -535,10 +531,18 @@ let array_index_usize (a : Type0) (n : usize) (x : array a n) (i : usize) : resu
   if i < length x then Return (index x i)
   else Fail Failure
 
-let array_update_usize (a : Type0) (n : usize) (x : array a n) (i : usize) (nx : a) : result (array a n) =
+let array_update_usize (a : Type0) (n : usize) (x : array a n) (i : usize) (nx : a) :
+  result (array a n) =
   if i < length x then Return (list_update x i nx)
   else Fail Failure
 
+let array_index_mut_usize (a : Type0) (n : usize) (x : array a n) (i : usize) :
+  result (a & (a -> result (array a n))) =
+  match array_index_usize a n x i with
+  | Fail e -> Fail e
+  | Return v ->
+    Return (v, array_update_usize a n x i)
+
 (*** Slice *)
 type slice (a : Type0) = s:list a{length s <= usize_max}
 
@@ -552,6 +556,13 @@ let slice_update_usize (a : Type0) (x : slice a) (i : usize) (nx : a) : result (
   if i < length x then Return (list_update x i nx)
   else Fail Failure
 
+let slice_index_mut_usize (a : Type0) (s : slice a) (i : usize) :
+  result (a & (a -> result (slice a))) =
+  match slice_index_usize a s i with
+  | Fail e -> Fail e
+  | Return x ->
+    Return (x, slice_update_usize a s i)
+
 (*** Subslices *)
 
 let array_to_slice (a : Type0) (n : usize) (x : array a n) : result (slice a) = Return x
@@ -559,6 +570,10 @@ let array_from_slice (a : Type0) (n : usize) (x : array a n) (s : slice a) : res
   if length s = n then Return s
   else Fail Failure
 
+let array_to_slice_mut (a : Type0) (n : usize) (x : array a n) :
+  result (slice a & (slice a -> result (array a n))) =
+  Return (x, array_from_slice a n x)
+
 // TODO: finish the definitions below (there lacks [List.drop] and [List.take] in the standard library *)
 let array_subslice (a : Type0) (n : usize) (x : array a n) (r : core_ops_range_Range usize) : result (slice a) =
   admit()
@@ -588,8 +603,13 @@ let alloc_vec_Vec_index_usize (#a : Type0) (v : alloc_vec_Vec a) (i : usize) : r
 let alloc_vec_Vec_update_usize (#a : Type0) (v : alloc_vec_Vec a) (i : usize) (x : a) : result (alloc_vec_Vec a) =
   if i < length v then Return (list_update v i x) else Fail Failure
 
-// The **forward** function shouldn't be used
-let alloc_vec_Vec_push_fwd (a  : Type0) (v : alloc_vec_Vec a) (x : a) : unit = ()
+let alloc_vec_Vec_index_mut_usize (#a : Type0) (v: alloc_vec_Vec a) (i: usize) :
+  result (a & (a → result (alloc_vec_Vec a))) =
+  match alloc_vec_Vec_index_usize v i with
+  | Return x ->
+    Return (x, alloc_vec_Vec_update_usize v i)
+  | Fail e -> Fail e
+
 let alloc_vec_Vec_push (a  : Type0) (v : alloc_vec_Vec a) (x : a) :
   Pure (result (alloc_vec_Vec a))
   (requires True)
@@ -605,9 +625,6 @@ let alloc_vec_Vec_push (a  : Type0) (v : alloc_vec_Vec a) (x : a) :
     end
   else Fail Failure
 
-// The **forward** function shouldn't be used
-let alloc_vec_Vec_insert_fwd (a : Type0) (v : alloc_vec_Vec a) (i : usize) (x : a) : result unit =
-  if i < length v then Return () else Fail Failure
 let alloc_vec_Vec_insert (a : Type0) (v : alloc_vec_Vec a) (i : usize) (x : a) : result (alloc_vec_Vec a) =
   if i < length v then Return (list_update v i x) else Fail Failure
 
@@ -619,13 +636,11 @@ noeq type core_slice_index_SliceIndex (self t : Type0) = {
   sealedInst : core_slice_index_private_slice_index_Sealed self;
   output : Type0;
   get : self → t → result (option output);
-  get_mut : self → t → result (option output);
-  get_mut_back : self → t → option output → result t;
+  get_mut : self → t → result (option output & (option output -> result t));
   get_unchecked : self → const_raw_ptr t → result (const_raw_ptr output);
   get_unchecked_mut : self → mut_raw_ptr t → result (mut_raw_ptr output);
   index : self → t → result output;
-  index_mut : self → t → result output;
-  index_mut_back : self → t → output → result t;
+  index_mut : self → t → result (output & (output -> result t));
 }
 
 // [core::slice::index::[T]::index]: forward function
@@ -643,14 +658,8 @@ let core_slice_index_RangeUsize_get (t : Type0) (i : core_ops_range_Range usize)
   admit () // TODO
 
 // [core::slice::index::Range::get_mut]: forward function
-let core_slice_index_RangeUsize_get_mut
-  (t : Type0) : core_ops_range_Range usize → slice t → result (option (slice t)) =
-  admit () // TODO
-
-// [core::slice::index::Range::get_mut]: backward function 0
-let core_slice_index_RangeUsize_get_mut_back
-  (t : Type0) :
-  core_ops_range_Range usize → slice t → option (slice t) → result (slice t) =
+let core_slice_index_RangeUsize_get_mut (t : Type0) :
+  core_ops_range_Range usize → slice t → result (option (slice t) & (option (slice t) -> result (slice t))) =
   admit () // TODO
 
 // [core::slice::index::Range::get_unchecked]: forward function
@@ -675,27 +684,16 @@ let core_slice_index_RangeUsize_index
   admit () // TODO
 
 // [core::slice::index::Range::index_mut]: forward function
-let core_slice_index_RangeUsize_index_mut
-  (t : Type0) : core_ops_range_Range usize → slice t → result (slice t) =
-  admit () // TODO
-
-// [core::slice::index::Range::index_mut]: backward function 0
-let core_slice_index_RangeUsize_index_mut_back
-  (t : Type0) : core_ops_range_Range usize → slice t → slice t → result (slice t) =
+let core_slice_index_RangeUsize_index_mut (t : Type0) :
+  core_ops_range_Range usize → slice t → result (slice t & (slice t -> result (slice t))) =
   admit () // TODO
 
 // [core::slice::index::[T]::index_mut]: forward function
 let core_slice_index_Slice_index_mut
   (t idx : Type0) (inst : core_slice_index_SliceIndex idx (slice t)) :
-  slice t → idx → result inst.output =
+  slice t → idx → result (inst.output & (inst.output -> result (slice t))) =
   admit () // 
 
-// [core::slice::index::[T]::index_mut]: backward function 0
-let core_slice_index_Slice_index_mut_back
-  (t idx : Type0) (inst : core_slice_index_SliceIndex idx (slice t)) :
-  slice t → idx → inst.output → result (slice t) =
-  admit () // TODO
-
 // [core::array::[T; N]::index]: forward function
 let core_array_Array_index
   (t idx : Type0) (n : usize) (inst : core_ops_index_Index (slice t) idx)
@@ -705,13 +703,8 @@ let core_array_Array_index
 // [core::array::[T; N]::index_mut]: forward function
 let core_array_Array_index_mut
   (t idx : Type0) (n : usize) (inst : core_ops_index_IndexMut (slice t) idx)
-  (a : array t n) (i : idx) : result inst.indexInst.output =
-  admit () // TODO
-
-// [core::array::[T; N]::index_mut]: backward function 0
-let core_array_Array_index_mut_back
-  (t idx : Type0) (n : usize) (inst : core_ops_index_IndexMut (slice t) idx)
-  (a : array t n) (i : idx) (x : inst.indexInst.output) : result (array t n) =
+  (a : array t n) (i : idx) :
+  result (inst.indexInst.output & (inst.indexInst.output -> result (array t n))) =
   admit () // TODO
 
 // Trait implementation: [core::slice::index::private_slice_index::Range]
@@ -725,12 +718,10 @@ let core_slice_index_SliceIndexRangeUsizeSliceTInst (t : Type0) :
   output = slice t;
   get = core_slice_index_RangeUsize_get t;
   get_mut = core_slice_index_RangeUsize_get_mut t;
-  get_mut_back = core_slice_index_RangeUsize_get_mut_back t;
   get_unchecked = core_slice_index_RangeUsize_get_unchecked t;
   get_unchecked_mut = core_slice_index_RangeUsize_get_unchecked_mut t;
   index = core_slice_index_RangeUsize_index t;
   index_mut = core_slice_index_RangeUsize_index_mut t;
-  index_mut_back = core_slice_index_RangeUsize_index_mut_back t;
 }
 
 // Trait implementation: [core::slice::index::[T]]
@@ -747,7 +738,6 @@ let core_ops_index_IndexMutSliceTIInst (t idx : Type0)
   core_ops_index_IndexMut (slice t) idx = {
   indexInst = core_ops_index_IndexSliceTIInst t idx inst;
   index_mut = core_slice_index_Slice_index_mut t idx inst;
-  index_mut_back = core_slice_index_Slice_index_mut_back t idx inst;
 }
 
 // Trait implementation: [core::array::[T; N]]
@@ -764,7 +754,6 @@ let core_ops_index_IndexMutArrayIInst (t idx : Type0) (n : usize)
   core_ops_index_IndexMut (array t n) idx = {
   indexInst = core_ops_index_IndexArrayInst t idx n inst.indexInst;
   index_mut = core_array_Array_index_mut t idx n inst;
-  index_mut_back = core_array_Array_index_mut_back t idx n inst;
 }
 
 // [core::slice::index::usize::get]: forward function
@@ -773,13 +762,8 @@ let core_slice_index_usize_get
   admit () // TODO
 
 // [core::slice::index::usize::get_mut]: forward function
-let core_slice_index_usize_get_mut
-  (t : Type0) : usize → slice t → result (option t) =
-  admit () // TODO
-
-// [core::slice::index::usize::get_mut]: backward function 0
-let core_slice_index_usize_get_mut_back
-  (t : Type0) : usize → slice t → option t → result (slice t) =
+let core_slice_index_usize_get_mut (t : Type0) :
+  usize → slice t → result (option t & (option t -> result (slice t))) =
   admit () // TODO
 
 // [core::slice::index::usize::get_unchecked]: forward function
@@ -797,12 +781,8 @@ let core_slice_index_usize_index (t : Type0) : usize → slice t → result t =
   admit () // TODO
 
 // [core::slice::index::usize::index_mut]: forward function
-let core_slice_index_usize_index_mut (t : Type0) : usize → slice t → result t =
-  admit () // TODO
-
-// [core::slice::index::usize::index_mut]: backward function 0
-let core_slice_index_usize_index_mut_back
-  (t : Type0) : usize → slice t → t → result (slice t) =
+let core_slice_index_usize_index_mut (t : Type0) :
+  usize → slice t → result (t & (t -> result (slice t))) =
   admit () // TODO
 
 // Trait implementation: [core::slice::index::private_slice_index::usize]
@@ -816,12 +796,10 @@ let core_slice_index_SliceIndexUsizeSliceTInst (t : Type0) :
   output = t;
   get = core_slice_index_usize_get t;
   get_mut = core_slice_index_usize_get_mut t;
-  get_mut_back = core_slice_index_usize_get_mut_back t;
   get_unchecked = core_slice_index_usize_get_unchecked t;
   get_unchecked_mut = core_slice_index_usize_get_unchecked_mut t;
   index = core_slice_index_usize_index t;
   index_mut = core_slice_index_usize_index_mut t;
-  index_mut_back = core_slice_index_usize_index_mut_back t;
 }
 
 // [alloc::vec::Vec::index]: forward function
@@ -831,13 +809,8 @@ let alloc_vec_Vec_index (t idx : Type0) (inst : core_slice_index_SliceIndex idx
 
 // [alloc::vec::Vec::index_mut]: forward function
 let alloc_vec_Vec_index_mut (t idx : Type0) (inst : core_slice_index_SliceIndex idx (slice t))
-  (self : alloc_vec_Vec t) (i : idx) : result inst.output =
-  admit () // TODO
-
-// [alloc::vec::Vec::index_mut]: backward function 0
-let alloc_vec_Vec_index_mut_back
-  (t idx : Type0) (inst : core_slice_index_SliceIndex idx (slice t))
-  (self : alloc_vec_Vec t) (i : idx) (x : inst.output) : result (alloc_vec_Vec t) =
+  (self : alloc_vec_Vec t) (i : idx) :
+  result (inst.output & (inst.output -> result (alloc_vec_Vec t))) =
   admit () // TODO
 
 // Trait implementation: [alloc::vec::Vec]
@@ -854,7 +827,6 @@ let alloc_vec_Vec_coreopsindexIndexMutInst (t idx : Type0)
   core_ops_index_IndexMut (alloc_vec_Vec t) idx = {
   indexInst = alloc_vec_Vec_coreopsindexIndexInst t idx inst;
   index_mut = alloc_vec_Vec_index_mut t idx inst;
-  index_mut_back = alloc_vec_Vec_index_mut_back t idx inst;
 }
 
 (*** Theorems *)
@@ -870,15 +842,7 @@ let alloc_vec_Vec_index_eq (#a : Type0) (v : alloc_vec_Vec a) (i : usize) :
 let alloc_vec_Vec_index_mut_eq (#a : Type0) (v : alloc_vec_Vec a) (i : usize) :
   Lemma (
     alloc_vec_Vec_index_mut a usize (core_slice_index_SliceIndexUsizeSliceTInst a) v i ==
-      alloc_vec_Vec_index_usize v i)
+      alloc_vec_Vec_index_mut_usize v i)
   [SMTPat (alloc_vec_Vec_index_mut a usize (core_slice_index_SliceIndexUsizeSliceTInst a) v i)]
   =
   admit()
-
-let alloc_vec_Vec_index_mut_back_eq (#a : Type0) (v : alloc_vec_Vec a) (i : usize) (x : a) :
-  Lemma (
-    alloc_vec_Vec_index_mut_back a usize (core_slice_index_SliceIndexUsizeSliceTInst a) v i x ==
-      alloc_vec_Vec_update_usize v i x)
-  [SMTPat (alloc_vec_Vec_index_mut_back a usize (core_slice_index_SliceIndexUsizeSliceTInst a) v i x)]
-  =
-  admit()
diff --git a/tests/fstar/traits/Traits.fst b/tests/fstar/traits/Traits.fst
index 7d504cb5..cb9c1654 100644
--- a/tests/fstar/traits/Traits.fst
+++ b/tests/fstar/traits/Traits.fst
@@ -9,7 +9,7 @@ open Primitives
     Source: 'src/traits.rs', lines 1:0-1:19 *)
 noeq type boolTrait_t (self : Type0) = { get_bool : self -> result bool; }
 
-(** [traits::{bool}::get_bool]: forward function
+(** [traits::{bool}::get_bool]:
     Source: 'src/traits.rs', lines 12:4-12:30 *)
 let bool_get_bool (self : bool) : result bool =
   Return self
@@ -18,24 +18,24 @@ let bool_get_bool (self : bool) : result bool =
     Source: 'src/traits.rs', lines 11:0-11:23 *)
 let traits_BoolTraitBoolInst : boolTrait_t bool = { get_bool = bool_get_bool; }
 
-(** [traits::BoolTrait::ret_true]: forward function
+(** [traits::BoolTrait::ret_true]:
     Source: 'src/traits.rs', lines 6:4-6:30 *)
 let boolTrait_ret_true
-  (#self : Type0) (self_clause : boolTrait_t self) (self0 : self) :
+  (#self : Type0) (self_clause : boolTrait_t self) (self1 : self) :
   result bool
   =
   Return true
 
-(** [traits::test_bool_trait_bool]: forward function
+(** [traits::test_bool_trait_bool]:
     Source: 'src/traits.rs', lines 17:0-17:44 *)
 let test_bool_trait_bool (x : bool) : result bool =
   let* b = bool_get_bool x in
   if b then boolTrait_ret_true traits_BoolTraitBoolInst x else Return false
 
-(** [traits::{core::option::Option<T>#1}::get_bool]: forward function
+(** [traits::{core::option::Option<T>#1}::get_bool]:
     Source: 'src/traits.rs', lines 23:4-23:30 *)
 let option_get_bool (t : Type0) (self : option t) : result bool =
-  begin match self with | None -> Return false | Some x -> Return true end
+  begin match self with | None -> Return false | Some _ -> Return true end
 
 (** Trait implementation: [traits::{core::option::Option<T>#1}]
     Source: 'src/traits.rs', lines 22:0-22:31 *)
@@ -44,7 +44,7 @@ let traits_BoolTraitcoreoptionOptionTInst (t : Type0) : boolTrait_t (option t)
   get_bool = option_get_bool t;
 }
 
-(** [traits::test_bool_trait_option]: forward function
+(** [traits::test_bool_trait_option]:
     Source: 'src/traits.rs', lines 31:0-31:54 *)
 let test_bool_trait_option (t : Type0) (x : option t) : result bool =
   let* b = option_get_bool t x in
@@ -52,7 +52,7 @@ let test_bool_trait_option (t : Type0) (x : option t) : result bool =
   then boolTrait_ret_true (traits_BoolTraitcoreoptionOptionTInst t) x
   else Return false
 
-(** [traits::test_bool_trait]: forward function
+(** [traits::test_bool_trait]:
     Source: 'src/traits.rs', lines 35:0-35:50 *)
 let test_bool_trait
   (t : Type0) (boolTraitTInst : boolTrait_t t) (x : t) : result bool =
@@ -62,7 +62,7 @@ let test_bool_trait
     Source: 'src/traits.rs', lines 39:0-39:15 *)
 noeq type toU64_t (self : Type0) = { to_u64 : self -> result u64; }
 
-(** [traits::{u64#2}::to_u64]: forward function
+(** [traits::{u64#2}::to_u64]:
     Source: 'src/traits.rs', lines 44:4-44:26 *)
 let u64_to_u64 (self : u64) : result u64 =
   Return self
@@ -71,14 +71,14 @@ let u64_to_u64 (self : u64) : result u64 =
     Source: 'src/traits.rs', lines 43:0-43:18 *)
 let traits_ToU64U64Inst : toU64_t u64 = { to_u64 = u64_to_u64; }
 
-(** [traits::{(A, A)#3}::to_u64]: forward function
+(** [traits::{(A, A)#3}::to_u64]:
     Source: 'src/traits.rs', lines 50:4-50:26 *)
 let pair_to_u64
   (a : Type0) (toU64AInst : toU64_t a) (self : (a & a)) : result u64 =
-  let (x, x0) = self in
+  let (x, x1) = self in
   let* i = toU64AInst.to_u64 x in
-  let* i0 = toU64AInst.to_u64 x0 in
-  u64_add i i0
+  let* i1 = toU64AInst.to_u64 x1 in
+  u64_add i i1
 
 (** Trait implementation: [traits::{(A, A)#3}]
     Source: 'src/traits.rs', lines 49:0-49:31 *)
@@ -87,18 +87,18 @@ let traits_ToU64TupleAAInst (a : Type0) (toU64AInst : toU64_t a) : toU64_t (a &
   to_u64 = pair_to_u64 a toU64AInst;
 }
 
-(** [traits::f]: forward function
+(** [traits::f]:
     Source: 'src/traits.rs', lines 55:0-55:36 *)
 let f (t : Type0) (toU64TInst : toU64_t t) (x : (t & t)) : result u64 =
   pair_to_u64 t toU64TInst x
 
-(** [traits::g]: forward function
+(** [traits::g]:
     Source: 'src/traits.rs', lines 59:0-61:18 *)
 let g
   (t : Type0) (toU64TupleTTInst : toU64_t (t & t)) (x : (t & t)) : result u64 =
   toU64TupleTTInst.to_u64 x
 
-(** [traits::h0]: forward function
+(** [traits::h0]:
     Source: 'src/traits.rs', lines 66:0-66:24 *)
 let h0 (x : u64) : result u64 =
   u64_to_u64 x
@@ -107,7 +107,7 @@ let h0 (x : u64) : result u64 =
     Source: 'src/traits.rs', lines 70:0-70:21 *)
 type wrapper_t (t : Type0) = { x : t; }
 
-(** [traits::{traits::Wrapper<T>#4}::to_u64]: forward function
+(** [traits::{traits::Wrapper<T>#4}::to_u64]:
     Source: 'src/traits.rs', lines 75:4-75:26 *)
 let wrapper_to_u64
   (t : Type0) (toU64TInst : toU64_t t) (self : wrapper_t t) : result u64 =
@@ -120,12 +120,12 @@ let traits_ToU64traitsWrapperTInst (t : Type0) (toU64TInst : toU64_t t) :
   to_u64 = wrapper_to_u64 t toU64TInst;
 }
 
-(** [traits::h1]: forward function
+(** [traits::h1]:
     Source: 'src/traits.rs', lines 80:0-80:33 *)
 let h1 (x : wrapper_t u64) : result u64 =
   wrapper_to_u64 u64 traits_ToU64U64Inst x
 
-(** [traits::h2]: forward function
+(** [traits::h2]:
     Source: 'src/traits.rs', lines 84:0-84:41 *)
 let h2 (t : Type0) (toU64TInst : toU64_t t) (x : wrapper_t t) : result u64 =
   wrapper_to_u64 t toU64TInst x
@@ -134,7 +134,7 @@ let h2 (t : Type0) (toU64TInst : toU64_t t) (x : wrapper_t t) : result u64 =
     Source: 'src/traits.rs', lines 88:0-88:19 *)
 noeq type toType_t (self t : Type0) = { to_type : self -> result t; }
 
-(** [traits::{u64#5}::to_type]: forward function
+(** [traits::{u64#5}::to_type]:
     Source: 'src/traits.rs', lines 93:4-93:28 *)
 let u64_to_type (self : u64) : result bool =
   Return (self > 0)
@@ -150,7 +150,7 @@ noeq type ofType_t (self : Type0) = {
     self;
 }
 
-(** [traits::h3]: forward function
+(** [traits::h3]:
     Source: 'src/traits.rs', lines 104:0-104:50 *)
 let h3
   (t1 t2 : Type0) (ofTypeT1Inst : ofType_t t1) (toTypeT2T1Inst : toType_t t2
@@ -166,7 +166,7 @@ noeq type ofTypeBis_t (self t : Type0) = {
   of_type : t -> result self;
 }
 
-(** [traits::h4]: forward function
+(** [traits::h4]:
     Source: 'src/traits.rs', lines 118:0-118:57 *)
 let h4
   (t1 t2 : Type0) (ofTypeBisT1T2Inst : ofTypeBis_t t1 t2) (toTypeT2T1Inst :
@@ -189,7 +189,7 @@ noeq type testType_test_TestTrait_t (self : Type0) = {
   test : self -> result bool;
 }
 
-(** [traits::{traits::TestType<T>#6}::test::{traits::{traits::TestType<T>#6}::test::TestType1}::test]: forward function
+(** [traits::{traits::TestType<T>#6}::test::{traits::{traits::TestType<T>#6}::test::TestType1}::test]:
     Source: 'src/traits.rs', lines 139:12-139:34 *)
 let testType_test_TestType1_test
   (self : testType_test_TestType1_t) : result bool =
@@ -202,20 +202,20 @@ let traits_TestType_test_TestTraittraitstraitsTestTypeTtestTestType1Inst :
   test = testType_test_TestType1_test;
 }
 
-(** [traits::{traits::TestType<T>#6}::test]: forward function
+(** [traits::{traits::TestType<T>#6}::test]:
     Source: 'src/traits.rs', lines 126:4-126:36 *)
 let testType_test
   (t : Type0) (toU64TInst : toU64_t t) (self : testType_t t) (x : t) :
   result bool
   =
-  let* x0 = toU64TInst.to_u64 x in
-  if x0 > 0 then testType_test_TestType1_test 0 else Return false
+  let* x1 = toU64TInst.to_u64 x in
+  if x1 > 0 then testType_test_TestType1_test 0 else Return false
 
 (** [traits::BoolWrapper]
     Source: 'src/traits.rs', lines 150:0-150:22 *)
 type boolWrapper_t = bool
 
-(** [traits::{traits::BoolWrapper#7}::to_type]: forward function
+(** [traits::{traits::BoolWrapper#7}::to_type]:
     Source: 'src/traits.rs', lines 156:4-156:25 *)
 let boolWrapper_to_type
   (t : Type0) (toTypeBoolTInst : toType_t bool t) (self : boolWrapper_t) :
@@ -251,8 +251,7 @@ noeq type withConstTy_t (self : Type0) (len : usize) = {
 let bool_len1_body : result usize = Return 12
 let bool_len1_c : usize = eval_global bool_len1_body
 
-(** [traits::{bool#8}::f]: merged forward/backward function
-    (there is a single backward function, and the forward function returns ())
+(** [traits::{bool#8}::f]:
     Source: 'src/traits.rs', lines 180:4-180:39 *)
 let bool_f (i : u64) (a : array u8 32) : result u64 =
   Return i
@@ -268,15 +267,15 @@ let traits_WithConstTyBool32Inst : withConstTy_t bool 32 = {
   f = bool_f;
 }
 
-(** [traits::use_with_const_ty1]: forward function
+(** [traits::use_with_const_ty1]:
     Source: 'src/traits.rs', lines 183:0-183:75 *)
 let use_with_const_ty1
   (h : Type0) (len : usize) (withConstTyHLENInst : withConstTy_t h len) :
   result usize
   =
-  let i = withConstTyHLENInst.cLEN1 in Return i
+  Return withConstTyHLENInst.cLEN1
 
-(** [traits::use_with_const_ty2]: forward function
+(** [traits::use_with_const_ty2]:
     Source: 'src/traits.rs', lines 187:0-187:73 *)
 let use_with_const_ty2
   (h : Type0) (len : usize) (withConstTyHLENInst : withConstTy_t h len)
@@ -285,7 +284,7 @@ let use_with_const_ty2
   =
   Return ()
 
-(** [traits::use_with_const_ty3]: forward function
+(** [traits::use_with_const_ty3]:
     Source: 'src/traits.rs', lines 189:0-189:80 *)
 let use_with_const_ty3
   (h : Type0) (len : usize) (withConstTyHLENInst : withConstTy_t h len)
@@ -294,12 +293,12 @@ let use_with_const_ty3
   =
   withConstTyHLENInst.tW_clause_0.to_u64 x
 
-(** [traits::test_where1]: forward function
+(** [traits::test_where1]:
     Source: 'src/traits.rs', lines 193:0-193:40 *)
 let test_where1 (t : Type0) (_x : t) : result unit =
   Return ()
 
-(** [traits::test_where2]: forward function
+(** [traits::test_where2]:
     Source: 'src/traits.rs', lines 194:0-194:57 *)
 let test_where2
   (t : Type0) (withConstTyT32Inst : withConstTy_t t 32) (_x : u32) :
@@ -326,22 +325,30 @@ noeq type childTrait_t (self : Type0) = {
   parentTrait1SelfInst : parentTrait1_t self;
 }
 
-(** [traits::test_child_trait1]: forward function
-    Source: 'src/traits.rs', lines 209:0-209:56 *)
+(** [traits::test_parent_trait0]:
+    Source: 'src/traits.rs', lines 208:0-208:57 *)
+let test_parent_trait0
+  (t : Type0) (parentTrait0TInst : parentTrait0_t t) (x : t) :
+  result parentTrait0TInst.tW
+  =
+  parentTrait0TInst.get_w x
+
+(** [traits::test_child_trait1]:
+    Source: 'src/traits.rs', lines 213:0-213:56 *)
 let test_child_trait1
   (t : Type0) (childTraitTInst : childTrait_t t) (x : t) : result string =
   childTraitTInst.parentTrait0SelfInst.get_name x
 
-(** [traits::test_child_trait2]: forward function
-    Source: 'src/traits.rs', lines 213:0-213:54 *)
+(** [traits::test_child_trait2]:
+    Source: 'src/traits.rs', lines 217:0-217:54 *)
 let test_child_trait2
   (t : Type0) (childTraitTInst : childTrait_t t) (x : t) :
   result childTraitTInst.parentTrait0SelfInst.tW
   =
   childTraitTInst.parentTrait0SelfInst.get_w x
 
-(** [traits::order1]: forward function
-    Source: 'src/traits.rs', lines 219:0-219:59 *)
+(** [traits::order1]:
+    Source: 'src/traits.rs', lines 223:0-223:59 *)
 let order1
   (t u : Type0) (parentTrait0TInst : parentTrait0_t t) (parentTrait0UInst :
   parentTrait0_t u) :
@@ -350,27 +357,27 @@ let order1
   Return ()
 
 (** Trait declaration: [traits::ChildTrait1]
-    Source: 'src/traits.rs', lines 222:0-222:35 *)
+    Source: 'src/traits.rs', lines 226:0-226:35 *)
 noeq type childTrait1_t (self : Type0) = {
   parentTrait1SelfInst : parentTrait1_t self;
 }
 
 (** Trait implementation: [traits::{usize#9}]
-    Source: 'src/traits.rs', lines 224:0-224:27 *)
+    Source: 'src/traits.rs', lines 228:0-228:27 *)
 let traits_ParentTrait1UsizeInst : parentTrait1_t usize = ()
 
 (** Trait implementation: [traits::{usize#10}]
-    Source: 'src/traits.rs', lines 225:0-225:26 *)
+    Source: 'src/traits.rs', lines 229:0-229:26 *)
 let traits_ChildTrait1UsizeInst : childTrait1_t usize = {
   parentTrait1SelfInst = traits_ParentTrait1UsizeInst;
 }
 
 (** Trait declaration: [traits::Iterator]
-    Source: 'src/traits.rs', lines 229:0-229:18 *)
+    Source: 'src/traits.rs', lines 233:0-233:18 *)
 noeq type iterator_t (self : Type0) = { tItem : Type0; }
 
 (** Trait declaration: [traits::IntoIterator]
-    Source: 'src/traits.rs', lines 233:0-233:22 *)
+    Source: 'src/traits.rs', lines 237:0-237:22 *)
 noeq type intoIterator_t (self : Type0) = {
   tItem : Type0;
   tIntoIter : Type0;
@@ -379,29 +386,29 @@ noeq type intoIterator_t (self : Type0) = {
 }
 
 (** Trait declaration: [traits::FromResidual]
-    Source: 'src/traits.rs', lines 250:0-250:21 *)
+    Source: 'src/traits.rs', lines 254:0-254:21 *)
 type fromResidual_t (self t : Type0) = unit
 
 (** Trait declaration: [traits::Try]
-    Source: 'src/traits.rs', lines 246:0-246:48 *)
+    Source: 'src/traits.rs', lines 250:0-250:48 *)
 noeq type try_t (self : Type0) = {
   tResidual : Type0;
   fromResidualSelftraitsTrySelfResidualInst : fromResidual_t self tResidual;
 }
 
 (** Trait declaration: [traits::WithTarget]
-    Source: 'src/traits.rs', lines 252:0-252:20 *)
+    Source: 'src/traits.rs', lines 256:0-256:20 *)
 noeq type withTarget_t (self : Type0) = { tTarget : Type0; }
 
 (** Trait declaration: [traits::ParentTrait2]
-    Source: 'src/traits.rs', lines 256:0-256:22 *)
+    Source: 'src/traits.rs', lines 260:0-260:22 *)
 noeq type parentTrait2_t (self : Type0) = {
   tU : Type0;
   tU_clause_0 : withTarget_t tU;
 }
 
 (** Trait declaration: [traits::ChildTrait2]
-    Source: 'src/traits.rs', lines 260:0-260:35 *)
+    Source: 'src/traits.rs', lines 264:0-264:35 *)
 noeq type childTrait2_t (self : Type0) = {
   parentTrait2SelfInst : parentTrait2_t self;
   convert : parentTrait2SelfInst.tU -> result
@@ -409,48 +416,59 @@ noeq type childTrait2_t (self : Type0) = {
 }
 
 (** Trait implementation: [traits::{u32#11}]
-    Source: 'src/traits.rs', lines 264:0-264:23 *)
+    Source: 'src/traits.rs', lines 268:0-268:23 *)
 let traits_WithTargetU32Inst : withTarget_t u32 = { tTarget = u32; }
 
 (** Trait implementation: [traits::{u32#12}]
-    Source: 'src/traits.rs', lines 268:0-268:25 *)
+    Source: 'src/traits.rs', lines 272:0-272:25 *)
 let traits_ParentTrait2U32Inst : parentTrait2_t u32 = {
   tU = u32;
   tU_clause_0 = traits_WithTargetU32Inst;
 }
 
-(** [traits::{u32#13}::convert]: forward function
-    Source: 'src/traits.rs', lines 273:4-273:29 *)
+(** [traits::{u32#13}::convert]:
+    Source: 'src/traits.rs', lines 277:4-277:29 *)
 let u32_convert (x : u32) : result u32 =
   Return x
 
 (** Trait implementation: [traits::{u32#13}]
-    Source: 'src/traits.rs', lines 272:0-272:24 *)
+    Source: 'src/traits.rs', lines 276:0-276:24 *)
 let traits_ChildTrait2U32Inst : childTrait2_t u32 = {
   parentTrait2SelfInst = traits_ParentTrait2U32Inst;
   convert = u32_convert;
 }
 
 (** Trait declaration: [traits::CFnOnce]
-    Source: 'src/traits.rs', lines 286:0-286:23 *)
+    Source: 'src/traits.rs', lines 290:0-290:23 *)
 noeq type cFnOnce_t (self args : Type0) = {
   tOutput : Type0;
   call_once : self -> args -> result tOutput;
 }
 
 (** Trait declaration: [traits::CFnMut]
-    Source: 'src/traits.rs', lines 292:0-292:37 *)
+    Source: 'src/traits.rs', lines 296:0-296:37 *)
 noeq type cFnMut_t (self args : Type0) = {
   cFnOnceSelfArgsInst : cFnOnce_t self args;
-  call_mut : self -> args -> result cFnOnceSelfArgsInst.tOutput;
-  call_mut_back : self -> args -> cFnOnceSelfArgsInst.tOutput -> result self;
+  call_mut : self -> args -> result (cFnOnceSelfArgsInst.tOutput & self);
 }
 
 (** Trait declaration: [traits::CFn]
-    Source: 'src/traits.rs', lines 296:0-296:33 *)
+    Source: 'src/traits.rs', lines 300:0-300:33 *)
 noeq type cFn_t (self args : Type0) = {
   cFnMutSelfArgsInst : cFnMut_t self args;
-  call_mut : self -> args -> result
-    cFnMutSelfArgsInst.cFnOnceSelfArgsInst.tOutput;
+  call : self -> args -> result cFnMutSelfArgsInst.cFnOnceSelfArgsInst.tOutput;
+}
+
+(** Trait declaration: [traits::GetTrait]
+    Source: 'src/traits.rs', lines 304:0-304:18 *)
+noeq type getTrait_t (self : Type0) = { tW : Type0; get_w : self -> result tW;
 }
 
+(** [traits::test_get_trait]:
+    Source: 'src/traits.rs', lines 309:0-309:49 *)
+let test_get_trait
+  (t : Type0) (getTraitTInst : getTrait_t t) (x : t) :
+  result getTraitTInst.tW
+  =
+  getTraitTInst.get_w x
+