Skip to content

Commit 204e055

Browse files
Fix lemmas
1 parent 8a3e183 commit 204e055

File tree

2 files changed

+5
-0
lines changed

2 files changed

+5
-0
lines changed

pykwasm/src/pykwasm/kdist/wasm-semantics/symbolic/sparse-bytes/set-range-lemmas.md

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -88,6 +88,9 @@ module SET-RANGE-LEMMAS [symbolic]
8888
andBool functionSparseBytesWellDefined(setRange(Value), Addr, Width)
8989
[simplification]
9090
91+
rule updateSparseBytes(setRange(#getRange(M, Addr, Width)), M, Addr, Width) => M
92+
[simplification]
93+
9194
endmodule
9295
9396
```

pykwasm/src/pykwasm/kdist/wasm-semantics/symbolic/wasm-lemmas.md

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,9 +1,11 @@
11
```k
2+
requires "int/symbolic.md"
23
requires "sparse-bytes/sparse-bytes-lemmas.md"
34
45
module WASM-LEMMAS
56
imports private CEILS-SYNTAX
67
imports private SPARSE-BYTES-LEMMAS
8+
imports private WASM-INT-SYMBOLIC
79
imports private WASM-TEXT
810
911
rule Bytes2Int(#getBytesRange(_:SparseBytes, _:Int, N:Int), _:Endianness, _:Signedness) <Int M:Int

0 commit comments

Comments
 (0)