@@ -15,41 +15,41 @@ module KASMER
1515
1616``` k
1717 configuration
18- <foundry >
18+ <kasmer >
1919 <mandos/>
2020 <wasmStore> .Map </wasmStore> // file path -> wasm module AST
2121 <prank> false </prank>
22- </foundry >
22+ </kasmer >
2323
24- syntax Bytes ::= "#foundryRunner " [macro]
24+ syntax Bytes ::= "#kasmerRunner " [macro]
2525 // --------------------------------------------------------
26- rule #foundryRunner
26+ rule #kasmerRunner
2727 => b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00k-test________________"
2828```
2929
30- ## Foundry Host Functions
30+ ## Kasmer Host Functions
3131
32- Only the ` #foundryRunner ` account can execute these commands/host functions.
32+ Only the ` #kasmerRunner ` account can execute these commands/host functions.
3333
3434### Create account
3535
3636``` k
3737 rule [testapi-createAccount]:
3838 <instrs> hostCall ( "env" , "createAccount" , [ i32 i64 i32 .ValTypes ] -> [ .ValTypes ] )
39- => foundryCreateAccount ( getBuffer(ADDR_HANDLE), NONCE, getBigInt(BALANCE_HANDLE))
39+ => kasmerCreateAccount ( getBuffer(ADDR_HANDLE), NONCE, getBigInt(BALANCE_HANDLE))
4040 ...
4141 </instrs>
4242 <locals>
4343 0 |-> <i32> ADDR_HANDLE
4444 1 |-> <i64> NONCE
4545 2 |-> <i32> BALANCE_HANDLE
4646 </locals>
47- <callee> #foundryRunner </callee>
47+ <callee> #kasmerRunner </callee>
4848
49- syntax InternalInstr ::= foundryCreateAccount (BytesResult, Int, IntResult)
49+ syntax InternalInstr ::= kasmerCreateAccount (BytesResult, Int, IntResult)
5050 // ----------------------------------------------------------------------------
51- rule [foundryCreateAccount ]:
52- <instrs> foundryCreateAccount (ADDR:Bytes, NONCE, BALANCE:Int)
51+ rule [kasmerCreateAccount ]:
52+ <instrs> kasmerCreateAccount (ADDR:Bytes, NONCE, BALANCE:Int)
5353 => #waitCommands
5454 ...
5555 </instrs>
@@ -58,8 +58,8 @@ Only the `#foundryRunner` account can execute these commands/host functions.
5858 ) ...
5959 </commands>
6060
61- rule [foundryCreateAccount -err]:
62- <instrs> foundryCreateAccount (_, _, _)
61+ rule [kasmerCreateAccount -err]:
62+ <instrs> kasmerCreateAccount (_, _, _)
6363 => #throwException(ExecutionFailed, "Could not create account")
6464 ...
6565 </instrs>
@@ -72,26 +72,26 @@ Only the `#foundryRunner` account can execute these commands/host functions.
7272``` k
7373 rule [testapi-registerNewAddress]:
7474 <instrs> hostCall ( "env" , "registerNewAddress" , [ i32 i64 i32 .ValTypes ] -> [ .ValTypes ] )
75- => foundryRegisterNewAddress ( getBuffer(OWNER_HANDLE), NONCE, getBuffer(ADDR_HANDLE))
75+ => kasmerRegisterNewAddress ( getBuffer(OWNER_HANDLE), NONCE, getBuffer(ADDR_HANDLE))
7676 ...
7777 </instrs>
7878 <locals>
7979 0 |-> <i32> OWNER_HANDLE
8080 1 |-> <i64> NONCE
8181 2 |-> <i32> ADDR_HANDLE
8282 </locals>
83- <callee> #foundryRunner </callee>
83+ <callee> #kasmerRunner </callee>
8484
85- syntax InternalInstr ::= foundryRegisterNewAddress (BytesResult, Int, BytesResult)
85+ syntax InternalInstr ::= kasmerRegisterNewAddress (BytesResult, Int, BytesResult)
8686 // ----------------------------------------------------------------------------
87- rule [foundryRegisterNewAddress ]:
88- <instrs> foundryRegisterNewAddress (CREATOR:Bytes, NONCE, NEW:Bytes)
87+ rule [kasmerRegisterNewAddress ]:
88+ <instrs> kasmerRegisterNewAddress (CREATOR:Bytes, NONCE, NEW:Bytes)
8989 => .K ...
9090 </instrs>
9191 <newAddresses> NEWADDRESSES => NEWADDRESSES [tuple(CREATOR, NONCE) <- NEW] </newAddresses>
9292
93- rule [foundryRegisterNewAddress -err]:
94- <instrs> foundryRegisterNewAddress (_, _, _)
93+ rule [kasmerRegisterNewAddress -err]:
94+ <instrs> kasmerRegisterNewAddress (_, _, _)
9595 => #throwException(ExecutionFailed, "Could not register address") ...
9696 </instrs>
9797 [owise]
@@ -103,7 +103,7 @@ Only the `#foundryRunner` account can execute these commands/host functions.
103103``` k
104104 rule [testapi-deployContract]:
105105 <instrs> hostCall("env", "deployContract", [i32 i64 i32 i32 i32 i32 .ValTypes] -> [.ValTypes])
106- => foundryDeployContract (
106+ => kasmerDeployContract (
107107 getBuffer(OWNER_HANDLE),
108108 GAS_LIMIT,
109109 getBigInt(VALUE_HANDLE),
@@ -121,12 +121,12 @@ Only the `#foundryRunner` account can execute these commands/host functions.
121121 4 |-> <i32> ARGS_HANDLE
122122 5 |-> <i32> RESULT_ADDR_HANDLE
123123 </locals>
124- <callee> #foundryRunner </callee>
124+ <callee> #kasmerRunner </callee>
125125
126- syntax InternalInstr ::= foundryDeployContract (BytesResult, Int, IntResult, BytesResult, ListBytesResult, Int)
126+ syntax InternalInstr ::= kasmerDeployContract (BytesResult, Int, IntResult, BytesResult, ListBytesResult, Int)
127127 // ----------------------------------------------------------------------------
128- rule [foundryDeployContract ]:
129- <instrs> foundryDeployContract (OWNER:Bytes, GAS, VALUE:Int, PATH:Bytes, ARGS:ListBytes, RESULT_ADDR_HANDLE)
128+ rule [kasmerDeployContract ]:
129+ <instrs> kasmerDeployContract (OWNER:Bytes, GAS, VALUE:Int, PATH:Bytes, ARGS:ListBytes, RESULT_ADDR_HANDLE)
130130 => #waitCommands
131131 ~> #setBuffer(RESULT_ADDR_HANDLE, NEWADDR)
132132 ...
@@ -147,8 +147,8 @@ Only the `#foundryRunner` account can execute these commands/host functions.
147147 <newAddresses> ... tuple(OWNER, NONCE) |-> NEWADDR:Bytes ... </newAddresses>
148148 <wasmStore> ... PATH |-> MODULE </wasmStore>
149149
150- rule [foundryDeployContract -err]:
151- <instrs> foundryDeployContract (_, _, _, _, _, _)
150+ rule [kasmerDeployContract -err]:
151+ <instrs> kasmerDeployContract (_, _, _, _, _, _)
152152 => #throwException(ExecutionFailed, "Could not deploy contract")
153153 ...
154154 </instrs>
@@ -173,14 +173,14 @@ Only the `#foundryRunner` account can execute these commands/host functions.
173173 1 |-> <i32> KEY_HANDLE
174174 2 |-> <i32> DEST_HANDLE
175175 </locals>
176- <callee> #foundryRunner </callee>
176+ <callee> #kasmerRunner </callee>
177177
178178 rule [testapi-setStorage]:
179179 <instrs> hostCall ( "env" , "setStorage" , [ i32 i32 i32 .ValTypes ] -> [ .ValTypes ] )
180180 => #getBuffer(VAL_HANDLE)
181181 ~> #getBuffer(KEY_HANDLE)
182182 ~> #getBuffer(ADDR_HANDLE)
183- ~> foundryWriteToStorage
183+ ~> kasmerWriteToStorage
184184 ~> #dropBytes
185185 ~> #dropBytes
186186 ~> #dropBytes
@@ -191,12 +191,12 @@ Only the `#foundryRunner` account can execute these commands/host functions.
191191 1 |-> <i32> KEY_HANDLE
192192 2 |-> <i32> VAL_HANDLE
193193 </locals>
194- <callee> #foundryRunner </callee>
194+ <callee> #kasmerRunner </callee>
195195
196- syntax InternalInstr ::= "foundryWriteToStorage "
196+ syntax InternalInstr ::= "kasmerWriteToStorage "
197197 // -------------------------------------------------
198- rule [foundryWriteToStorage -empty]:
199- <instrs> foundryWriteToStorage => .K ... </instrs>
198+ rule [kasmerWriteToStorage -empty]:
199+ <instrs> kasmerWriteToStorage => .K ... </instrs>
200200 <bytesStack> ADDR : KEY : VALUE : _ </bytesStack>
201201 <account>
202202 <address> ADDR </address>
@@ -206,8 +206,8 @@ Only the `#foundryRunner` account can execute these commands/host functions.
206206 requires VALUE ==K .Bytes
207207 [preserves-definedness] // ADDR exists prior in account map
208208
209- rule [foundryWriteToStorage ]:
210- <instrs> foundryWriteToStorage => .K ... </instrs>
209+ rule [kasmerWriteToStorage ]:
210+ <instrs> kasmerWriteToStorage => .K ... </instrs>
211211 <bytesStack> ADDR : KEY : VALUE : _ </bytesStack>
212212 <account>
213213 <address> ADDR </address>
@@ -231,7 +231,7 @@ Only the `#foundryRunner` account can execute these commands/host functions.
231231 0 |-> <i32> ADDR_HANDLE
232232 1 |-> <i32> VAL_HANDLE
233233 </locals>
234- <callee> #foundryRunner </callee>
234+ <callee> #kasmerRunner </callee>
235235
236236 syntax InternalInstr ::= #setBalance(BytesResult, IntResult)
237237 // ------------------------------------------------------------
@@ -291,7 +291,7 @@ Only the `#foundryRunner` account can execute these commands/host functions.
291291 1 |-> <i32> TOK_ID_HANDLE
292292 2 |-> <i32> VAL_HANDLE
293293 </locals>
294- <callee> #foundryRunner </callee>
294+ <callee> #kasmerRunner </callee>
295295
296296
297297 syntax InternalInstr ::= #setESDTBalance(IntResult)
@@ -514,7 +514,7 @@ Only the `#foundryRunner` account can execute these commands/host functions.
514514 => S +String " -- setBlockTimestamp "
515515 +String Int2String(TIMESTAMP)
516516 </logging>
517- <callee> #foundryRunner </callee>
517+ <callee> #kasmerRunner </callee>
518518
519519```
520520
@@ -529,13 +529,13 @@ Only the `#foundryRunner` account can execute these commands/host functions.
529529 0 |-> <i32> P
530530 </locals>
531531
532- syntax InternalInstr ::= #assert(Int) [symbol, klabel(foundryAssert )]
532+ syntax InternalInstr ::= #assert(Int) [symbol, klabel(kasmerAssert )]
533533 // -------------------------------------------------------------------------
534- rule [foundryAssert -true]:
534+ rule [kasmerAssert -true]:
535535 <instrs> #assert( I ) => .K ... </instrs>
536536 requires I =/=Int 0
537537
538- rule [foundryAssert -false]:
538+ rule [kasmerAssert -false]:
539539 <instrs> #assert( I )
540540 => #throwException(ExecutionFailed, "assertion failed") ...
541541 </instrs>
@@ -550,13 +550,13 @@ Only the `#foundryRunner` account can execute these commands/host functions.
550550 0 |-> <i32> P
551551 </locals>
552552
553- syntax IternalInstr ::= #assume(Int) [symbol, klabel(foundryAssume )]
553+ syntax IternalInstr ::= #assume(Int) [symbol, klabel(kasmerAssume )]
554554 // ------------------------------------------------------------------------
555- rule [foundryAssume -true]:
555+ rule [kasmerAssume -true]:
556556 <instrs> #assume(P) => .K ... </instrs>
557557 requires P =/=Int 0
558558
559- rule [foundryAssume -false]:
559+ rule [kasmerAssume -false]:
560560 <instrs> #assume(P) => #endFoundryImmediately ... </instrs>
561561 requires P ==Int 0
562562
@@ -593,13 +593,13 @@ Only the `#foundryRunner` account can execute these commands/host functions.
593593 <locals>
594594 0 |-> <i32> ADDR_HANDLE
595595 </locals>
596- <callee> #foundryRunner </callee>
596+ <callee> #kasmerRunner </callee>
597597
598598 syntax InternalInstr ::= #startPrank(BytesResult)
599599 // -------------------------------------------------
600600 rule [startPrank]:
601601 <instrs> #startPrank(ADDR:Bytes) => .K ... </instrs>
602- <callee> #foundryRunner => ADDR </callee>
602+ <callee> #kasmerRunner => ADDR </callee>
603603 <prank> false => true </prank>
604604
605605 rule [startPrank-not-allowed]:
@@ -609,7 +609,7 @@ Only the `#foundryRunner` account can execute these commands/host functions.
609609 </instrs>
610610 <callee> ADDR </callee>
611611 <prank> PRANK </prank>
612- requires ADDR =/=K #foundryRunner
612+ requires ADDR =/=K #kasmerRunner
613613 orBool PRANK
614614
615615 rule [startPrank-err]:
@@ -623,7 +623,7 @@ Only the `#foundryRunner` account can execute these commands/host functions.
623623 => .K ...
624624 </instrs>
625625 <locals> .Map </locals>
626- <callee> _ => #foundryRunner </callee>
626+ <callee> _ => #kasmerRunner </callee>
627627 <prank> true => false </prank>
628628
629629 rule [testapi-stopPrank-err]:
0 commit comments