Merge pull request #210 from formal-land/bk@compile-more-of-ink_env-8

Compile more of ink_env.v 8
formal-land · Sep 19, 2023 · 876f3e4 · 876f3e4
2 parents 5a03c98 + d8d26d4
commit 876f3e4
Show file tree

Hide file tree

Showing 5 changed files with 364 additions and 276 deletions.
diff --git a/CoqOfRust/ink/erc20.v b/CoqOfRust/ink/erc20.v
@@ -3103,7 +3103,7 @@ Module
       let* _ :=
         let* α0 := output_result.["is_err"] in
         let* α1 :=
-          ink_env.backend_and_call_builder_and_error.ReturnFlags::["new_with_reverted"]
+          ink_env.backend_and_call_builder_and_engine_and_error.ReturnFlags::["new_with_reverted"]
             α0 in
         let* α2 := output_result.["map"] (fun _ => Pure tt) in
         let* α3 := ink_primitives.ConstructorResult::["Ok"] α2 in
@@ -3440,7 +3440,7 @@ Module
           else
             Pure tt in
         let* α0 :=
-          ink_env.backend_and_call_builder_and_error.ReturnFlags::["new_with_reverted"]
+          ink_env.backend_and_call_builder_and_engine_and_error.ReturnFlags::["new_with_reverted"]
             is_reverted in
         let* α1 := ink_primitives.MessageResult::["Ok"] result in
         ink_env.api.return_value α0 (addr_of α1)
@@ -3507,7 +3507,7 @@ Module
           else
             Pure tt in
         let* α0 :=
-          ink_env.backend_and_call_builder_and_error.ReturnFlags::["new_with_reverted"]
+          ink_env.backend_and_call_builder_and_engine_and_error.ReturnFlags::["new_with_reverted"]
             is_reverted in
         let* α1 := ink_primitives.MessageResult::["Ok"] result in
         ink_env.api.return_value α0 (addr_of α1)
@@ -3574,7 +3574,7 @@ Module
           else
             Pure tt in
         let* α0 :=
-          ink_env.backend_and_call_builder_and_error.ReturnFlags::["new_with_reverted"]
+          ink_env.backend_and_call_builder_and_engine_and_error.ReturnFlags::["new_with_reverted"]
             is_reverted in
         let* α1 := ink_primitives.MessageResult::["Ok"] result in
         ink_env.api.return_value α0 (addr_of α1)
@@ -3641,7 +3641,7 @@ Module
           else
             Pure tt in
         let* α0 :=
-          ink_env.backend_and_call_builder_and_error.ReturnFlags::["new_with_reverted"]
+          ink_env.backend_and_call_builder_and_engine_and_error.ReturnFlags::["new_with_reverted"]
             is_reverted in
         let* α1 := ink_primitives.MessageResult::["Ok"] result in
         ink_env.api.return_value α0 (addr_of α1)
@@ -3708,7 +3708,7 @@ Module
           else
             Pure tt in
         let* α0 :=
-          ink_env.backend_and_call_builder_and_error.ReturnFlags::["new_with_reverted"]
+          ink_env.backend_and_call_builder_and_engine_and_error.ReturnFlags::["new_with_reverted"]
             is_reverted in
         let* α1 := ink_primitives.MessageResult::["Ok"] result in
         ink_env.api.return_value α0 (addr_of α1)
@@ -3775,7 +3775,7 @@ Module
           else
             Pure tt in
         let* α0 :=
-          ink_env.backend_and_call_builder_and_error.ReturnFlags::["new_with_reverted"]
+          ink_env.backend_and_call_builder_and_engine_and_error.ReturnFlags::["new_with_reverted"]
             is_reverted in
         let* α1 := ink_primitives.MessageResult::["Ok"] result in
         ink_env.api.return_value α0 (addr_of α1)
