Initial semantics (#10)

* initial semantics

* change kdist target

* add ksoroban executable

* add integration tests

* Set Version: 0.1.6

* refactor

* add minor comments

* fox program name in argument parser

---------

Co-authored-by: devops <[email protected]>

package/version

@@ -1 +1 @@
-0.1.5
+0.1.6

pyproject.toml

@@ -4,12 +4,15 @@ build-backend = "poetry.core.masonry.api"
 
 [tool.poetry]
 name = "ksoroban"
-version = "0.1.5"
+version = "0.1.6"
 description = "K tooling for the Soroban platform"
 authors = [
     "Runtime Verification, Inc. <[email protected]>",
 ]
 
+[tool.poetry.scripts]
+ksoroban = "ksoroban.ksoroban:main"
+
 [tool.poetry.plugins.kdist]
 soroban-semantics = "ksoroban.kdist.plugin"
 

src/ksoroban/kdist/plugin.py

@@ -48,8 +48,8 @@ def deps(self) -> tuple[str]:
     'source': SourceTarget(),
     'llvm': KompileTarget(
         lambda src_dir: {
-            'main_file': src_dir / 'soroban-semantics/soroban.md',
-            'syntax_module': 'SOROBAN',
+            'main_file': src_dir / 'soroban-semantics/kasmer.md',
+            'syntax_module': 'KASMER-SYNTAX',
             'include_dirs': [src_dir],
             'md_selector': 'k',
             'warnings_to_errors': True,

src/ksoroban/kdist/soroban-semantics/auto-allocate.md

@@ -0,0 +1,84 @@
+Auto Allocate Host Modules
+==========================
+
+When `AUTO-ALLOCATE` is imported, an new module will be automatically created and registered whenever necessary to resolve an import.
+This makes it possible to implement host modules easily in K.
+Accessing the import will result in an instruction being left on the `instrs` cell that can't be resolved in the regular Wasm semantics.
+Instead, the embedder can add rules for handling the host import.
+
+Currently, only function imports are supported.
+Calling an imported host function will result in `hostCall(MODULE_NAME, FUNCTION_NAME, FUNCTION_TYPE)` being left on the `instrs` cell.
+
+```k
+requires "wasm-semantics/wasm-text.md"
+
+module WASM-AUTO-ALLOCATE
+    imports WASM-DATA-TOOLS
+    imports WASM-TEXT
+
+    syntax Stmt ::= "newEmptyModule" WasmString
+ // -------------------------------------------
+    rule <instrs> newEmptyModule MODNAME => .K ... </instrs>
+         <moduleRegistry> MR => MR [ MODNAME <- NEXT ] </moduleRegistry>
+         <nextModuleIdx> NEXT => NEXT +Int 1 </nextModuleIdx>
+         <moduleInstances> ( .Bag => <moduleInst> <modIdx> NEXT </modIdx> ... </moduleInst>) ... </moduleInstances>
+
+    syntax Stmts ::=  autoAllocModules ( ModuleDecl, Map ) [function]
+                   | #autoAllocModules ( Defns     , Map ) [function]
+ // -----------------------------------------------------------------
+    rule  autoAllocModules(#module(... importDefns:IS), MR) => #autoAllocModules(IS, MR)
+```
+
+In helper function `#autoAllocModules`, the module registry map is passed along to check if the module being imported from is present.
+It is treated purely as a key set -- the actual stored values are not used or stored anywhere.
+
+```k
+    rule #autoAllocModules(.Defns, _) => .Stmts
+    rule #autoAllocModules((#import(MOD, _, _) DS) => DS, MR) requires MOD in_keys(MR)
+    rule #autoAllocModules((#import(MOD, _, _) DS), MR)
+      => newEmptyModule MOD #autoAllocModules(DS, MR [MOD <- -1])
+      requires notBool MOD in_keys(MR)
+
+    rule <instrs> MD:ModuleDecl
+               => sequenceStmts(autoAllocModules(MD, MR))
+               ~> MD
+              ...
+         </instrs>
+         <moduleRegistry> MR </moduleRegistry>
+      requires autoAllocModules(MD, MR) =/=K .Stmts
+      [priority(10)]
+
+    syntax Instr ::= hostCall(String, String, FuncType)
+ // ---------------------------------------------------
+    rule <instrs> (.K => allocfunc(HOSTMOD, NEXTADDR, TYPE, [ .ValTypes ], hostCall(wasmString2StringStripped(MOD), wasmString2StringStripped(NAME), TYPE) .Instrs, #meta(... id: String2Identifier("$auto-alloc:" +String #parseWasmString(MOD) +String ":" +String #parseWasmString(NAME) ), localIds: .Map )))
+               ~> #import(MOD, NAME, #funcDesc(... type: TIDX))
+              ...
+         </instrs>
+         <curModIdx> CUR </curModIdx>
+         <moduleInst>
+           <modIdx> CUR </modIdx>
+           <types> ... TIDX |-> TYPE ... </types>
+           ...
+        </moduleInst>
+        <nextFuncAddr> NEXTADDR => NEXTADDR +Int 1 </nextFuncAddr>
+        <moduleRegistry> ... MOD |-> HOSTMOD ... </moduleRegistry>
+        <moduleInst>
+          <modIdx> HOSTMOD </modIdx>
+          <exports> EXPORTS => EXPORTS [NAME <- NEXTFUNC ] </exports>
+          <funcAddrs> FS => setExtend(FS, NEXTFUNC, NEXTADDR, -1) </funcAddrs>
+          <nextFuncIdx> NEXTFUNC => NEXTFUNC +Int 1 </nextFuncIdx>
+          <nextTypeIdx> NEXTTYPE => NEXTTYPE +Int 1 </nextTypeIdx>
+          <types> TYPES => TYPES [ NEXTTYPE <- TYPE ] </types>
+          ...
+        </moduleInst>
+      requires notBool NAME in_keys(EXPORTS)
+
+    syntax String ::= wasmString2StringStripped ( WasmString ) [function]
+                    | #stripQuotes ( String ) [function]
+ // ----------------------------------------------------
+    rule wasmString2StringStripped(WS) => #stripQuotes(#parseWasmString(WS))
+
+    rule #stripQuotes(S) => replaceAll(S, "\"", "")
+
+endmodule
+```

src/ksoroban/kdist/soroban-semantics/configuration.md

@@ -0,0 +1,268 @@
+
+```k
+requires "auto-allocate.md"
+requires "wasm-semantics/wasm.md"
+requires "data.md"
+
+module CONFIG
+    imports HOST-OBJECT
+    imports MAP
+    imports WASM
+
+    configuration
+      <soroban>
+        <k> .K </k>
+        <host>
+          <callState>
+            <callee> Contract(.Bytes) </callee>
+            <caller> Account(.Bytes) </caller>
+            <function> .WasmString </function>
+            <args> .List </args>
+            <wasm/>
+            <relativeObjects> .List </relativeObjects> // List of HostVals with absolute handles to host objects
+            <contractModIdx> .Int </contractModIdx>
+          </callState>
+          <hostStack> .HostStack </hostStack>
+          <hostObjects> .List </hostObjects> // List of ScVals
+          <callStack> .List </callStack>
+          <interimStates> .List </interimStates>
+        </host>  
+
+        <contracts>
+          <contract multiplicity="*" type="Map">
+            <contractId> Contract(.Bytes) </contractId>
+            <wasmHash> .Bytes </wasmHash>
+            <instanceStorage> .Map </instanceStorage>
+          </contract>
+        </contracts>
+        <accounts>
+          <account multiplicity="*" type="Map">
+            <accountId> Account(.Bytes) </accountId>
+            <balance> 0 </balance>
+          </account>
+        </accounts>
+        <contractCodes> .Map </contractCodes>
+        <logging> .List </logging>
+      </soroban>
+
+    syntax HostStack ::= List{HostStackVal, ":"}  [symbol(hostStackList)]
+    syntax HostStackVal ::= ScVal | HostVal
+
+
+    syntax InternalCmd ::= #callResult(ValStack, List)   [symbol(#callResult)]
+
+endmodule
+```
+
+
+```k
+module CONFIG-OPERATIONS
+    imports WASM-AUTO-ALLOCATE
+    imports CONFIG
+    imports SWITCH-SYNTAX
+```
+
+## Stack operations
+
+```k
+    syntax InternalCmd ::= pushStack(HostStackVal)    [symbol(pushStack)]
+ // ---------------------------------------------------------------------
+    rule [pushStack]:
+        <k> pushStack(V) => .K ... </k>
+        <hostStack> S => V : S </hostStack>
+
+    syntax InternalCmd ::= "dropStack"    [symbol(dropStack)]
+ // ---------------------------------------------------------------------
+    rule [dropStack]:
+        <k> dropStack => .K ... </k>
+        <hostStack> _V : S => S </hostStack>
+
+```
+
+## Call State
+
+The `<callStack>` cell stores a list of previous contract execution states. 
+These internal commands manages the call stack when calling and returning from a contract.
+
+```k
+    syntax InternalCmd ::= "pushCallState"  [symbol(pushCallState)]
+ // ---------------------------------------
+    rule [pushCallState]:
+         <k> pushCallState => .K ... </k>
+         <callStack> (.List => ListItem(CALLSTATE)) ... </callStack>
+         CALLSTATE:CallStateCell
+      [priority(60)]
+
+    syntax InternalCmd ::= "popCallState"  [symbol(popCallState)]
+ // --------------------------------------
+    rule [popCallState]:
+         <k> popCallState => .K ... </k>
+         <callStack> (ListItem(CALLSTATE:CallStateCell) => .List) ... </callStack>
+         (_:CallStateCell => CALLSTATE)
+      [priority(60)]
+
+    syntax InternalCmd ::= "dropCallState"  [symbol(dropCallState)]
+ // ---------------------------------------
+    rule [dropCallState]:
+         <k> dropCallState => .K ... </k>
+         <callStack> (ListItem(_) => .List) ... </callStack>
+      [priority(60)]
+
+    syntax InternalCmd ::= "resetCallstate"      [symbol(resetCallState)]
+ // ---------------------------------------------------------------------------
+    rule [resetCallstate]:
+        <k> resetCallstate => .K ... </k>
+        (_:CallStateCell => <callState> <instrs> .K </instrs> ... </callState>)
+      [preserves-definedness] // all constant configuration cells should be defined
+
+```
+
+## World State
+
+```k
+    syntax AccountsCellFragment
+    syntax ContractsCellFragment
+
+    syntax Accounts ::= "{" AccountsCellFragment "," ContractsCellFragment "}"
+ // --------------------------------------------------------
+
+    syntax InternalCmd ::= "pushWorldState"  [symbol(pushWorldState)]
+ // ---------------------------------------
+    rule [pushWorldState]:
+         <k> pushWorldState => .K ... </k>
+         <interimStates> (.List => ListItem({ ACCTDATA , CONTRACTS })) ... </interimStates>
+         <contracts> CONTRACTS </contracts>
+         <accounts> ACCTDATA </accounts>
+      [priority(60)]
+
+    syntax InternalCmd ::= "popWorldState"  [symbol(popWorldState)]
+ // --------------------------------------
+    rule [popWorldState]:
+         <k> popWorldState => .K ... </k>
+         <interimStates> (ListItem({ ACCTDATA , CONTRACTS }) => .List) ... </interimStates>
+         <contracts> _ =>  CONTRACTS </contracts>
+         <accounts> _ => ACCTDATA </accounts>
+      [priority(60)]
+
+    syntax InternalCmd ::= "dropWorldState"  [symbol(dropWorldState)]
+ // ---------------------------------------
+    rule [dropWorldState]:
+         <k> dropWorldState => .K ... </k>
+         <interimStates> (ListItem(_) => .List) ... </interimStates>
+      [priority(60)]
+```
+
+## `ScVal` Operations
+
+```k
+    syntax InternalCmd ::= allocObject(ScVal)             [symbol(allocObject)]
+ // ---------------------------------------------------------------------------
+    rule [allocObject-small]:
+        <k> allocObject(SCV) => .K ... </k>
+        <hostStack> STACK => toSmall(SCV) : STACK </hostStack>
+      requires toSmallValid(SCV)
+
+    rule [allocObject]:
+        <k> allocObject(SCV) => .K ... </k>
+        <hostObjects> OBJS => OBJS ListItem(SCV) </hostObjects>
+        <hostStack> STACK => fromHandleAndTag(indexToHandle(size(OBJS), false), getTag(SCV)) : STACK </hostStack>
+      [owise]
+
+    syntax InternalCmd ::= allocObjects       (List)       [symbol(allocObjects)]
+                         | allocObjectsAux    (List)       [symbol(allocObjectsAux)]
+                         | allocObjectsCollect(Int)        [symbol(allocObjectsCollect)]
+ // ---------------------------------------------------------------------------
+    rule [allocObjects]:
+        <k> allocObjects(L) => allocObjectsAux(L) ~> allocObjectsCollect(size(L))  ... </k>
+
+    rule [allocObjectsAux-empty]:
+        <k> allocObjectsAux(.List) => .K ... </k>
+
+    rule [allocObjectsAux]:
+        <k> allocObjectsAux(ListItem(SCV:ScVal) L) 
+         => allocObjectsAux(L)
+         ~> allocObject(SCV)
+            ...
+        </k>
+
+    rule [allocObjectsCollect]:
+        <k> allocObjectsCollect(LENGTH) => .K ... </k> 
+        <hostStack> STACK => ScVec(take(LENGTH, STACK)) : drop(LENGTH, STACK) </hostStack>
+
+    syntax HostStack ::= drop(Int, HostStack)   [function, total, symbol(HostStack:drop)]
+ // -------------------------------------------------------------------------------------
+    rule drop(N, _ : S) => drop(N -Int 1, S)                requires N >Int 0
+    rule drop(_,     S) => S                                [owise]
+    
+    syntax List ::= take(Int, HostStack)        [function, total, symbol(HostStack:take)]
+ // -------------------------------------------------------------------------------------
+    rule take(N, X : S) => ListItem(X) take(N -Int 1, S)    requires N >Int 0
+    rule take(_,     _) => .List                            [owise]
+
+    syntax InternalInstr ::= loadObject(HostVal)    [symbol(loadObject)]
+ // --------------------------------------------------------------------
+    rule [loadObject-abs]:
+        <instrs> loadObject(VAL) => .K ... </instrs>
+        <hostStack> S => OBJS {{ getIndex(VAL) }} orDefault Void : S </hostStack>
+        <hostObjects> OBJS </hostObjects>
+      requires isObject(VAL)
+       andBool notBool isRelativeObjectHandle(VAL)
+       andBool 0 <=Int getIndex(VAL)
+       andBool getIndex(VAL) <Int size(OBJS)
+
+    rule [loadObject-rel]:
+        <instrs> loadObject(VAL) 
+              => loadObject(RELS {{ getIndex(VAL) }} orDefault HostVal(0))
+                 ...
+        </instrs>
+        <relativeObjects> RELS </relativeObjects>
+      requires isObject(VAL)
+       andBool isRelativeObjectHandle(VAL)
+       andBool 0 <=Int getIndex(VAL)
+       andBool getIndex(VAL) <Int size(RELS)
+```
+
+## Call result handling
+
+```k
+    rule [callResult-empty]:
+        <k> #callResult(.ValStack, _RELS) => .K ... </k>
+    
+    rule [callResult]:
+        <k> #callResult(<i64> I : SS, RELS)
+         => #callResult(SS, RELS)
+         ~> HostVal2ScVal(HostVal(I), RELS)
+            ...
+        </k>
+    
+    syntax InternalCmd ::= HostVal2ScVal(HostVal, List)      [symbol(HostVal2ScVal)]
+ // --------------------------------------------------------------------------
+    rule [HostVal2ScVal-obj-abs]:
+        <k> HostVal2ScVal(VAL, _RELS) => .K ... </k>
+        <hostObjects> OBJS </hostObjects>
+        <hostStack> S => OBJS {{ getIndex(VAL) }} orDefault Void : S </hostStack>
+      requires isObject(VAL)
+       andBool notBool(isRelativeObjectHandle(VAL))
+       andBool getIndex(VAL) <Int size(OBJS)
+
+    rule [HostVal2ScVal-obj-rel]:
+        <k> HostVal2ScVal(VAL, RELS)
+         => HostVal2ScVal(RELS {{ getIndex(VAL) }} orDefault HostVal(0), RELS)
+            ...
+        </k>
+      requires isObject(VAL)
+       andBool isRelativeObjectHandle(VAL)
+       andBool getIndex(VAL) <Int size(RELS)
+      [preserves-definedness]
+
+    rule [HostVal2ScVal-small]:
+        <k> HostVal2ScVal(VAL, _RELS) => .K ... </k>
+        <hostStack> S => fromSmall(VAL) : S </hostStack>
+      requires notBool isObject(VAL)
+       andBool fromSmallValid(VAL)
+
+```
+
+```k
+endmodule
+```