Skip to content

Commit 65b1576

Browse files
bbyalcinkayabbyalcinkaya
committed
implement math_mul_mod/math_div/math_mod/math_add_mod 
1 parent 528e64b commit 65b1576

1 file changed

Lines changed: 173 additions & 1 deletion

File tree

‎src/skribe/kdist/stylus-semantics/hostfuns.md‎

Lines changed: 173 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -11,6 +11,122 @@ module HOSTFUNS
1111
1212
syntax InternalInstr ::= hostCallAux(String, String) [symbol(hostCallAux)]
1313
14+
syntax InternalInstr ::= #memLoadWord( Int )
15+
// ---------------------------------------------
16+
rule <instrs> #memLoadWord(PTR) => #memLoad(PTR, 32) ~> #asWordFromStack ... </instrs>
17+
18+
```
19+
20+
## math_mul_mod
21+
22+
```k
23+
rule [hostCall-math-mul-mod]:
24+
<instrs> hostCall ( "vm_hooks" , "math_mul_mod" , [ i32 i32 i32 .ValTypes ] -> [ .ValTypes ] )
25+
=> pushStack(VALUE_PTR)
26+
~> #memLoadWord(MODULUS_PTR)
27+
~> #memLoadWord(MULTIPLIER_PTR)
28+
~> #memLoadWord(VALUE_PTR)
29+
~> hostCallAux ( "vm_hooks" , "math_mul_mod" )
30+
...
31+
</instrs>
32+
<locals>
33+
0 |-> < i32 > VALUE_PTR
34+
1 |-> < i32 > MULTIPLIER_PTR
35+
2 |-> < i32 > MODULUS_PTR
36+
</locals>
37+
<k> #endWasm ... </k>
38+
39+
rule [hostCallAux-math-mul-mod]:
40+
<instrs> hostCallAux ( "vm_hooks" , "math_mul_mod" )
41+
=> #memStore(RES_PTR, Int2Bytes(32, (VALUE *Int MULTIPLIER) %Word MODULUS, BE))
42+
...
43+
</instrs>
44+
<stylusStack> VALUE : MULTIPLIER : MODULUS : RES_PTR : S => S </stylusStack>
45+
<k> #endWasm ... </k>
46+
47+
```
48+
49+
## math_div
50+
51+
```k
52+
rule [hostCall-math-div]:
53+
<instrs> hostCall ( "vm_hooks" , "math_div" , [ i32 i32 .ValTypes ] -> [ .ValTypes ] )
54+
=> pushStack(A_PTR)
55+
~> #memLoadWord(B_PTR)
56+
~> #memLoadWord(A_PTR)
57+
~> hostCallAux ( "vm_hooks" , "math_div" )
58+
...
59+
</instrs>
60+
<locals>
61+
0 |-> < i32 > A_PTR
62+
1 |-> < i32 > B_PTR
63+
</locals>
64+
<k> #endWasm ... </k>
65+
66+
rule [hostCallAux-math-div]:
67+
<instrs> hostCallAux ( "vm_hooks" , "math_div" )
68+
=> #memStore(RES_PTR, Int2Bytes(32, A /Word B, BE))
69+
...
70+
</instrs>
71+
<stylusStack> A : B : RES_PTR : S => S </stylusStack>
72+
<k> #endWasm ... </k>
73+
74+
```
75+
76+
## math_mod
77+
78+
```k
79+
rule [hostCall-math-mod]:
80+
<instrs> hostCall ( "vm_hooks" , "math_mod" , [ i32 i32 .ValTypes ] -> [ .ValTypes ] )
81+
=> pushStack(A_PTR)
82+
~> #memLoadWord(B_PTR)
83+
~> #memLoadWord(A_PTR)
84+
~> hostCallAux ( "vm_hooks" , "math_mod" )
85+
...
86+
</instrs>
87+
<locals>
88+
0 |-> < i32 > A_PTR
89+
1 |-> < i32 > B_PTR
90+
</locals>
91+
<k> #endWasm ... </k>
92+
93+
rule [hostCallAux-math-mod]:
94+
<instrs> hostCallAux ( "vm_hooks" , "math_mod" )
95+
=> #memStore(RES_PTR, Int2Bytes(32, A %Word B, BE))
96+
...
97+
</instrs>
98+
<stylusStack> A : B : RES_PTR : S => S </stylusStack>
99+
<k> #endWasm ... </k>
100+
101+
```
102+
103+
## math_add_mod
104+
105+
```k
106+
rule [hostCall-math-add-mod]:
107+
<instrs> hostCall ( "vm_hooks" , "math_add_mod" , [ i32 i32 i32 .ValTypes ] -> [ .ValTypes ] )
108+
=> pushStack(W0_PTR)
109+
~> #memLoadWord(W2_PTR)
110+
~> #memLoadWord(W1_PTR)
111+
~> #memLoadWord(W0_PTR)
112+
~> hostCallAux ( "vm_hooks" , "math_add_mod" )
113+
...
114+
</instrs>
115+
<locals>
116+
0 |-> < i32 > W0_PTR
117+
1 |-> < i32 > W1_PTR
118+
2 |-> < i32 > W2_PTR
119+
</locals>
120+
<k> #endWasm ... </k>
121+
122+
rule [hostCallAux-math-add-mod]:
123+
<instrs> hostCallAux ( "vm_hooks" , "math_add_mod" )
124+
=> #memStore(RES_PTR, Int2Bytes(32, (W0 +Int W1) %Word W2, BE))
125+
...
126+
</instrs>
127+
<stylusStack> W0 : W1 : W2 : RES_PTR : S => S </stylusStack>
128+
<k> #endWasm ... </k>
129+
14130
```
15131

16132
## msg_reentrant
@@ -475,6 +591,50 @@ The semantics are equivalent to the `BALANCE` opcode.
475591
476592
```
477593