@@ -4543,17 +4543,18 @@ Module Impl_erc20_erc20___CallBuilder_18.
       (self : ref Self)
       :
         M (H := H')
-          (ink_env.backend_and_call_builder_and_error.CallBuilder
+          (ink_env.backend_and_call_builder_and_engine_and_error.CallBuilder
             erc20.erc20.Environment
             (ink_env.call.common.Set_
-              (ink_env.backend_and_call_builder_and_error.Call
+              (ink_env.backend_and_call_builder_and_engine_and_error.Call
                 erc20.erc20.Environment))
             (ink_env.call.common.Set_
               (ink_env.call.execution_input.ExecutionInput
                 ink_env.call.execution_input.EmptyArgumentList))
             (ink_env.call.common.Set_
               (ink_env.call.common.ReturnType erc20.erc20.Balance))) :=
-    let* α0 := ink_env.backend_and_call_builder_and_error.build_call in
+    let* α0 :=
+      ink_env.backend_and_call_builder_and_engine_and_error.build_call in
     let* α1 := ink.contract_ref.ToAccountId.to_account_id self in
     let* α2 := α0.["call"] α1 in
     let* α3 := ink_env.call.selector.Selector::["new"] [ 219; 99; 117; 168 ] in
@@ -4572,10 +4573,10 @@ Module Impl_erc20_erc20___CallBuilder_18.
       (__ink_binding_0 : erc20.erc20.AccountId)
       :
         M (H := H')
-          (ink_env.backend_and_call_builder_and_error.CallBuilder
+          (ink_env.backend_and_call_builder_and_engine_and_error.CallBuilder
             erc20.erc20.Environment
             (ink_env.call.common.Set_
-              (ink_env.backend_and_call_builder_and_error.Call
+              (ink_env.backend_and_call_builder_and_engine_and_error.Call
                 erc20.erc20.Environment))
             (ink_env.call.common.Set_
               (ink_env.call.execution_input.ExecutionInput
@@ -4584,7 +4585,8 @@ Module Impl_erc20_erc20___CallBuilder_18.
                   ink_env.call.execution_input.EmptyArgumentList)))
             (ink_env.call.common.Set_
               (ink_env.call.common.ReturnType erc20.erc20.Balance))) :=
-    let* α0 := ink_env.backend_and_call_builder_and_error.build_call in
+    let* α0 :=
+      ink_env.backend_and_call_builder_and_engine_and_error.build_call in
     let* α1 := ink.contract_ref.ToAccountId.to_account_id self in
     let* α2 := α0.["call"] α1 in
     let* α3 := ink_env.call.selector.Selector::["new"] [ 15; 117; 90; 86 ] in
@@ -4605,10 +4607,10 @@ Module Impl_erc20_erc20___CallBuilder_18.
       (__ink_binding_1 : erc20.erc20.AccountId)
       :
         M (H := H')
-          (ink_env.backend_and_call_builder_and_error.CallBuilder
+          (ink_env.backend_and_call_builder_and_engine_and_error.CallBuilder
             erc20.erc20.Environment
             (ink_env.call.common.Set_
-              (ink_env.backend_and_call_builder_and_error.Call
+              (ink_env.backend_and_call_builder_and_engine_and_error.Call
                 erc20.erc20.Environment))
             (ink_env.call.common.Set_
               (ink_env.call.execution_input.ExecutionInput
@@ -4620,7 +4622,8 @@ Module Impl_erc20_erc20___CallBuilder_18.
                     ink_env.call.execution_input.EmptyArgumentList))))
             (ink_env.call.common.Set_
               (ink_env.call.common.ReturnType erc20.erc20.Balance))) :=
-    let* α0 := ink_env.backend_and_call_builder_and_error.build_call in
+    let* α0 :=
+      ink_env.backend_and_call_builder_and_engine_and_error.build_call in
     let* α1 := ink.contract_ref.ToAccountId.to_account_id self in
     let* α2 := α0.["call"] α1 in
     let* α3 := ink_env.call.selector.Selector::["new"] [ 106; 0; 22; 94 ] in
@@ -4642,10 +4645,10 @@ Module Impl_erc20_erc20___CallBuilder_18.
       (__ink_binding_1 : erc20.erc20.Balance)
       :
         M (H := H')
-          (ink_env.backend_and_call_builder_and_error.CallBuilder
+          (ink_env.backend_and_call_builder_and_engine_and_error.CallBuilder
             erc20.erc20.Environment
             (ink_env.call.common.Set_
-              (ink_env.backend_and_call_builder_and_error.Call
+              (ink_env.backend_and_call_builder_and_engine_and_error.Call
                 erc20.erc20.Environment))
             (ink_env.call.common.Set_
               (ink_env.call.execution_input.ExecutionInput
@@ -4657,7 +4660,8 @@ Module Impl_erc20_erc20___CallBuilder_18.
                     ink_env.call.execution_input.EmptyArgumentList))))
             (ink_env.call.common.Set_
               (ink_env.call.common.ReturnType (erc20.erc20.Result unit)))) :=
-    let* α0 := ink_env.backend_and_call_builder_and_error.build_call in
+    let* α0 :=
+      ink_env.backend_and_call_builder_and_engine_and_error.build_call in
     let* α1 := ink.contract_ref.ToAccountId.to_account_id self in
     let* α2 := α0.["call"] α1 in
     let* α3 := ink_env.call.selector.Selector::["new"] [ 132; 161; 93; 161 ] in
@@ -4679,10 +4683,10 @@ Module Impl_erc20_erc20___CallBuilder_18.
       (__ink_binding_1 : erc20.erc20.Balance)
       :
         M (H := H')
-          (ink_env.backend_and_call_builder_and_error.CallBuilder
+          (ink_env.backend_and_call_builder_and_engine_and_error.CallBuilder
             erc20.erc20.Environment
             (ink_env.call.common.Set_
-              (ink_env.backend_and_call_builder_and_error.Call
+              (ink_env.backend_and_call_builder_and_engine_and_error.Call
                 erc20.erc20.Environment))
             (ink_env.call.common.Set_
               (ink_env.call.execution_input.ExecutionInput
@@ -4694,7 +4698,8 @@ Module Impl_erc20_erc20___CallBuilder_18.
                     ink_env.call.execution_input.EmptyArgumentList))))
             (ink_env.call.common.Set_
               (ink_env.call.common.ReturnType (erc20.erc20.Result unit)))) :=
-    let* α0 := ink_env.backend_and_call_builder_and_error.build_call in
+    let* α0 :=
+      ink_env.backend_and_call_builder_and_engine_and_error.build_call in
     let* α1 := ink.contract_ref.ToAccountId.to_account_id self in
     let* α2 := α0.["call"] α1 in
     let* α3 := ink_env.call.selector.Selector::["new"] [ 104; 18; 102; 160 ] in
@@ -4717,10 +4722,10 @@ Module Impl_erc20_erc20___CallBuilder_18.
       (__ink_binding_2 : erc20.erc20.Balance)
       :
         M (H := H')
-          (ink_env.backend_and_call_builder_and_error.CallBuilder
+          (ink_env.backend_and_call_builder_and_engine_and_error.CallBuilder
             erc20.erc20.Environment
             (ink_env.call.common.Set_
-              (ink_env.backend_and_call_builder_and_error.Call
+              (ink_env.backend_and_call_builder_and_engine_and_error.Call
                 erc20.erc20.Environment))
             (ink_env.call.common.Set_
               (ink_env.call.execution_input.ExecutionInput
@@ -4735,7 +4740,8 @@ Module Impl_erc20_erc20___CallBuilder_18.
                       ink_env.call.execution_input.EmptyArgumentList)))))
             (ink_env.call.common.Set_
               (ink_env.call.common.ReturnType (erc20.erc20.Result unit)))) :=
-    let* α0 := ink_env.backend_and_call_builder_and_error.build_call in
+    let* α0 :=
+      ink_env.backend_and_call_builder_and_engine_and_error.build_call in
     let* α1 := ink.contract_ref.ToAccountId.to_account_id self in
     let* α2 := α0.["call"] α1 in
     let* α3 := ink_env.call.selector.Selector::["new"] [ 11; 57; 111; 24 ] in

diff --git a/CoqOfRust/ink/ink_e2e.v b/CoqOfRust/ink/ink_e2e.v
@@ -47,10 +47,10 @@ Parameter constructor_exec_input :
 
 Module client.
   Definition CallBuilderFinal (E Args RetType : Set) : Set :=
-    ink_env.backend_and_call_builder_and_error.CallBuilder
+    ink_env.backend_and_call_builder_and_engine_and_error.CallBuilder
       E
       (ink_env.call.common.Set_
-        (ink_env.backend_and_call_builder_and_error.Call E))
+        (ink_env.backend_and_call_builder_and_engine_and_error.Call E))
       (ink_env.call.common.Set_
         (ink_env.call.execution_input.ExecutionInput Args))
       (ink_env.call.common.Set_ (ink_env.call.common.ReturnType RetType)).
@@ -244,10 +244,10 @@ Module client.
 End client.
 
 Definition CallBuilderFinal (E Args RetType : Set) : Set :=
-  ink_env.backend_and_call_builder_and_error.CallBuilder
+  ink_env.backend_and_call_builder_and_engine_and_error.CallBuilder
     E
     (ink_env.call.common.Set_
-      (ink_env.backend_and_call_builder_and_error.Call E))
+      (ink_env.backend_and_call_builder_and_engine_and_error.Call E))
     (ink_env.call.common.Set_
       (ink_env.call.execution_input.ExecutionInput Args))
     (ink_env.call.common.Set_ (ink_env.call.common.ReturnType RetType)).