Open
Description
Note that this spec is not supposed to pass, it was drastically changed form the original in order to reduce the size of the files below.
To reproduce:
Versions
kompile:
K version: v5.5.40-0-g98574f12a2-dirty
Build date: Wed Dec 07 16:21:49 EET 2022
backend:
Kore version 0.60.0.0
Git:
revision: bdfc0fa4b0e381b3d02551ab0d4b4f89cedf814b
branch: HEAD
last commit: Wed Nov 30 06:11:08 2022 -0700
Files
a.k
module A
imports BOOL
imports INT
imports K-EQUAL
configuration
<esdt>
<is-running> #no:Running </is-running>
<shards>
<shard multiplicity="*" type="Map">
<shard-id> 0:Int </shard-id>
<steps> .K </steps>
<current-tx> 0 </current-tx>
</shard>
</shards>
</esdt>
syntax Running ::= "#no"
| Int
syntax TxStep ::= #failure( Int )
| "#finalizeTransaction"
rule <shard>
<steps> (#failure(_Err) => .) ~> #finalizeTransaction </steps>
<current-tx> _Tx </current-tx>
...
</shard>
// Check if the execution cells (<current-tx/> and <steps/>) in all shards are empty
syntax Bool ::= #allEmpty(ShardsCell) [function, total]
rule #allEmpty(S) => #allEmptyHelper(S, true)
syntax Bool ::= #allEmptyHelper(ShardsCell, Bool) [function, total]
rule #allEmptyHelper(<shards> .Bag </shards>, true) => true
rule #allEmptyHelper(_, false) => false
rule #allEmptyHelper(<shards>
(<shard>
<steps> Ss </steps>
<current-tx> Tx </current-tx>
_
</shard> => .Bag
)
...
</shards>
, B => B andBool (Ss =/=K .K orBool Tx =/=K 0)
) [simplification]
rule #allEmptyHelper(S, (_ andBool _) #as Cond) => #allEmptyHelper(S, true) andBool Cond [simplification]
rule #allEmptyHelper(S, (_ orBool _) #as Cond) => #allEmptyHelper(S, true) andBool Cond [simplification]
endmodule
spec.k
requires "a.k"
module SPEC
imports A
claim
<is-running> ShrId </is-running>
<shards>
<shard>
<shard-id> ShrId </shard-id>
// Execution
<current-tx> 1 </current-tx>
<steps> . => #finalizeTransaction </steps>
...
</shard>
OtherShards
</shards>
requires #allEmpty(<shards> OtherShards </shards>)
endmodule
Running
Command line:
kompile a.k --backend haskell && kprove --debug spec.k --haskell-backend-command 'kore-repl --version --repl-script ../kast.kscript'
repl:
step
select 1
konfig
Results
Note that the displayed config contains this:
#And
{
true
#Equals
notBool ( #failure ( _Err ) ~> #finalizeTransaction ~> . ) ==K . orBool notBool _Tx ==Int 0
}
which should be simplified to Top.