Host functions for the FxDAO test (#27)

* Implement `bytes_new_from_linear_memory`, `bytes_len` * Implement `get_current_contract_address` * Set Version: 0.1.22 * Add no-op implementation for `require_auth` * Implement `kasmer_create_contract` cheatcode * Generalize `<caller>` sort * Move `callContract` to `SOROBAN-SYNTAX` to make it available for hostfun modules * Implement `call` --------- Co-authored-by: devops <[email protected]>
runtimeverification · Aug 18, 2024 · b44523a · b44523a
1 parent d73500d
commit b44523a
Show file tree

Hide file tree

Showing 16 changed files with 993 additions and 10 deletions.
diff --git a/package/version b/package/version
@@ -1 +1 @@
-0.1.21
+0.1.22
diff --git a/pyproject.toml b/pyproject.toml
@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
 
 [tool.poetry]
 name = "ksoroban"
-version = "0.1.21"
+version = "0.1.22"
 description = "K tooling for the Soroban platform"
 authors = [
     "Runtime Verification, Inc. <[email protected]>",

diff --git a/src/ksoroban/kdist/soroban-semantics/cheatcodes.md b/src/ksoroban/kdist/soroban-semantics/cheatcodes.md
@@ -3,15 +3,25 @@
 
 ```k
 requires "host/hostfuns.md"
+requires "kasmer.md"
 
 module CHEATCODES
     imports HOSTFUNS
+    imports KASMER-SYNTAX-COMMON
 
     // TODO: Add a check to ensure these host functions are only called from a Kasmer test contract.
 
-    // extern "C" {
-    //     fn kasmer_set_ledger_sequence(x : u64);
-    // }
+```
+
+## kasmer_set_ledger_sequence
+
+```rust
+    extern "C" {
+        fn kasmer_set_ledger_sequence(x : u64);
+    }
+```
+
+```k
     rule [kasmer-set-ledger-sequence]:
         <instrs> hostCall ( "env" , "kasmer_set_ledger_sequence" , [ i64  .ValTypes ] -> [ .ValTypes ] )
               => toSmall(Void)
@@ -22,6 +32,49 @@ module CHEATCODES
         </locals>
         <ledgerSequenceNumber> _ => getMajor(HostVal(NEW_SEQ_NUM)) </ledgerSequenceNumber>
       requires getTag(HostVal(NEW_SEQ_NUM)) ==Int getTag(U32(0)) // check `NEW_SEQ_NUM` is a U32
+```
+
+## kasmer_create_contract
+
+```rust
+extern "C" {
+    fn kasmer_create_contract(addr_val: u64, hash_val: u64) -> u64;
+}
+
+fn create_contract(env: &Env, addr: &Bytes, hash: &Bytes) -> Address {
+    unsafe {
+        let res = kasmer_create_contract(addr.as_val().get_payload(), hash.as_val().get_payload());
+        Address::from_val(env, &Val::from_payload(res))
+    }
+}
+```
+
+```k
+    rule [kasmer-create-contract]:
+        <instrs> hostCall ( "env" , "kasmer_create_contract" , [ i64  i64  .ValTypes ] -> [ i64  .ValTypes ] )
+              => loadObject(HostVal(HASH))
+              ~> loadObject(HostVal(ADDR))
+              ~> kasmerCreateContract
+                 ...
+        </instrs>
+        <locals>
+          0 |-> < i64 > ADDR // ScBytes HostVal
+          1 |-> < i64 > HASH // ScBytes HostVal
+        </locals>
+
+    syntax InternalInstr ::= "kasmerCreateContract"   [symbol(kasmerCreateContract)]
+ // --------------------------------------------------------------------------------
+    rule [kasmerCreateContract]:
+        <instrs> kasmerCreateContract
+              => #waitCommands
+              ~> allocObject(ScAddress(Contract(ADDR)))
+              ~> returnHostVal
+                 ...
+        </instrs>
+        <k> (.K => deployContract(CONTRACT, Contract(ADDR), HASH)) ... </k>
+        <hostStack> ScBytes(ADDR) : ScBytes(HASH) : S => S </hostStack>
+        <callee> CONTRACT </callee>
+
 
 endmodule
 ```
diff --git a/src/ksoroban/kdist/soroban-semantics/configuration.md b/src/ksoroban/kdist/soroban-semantics/configuration.md
@@ -15,7 +15,7 @@ module CONFIG
         <host>
           <callState>
             <callee> Contract(.Bytes) </callee>
-            <caller> Account(.Bytes) </caller>
+            <caller> Account(.Bytes):Address </caller>
             <function> .WasmString </function>
             <args> .List </args>
             <wasm/>

diff --git a/src/ksoroban/kdist/soroban-semantics/data.md b/src/ksoroban/kdist/soroban-semantics/data.md
@@ -53,7 +53,7 @@ various contexts:
     syntax ScVal
       ::= SCBool(Bool)                             [symbol(SCVal:Bool)]
         | "Void"                                   [symbol(SCVal:Void)]
-        | Error(ErrorType, Int)                  [symbol(SCVal:Error)]
+        | Error(ErrorType, Int)                    [symbol(SCVal:Error)]
         | U32(Int)                                 [symbol(SCVal:U32)]
         | I32(Int)                                 [symbol(SCVal:I32)]
         | U64(Int)                                 [symbol(SCVal:U64)]
@@ -63,6 +63,7 @@ various contexts:
         | ScMap(Map)                               [symbol(SCVal:Map)]      // Map<ScVal, HostVal>
         | ScAddress(Address)                       [symbol(SCVal:Address)]
         | Symbol(String)                           [symbol(SCVal:Symbol)]
+        | ScBytes(Bytes)                           [symbol(SCVal:Bytes)]
 
     syntax Address ::= AccountId | ContractId
     syntax AccountId  ::= Account(Bytes)          [symbol(AccountId)]
@@ -158,7 +159,7 @@ module HOST-OBJECT
     rule getTag(ScAddress(_))  => 77
     rule getTag(Symbol(BS))    => 14    requires lengthString(BS) <=Int 9
     rule getTag(Symbol(BS))    => 74    requires lengthString(BS) >Int  9
-
+    rule getTag(ScBytes(_))    => 72
 
     // 64-bit integers that fit in 56 bits
     syntax Int ::= "#maxU64small"     [macro]

diff --git a/src/ksoroban/kdist/soroban-semantics/host/address.md b/src/ksoroban/kdist/soroban-semantics/host/address.md
@@ -0,0 +1,32 @@
+# ADDRESS
+
+```k
+requires "../configuration.md"
+requires "../switch.md"
+requires "../wasm-ops.md"
+requires "integer.md"
+
+module HOST-ADDRESS
+    imports CONFIG-OPERATIONS
+    imports WASM-OPERATIONS
+    imports HOST-INTEGER
+    imports SWITCH-SYNTAX
+
+```
+
+## require_auth
+
+```k
+    // TODO This is just a placeholder, as the auth system is out of scope for now.
+    // This function needs to be properly implemented to handle the authorization.
+    rule [hostfun-require-auth]:
+        <instrs> hostCall ( "a" , "0" , [ i64  .ValTypes ] -> [ i64  .ValTypes ] )
+              => toSmall(Void)
+                 ...
+        </instrs>
+        <locals>
+          0 |-> < i64 > _      // Address
+        </locals>
+
+endmodule
+```
diff --git a/src/ksoroban/kdist/soroban-semantics/host/buffer.md b/src/ksoroban/kdist/soroban-semantics/host/buffer.md
@@ -0,0 +1,69 @@
+# Buffer
+
+```k
+requires "../configuration.md"
+requires "../switch.md"
+requires "../wasm-ops.md"
+requires "integer.md"
+
+module HOST-BUFFER
+    imports CONFIG-OPERATIONS
+    imports WASM-OPERATIONS
+    imports HOST-INTEGER
+    imports SWITCH-SYNTAX
+
+```
+
+## bytes_new_from_linear_memory
+
+```k
+    rule [hostfun-bytes-new-from-linear-memory]:
+        <instrs> hostCall ( "b" , "3" , [ i64  i64  .ValTypes ] -> [ i64  .ValTypes ] )
+              => #memLoad(getMajor(HostVal(LM_POS)), getMajor(HostVal(LEN)))
+              ~> bytesNewFromLinearMemory
+                 ...
+        </instrs>
+        <locals>
+          0 |-> < i64 > LM_POS      // U32
+          1 |-> < i64 > LEN         // U32
+        </locals>
+      requires fromSmallValid(HostVal(LM_POS))
+       andBool fromSmallValid(HostVal(LEN))
+
+    syntax InternalInstr ::= "bytesNewFromLinearMemory"      [symbol(bytesNewFromLinearMemory)]
+ // ---------------------------------------------------------------------------------
+    rule [bytesNewFromLinearMemory]:
+        <instrs> bytesNewFromLinearMemory
+              => allocObject(ScBytes(BS))
+              ~> returnHostVal
+                 ...
+        </instrs>
+        <hostStack> BS:Bytes : S => S </hostStack>
+
+```
+
+## bytes_len
+
+```k
+
+    rule [hostfun-bytes-len]:
+        <instrs> hostCall ( "b" , "8" , [ i64  .ValTypes ] -> [ i64  .ValTypes ] )
+              => loadObject(HostVal(BYTES))
+              ~> bytesLen
+                 ...
+        </instrs>
+        <locals>
+          0 |-> < i64 > BYTES      // Bytes HostVal
+        </locals>
+
+    syntax InternalInstr ::= "bytesLen"      [symbol(bytesLen)]
+ // ---------------------------------------------------------------------------------
+    rule [bytesLen]:
+        <instrs> bytesLen
+              => toSmall(U32(lengthBytes(BS)))
+                 ...
+        </instrs>
+        <hostStack> ScBytes(BS) : S => S </hostStack>
+
+endmodule
+```
diff --git a/src/ksoroban/kdist/soroban-semantics/host/call.md b/src/ksoroban/kdist/soroban-semantics/host/call.md
@@ -0,0 +1,64 @@
+# Call
+
+```k
+requires "../configuration.md"
+requires "../switch.md"
+requires "../soroban.md"
+requires "integer.md"
+
+module HOST-CALL
+    imports CONFIG-OPERATIONS
+    imports SOROBAN-SYNTAX
+    imports HOST-INTEGER
+    imports SWITCH-SYNTAX
+
+```
+
+## call
+
+```k
+    // TODO Check reentry
+    rule [hostfun-require-auth]:
+        <instrs> hostCall ( "d" , "_" , [ i64  i64  i64  .ValTypes ] -> [ i64  .ValTypes ] )
+              => loadObject(HostVal(ARGS))
+              ~> loadObject(HostVal(FUNC))
+              ~> loadObject(HostVal(ADDR))
+              ~> call
+                 ...
+        </instrs>
+        <locals>
+          0 |-> < i64 > ADDR      // Address
+          1 |-> < i64 > FUNC      // Symbol
+          2 |-> < i64 > ARGS      // Vec
+        </locals>
+
+    syntax InternalInstr ::= "call"   [symbol(call)]
+ // ------------------------------------------
+    rule [call]:
+        <instrs> call
+              => #waitCommands
+              ~> returnCallResult
+                 ...
+        </instrs>
+        <hostStack> ScAddress(TO) : Symbol(FUNC) : ScVec(ARGS) : S => S </hostStack>
+        <callee> FROM </callee>
+        <k> (.K => callContract(FROM, TO, FUNC, ARGS)) ... </k>
+
+
+    syntax InternalInstr ::= "returnCallResult"   [symbol(returnCallResult)]
+ // ------------------------------------------------------------------------
+    rule [returnCallResult-error]:
+        <instrs> returnCallResult => trap ... </instrs>
+        <hostStack> Error(_,_) : _ </hostStack>
+    
+    rule [returnCallResult]:
+        <instrs> returnCallResult
+              => allocObject(RES)
+              ~> returnHostVal
+                 ...
+        </instrs>
+        <hostStack> RES:ScVal : S => S </hostStack>
+      [owise]
+
+endmodule
+```
diff --git a/src/ksoroban/kdist/soroban-semantics/host/context.md b/src/ksoroban/kdist/soroban-semantics/host/context.md
@@ -48,5 +48,19 @@ Return the current ledger sequence number as `U32`.
        andBool getTag(HostVal(ERR)) ==Int 3
        andBool Int2ErrorType(getMinor(HostVal(ERR))) =/=K ErrContract
 
+```
+
+## get_current_contract_address
+
+```k
+    rule [hostfun-get-current-contract-address]:
+        <instrs> hostCall ( "x" , "7" , [ .ValTypes ] -> [ i64  .ValTypes ] )
+              => allocObject(ScAddress(CONTRACT))
+              ~> returnHostVal
+                 ...
+        </instrs>
+        <locals> .Map </locals>
+        <callee> CONTRACT </callee>
+
 endmodule
 ```
diff --git a/src/ksoroban/kdist/soroban-semantics/host/hostfuns.md b/src/ksoroban/kdist/soroban-semantics/host/hostfuns.md
@@ -1,5 +1,8 @@
 
 ```k
+requires "address.md"
+requires "buffer.md"
+requires "call.md"
 requires "context.md"
 requires "integer.md"
 requires "ledger.md"
@@ -8,6 +11,9 @@ requires "symbol.md"
 requires "vector.md"
 
 module HOSTFUNS
+    imports HOST-ADDRESS
+    imports HOST-BUFFER
+    imports HOST-CALL
     imports HOST-CONTEXT
     imports HOST-INTEGER
     imports HOST-LEDGER

diff --git a/src/ksoroban/kdist/soroban-semantics/soroban.md b/src/ksoroban/kdist/soroban-semantics/soroban.md
@@ -6,6 +6,10 @@ requires "switch.md"
 requires "host/hostfuns.md"
 
 module SOROBAN-SYNTAX
+    imports HOST-OBJECT-SYNTAX
+
+    syntax InternalCmd ::= callContract ( Address, ContractId, String, List ) [symbol(callContractString), function, total]
+
 endmodule
 
 
@@ -20,8 +24,7 @@ module SOROBAN
 
 ```k
 
-    syntax InternalCmd ::= callContract    ( Address, ContractId, String,     List ) [symbol(callContractString), function, total]
-                         | callContract    ( Address, ContractId, WasmString, List ) [symbol(callContractWasmString)]
+    syntax InternalCmd ::= callContract    ( Address, ContractId, WasmString, List ) [symbol(callContractWasmString)]
                          | callContractAux ( Address, ContractId, WasmString, List ) [symbol(callContractAux)]
  // -------------------------------------------------------------------------------------
     rule callContract(FROM, TO, FUNCNAME:String, ARGS)