594+
## account_codehash
595+
596+
```k
597+
rule [hostCall-account-codehash]:
598+
<instrs> hostCall ( "vm_hooks" , "account_codehash" , [ i32 i32 .ValTypes ] -> [ .ValTypes ] )
599+
=> pushStack(DEST_PTR)
600+
~> #memLoad(ADDR_PTR, 20)
601+
~> #asWordFromStack
602+
~> hostCallAux ( "vm_hooks" , "account_codehash" )
603+
...
604+
</instrs>
605+
<locals>
606+
0 |-> < i32 > ADDR_PTR
607+
1 |-> < i32 > DEST_PTR
608+
</locals>
609+
<k> #endWasm ... </k>
610+
611+
rule [hostCallAux-account-codehash]:
612+
<instrs> hostCallAux ( "vm_hooks" , "account_codehash" )
613+
=> #memStore( DEST_PTR , Int2Bytes(32, keccak(CODE), BE) )
614+
~> #waitCommands
615+
...
616+
</instrs>
617+
<stylusStack> ACCT : DEST_PTR:Int : S => S </stylusStack>
618+
<account>
619+
<acctID> ACCT </acctID>
620+
<code> CODE </code>
621+
...
622+
</account>
623+
<k> (.K => #accessAccounts ACCT) ~> #endWasm ... </k>
624+
625+
626+
rule [hostCallAux-account-codehash-ow]:
627+
<instrs> hostCallAux ( "vm_hooks" , "account_codehash" )
628+
=> #memStore( DEST_PTR , Int2Bytes(32, 0, BE) )
629+
~> #waitCommands
630+
...
631+
</instrs>
632+
<stylusStack> ACCT : DEST_PTR:Int : S => S </stylusStack>
633+
<k> (.K => #accessAccounts ACCT) ~> #endWasm ... </k>
634+
[owise]
635+
```
636+
637+
478638
## block_number
479639

480640
```k
@@ -484,7 +644,7 @@ The semantics are equivalent to the `BALANCE` opcode.
484644
...
485645
</instrs>
486646
<locals> .Map </locals>
487-
<number> NUM </number>
647+
<number> NUM </number>
488648
<k> #endWasm ... </k>
489649
```
490650

@@ -573,6 +733,18 @@ The semantics are equivalent to the `BALANCE` opcode.
573733
574734
```
575735

736+
## emit_log
737+
738+
TODO: implement logs
739+
740+
```k
741+
rule [hostCall-emit-log]:
742+
<instrs> hostCall ( "vm_hooks" , "emit_log" , [ i32 i32 i32 .ValTypes ] -> [ .ValTypes ] )
743+
=> .K ...
744+
</instrs>
745+
<k> #endWasm ... </k>
746+
```
747+
576748
```k
577749
endmodule
578750
```

0 commit comments

Comments
 (0)