Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged rules #116

Draft
wants to merge 13 commits into
base: master
Choose a base branch
from
180 changes: 180 additions & 0 deletions kwasm-polkadot-host.md
Original file line number Diff line number Diff line change
Expand Up @@ -16,6 +16,7 @@ module KWASM-POLKADOT-HOST
imports K-IO
imports WASM-TEST
imports KWASM-LEMMAS
imports MERGED-RULES

configuration
<polkadot-host>
Expand Down Expand Up @@ -56,6 +57,185 @@ module KWASM-POLKADOT-HOST
<funcIds> ... ID |-> IDX:Int ... </funcIds>
...
</moduleInst>
endmodule
```

Merged Rules
============

This is a set of rules created by identifying common sub-sequences of semantic steps during execution of the `set_free_balance` function.

Most rules could not be used as they were printed, but had to be massaged in the following ways.
- Remove <generatedTop> cell
- Remove ellipsis inserted under that cell
- Remove ensures
- ~> DotVar\W* => ...
- #init\([^l]\)locals => #init_locals \1
- S SS => S SS:Stmts
- `BOP` => `BOP:IBinOp`,
- remove `<polkadot-host>`

```k
module MERGED-RULES
imports WASM-TEST

rule <wasm>
<k>
( ITYPE0 .const VAL
~> ITYPE0 . BOP:IBinOp:IBinOp SS => ITYPE0 . BOP C1 VAL modInt #pow( ITYPE0 )
~> SS )
...
</k>
<valstack>
( < ITYPE0 > C1 : VALSTACK0 => VALSTACK0 )
</valstack>
...
</wasm>
requires notBool SS ==K .EmptyStmts andBool false ==K #pow( ITYPE0 ) ==Int 0 andBool true
[priority(25)]

rule <wasm>
<k>
( #init_locals N VALUE0 : VALUE2 : VALSTACK0 => #init_locals N +Int 2 VALSTACK0 )
...
</k>
<curFrame>
<locals>
( LOCALS => LOCALS [ N <- VALUE0 ] [ N +Int 1 <- VALUE2 ] )
</locals>
...
</curFrame>
...
</wasm>
requires true andBool true
[priority(25)]

rule <wasm>
<k>
( ITYPE .const VAL
~> S SS:Stmts => S
~> SS )
...
</k>
<valstack>
( VALSTACK => < ITYPE > VAL modInt #pow( ITYPE ) : VALSTACK )
</valstack>
...
</wasm>
requires notBool SS ==K .EmptyStmts andBool false ==K #pow( ITYPE ) ==Int 0 andBool true
[priority(25)]

rule <wasm>
<k>
( #init_locals N VALUE0 : VALSTACK => #init_locals N +Int 1 VALSTACK )
...
</k>
<curFrame>
<locals>
( LOCALS => LOCALS [ N <- VALUE0 ] )
</locals>
...
</curFrame>
...
</wasm>
requires true andBool true
[priority(25)]

rule <wasm>
<k>
( ITYPE0 .const VAL ITYPE0 . BOP:IBinOp SS0 => ITYPE0 . BOP C1 VAL modInt #pow( ITYPE0 )
~> SS0 )
...
</k>
<valstack>
( < ITYPE0 > C1 : VALSTACK0 => VALSTACK0 )
</valstack>
...
</wasm>
requires notBool SS0 ==K .EmptyStmts andBool false ==K #pow( ITYPE0 ) ==Int 0 andBool true
[priority(25)]

rule <wasm>
<k>
( V
~> S SS:Stmts => S
~> SS )
...
</k>
<valstack>
( VALSTACK => V : VALSTACK )
</valstack>
...
</wasm>
requires notBool V ==K undefined andBool notBool SS ==K .EmptyStmts
```

The following rule required extra massaging:

- Remove `#Forall` side condition.
- Change #SemanticCastToInt to regular typing.
- Dotvar5 in the `<locals>` cell => ... on both sides.

```k
rule <wasm>
<k>
( local.get I:Int
~> S SS:Stmts => S
~> SS )
...
</k>
<valstack>
( VALSTACK => VALUE : VALSTACK )
</valstack>
<curFrame>
<locals>
... I |-> VALUE ...
</locals>
...
</curFrame>
...
</wasm>
requires notBool SS ==K .EmptyStmts andBool true
[priority(25)]

rule <wasm>
<k>
( local.get I:Int S0 SS0 => S0
~> SS0 )
...
</k>
<valstack>
( VALSTACK => VALUE : VALSTACK )
</valstack>
<curFrame>
<locals>
... I |-> VALUE ...
</locals>
...
</curFrame>
...
</wasm>
requires notBool SS0 ==K .EmptyStmts
andBool true
[priority(25)]

rule <wasm>
<k>
( local.get I:Int ITYPE0 .const VAL ITYPE0 . BOP:IBinOp SS1 => ITYPE0 . BOP C1 VAL modInt #pow( ITYPE0 )
~> SS1 )
...
</k>
<curFrame>
<locals>
... I |-> < ITYPE0 > C1 ...
</locals>
...
</curFrame>
...
</wasm>
requires notBool SS1 ==K .EmptyStmts andBool false ==K #pow( ITYPE0 ) ==Int 0 andBool true
```

```k
endmodule
```
2 changes: 1 addition & 1 deletion search.py
Original file line number Diff line number Diff line change
Expand Up @@ -99,7 +99,7 @@ def wasm_stmts_flattened(stmts, stmtType = 'Stmt'):
sys.stdout.flush()

if args['command'] == 'summary':
ruleMerges = merge_rules_max_productivity(ruleSeqs, min_merged_success_rate = 0.25, min_occurance_rate = 0.05)
ruleMerges = merge_rules_max_productivity(ruleSeqs, min_merged_success_rate = 0.15, min_occurance_rate = 0.00)
mergedRules = tryMergeRules(WASM_definition_haskell_no_coverage_dir, WASM_definition_main_file, WASM_definition_main_module, ruleMerges)
for mr in mergedRules:
print('Merged Rule:')
Expand Down