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.

Sign up for GitHub

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

Jump to bottom

Sparse bytes lemmas #659

Open
wants to merge 11 commits into
base: master
Choose a base branch
from
Open

Sparse bytes lemmas #659

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
11 commits
Select commit Hold shift + click to select a range
7e908d3
Disable replaceAtB for symbolic inputs
virgil-serbanuta Jun 26, 2024
4dcf8f6
Add SparseBytes lemmas
virgil-serbanuta Jun 26, 2024
ff07664
Set Version: 0.1.71
Jun 26, 2024
437e7f6
Fix shift definedness
virgil-serbanuta Jun 27, 2024
8a3e183
Fix right shifting of negative numbers: -1 >>Int 1 ==K -1
virgil-serbanuta Jun 27, 2024
204e055
Fix lemmas
virgil-serbanuta Jun 27, 2024
3bca8d7
Use total versions of operators.
virgil-serbanuta Jun 27, 2024
7d71631
Enable trivial evaluation for extractSparseBytes
virgil-serbanuta Jun 28, 2024
8b17c66
Int simplification lemmas
virgil-serbanuta Jun 28, 2024
22d891a
Merge branch 'master' into sparse-bytes-lemmas
virgil-serbanuta Jun 28, 2024
46d9252
Set Version: 0.1.74
Jun 28, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion package/version
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1 +1 @@
0.1.73
0.1.74
2 changes: 1 addition & 1 deletion pykwasm/pyproject.toml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"

[tool.poetry]
name = "pykwasm"
version = "0.1.73"
version = "0.1.74"
description = ""
authors = [
"Runtime Verification, Inc. <[email protected]>",
Expand Down
57 changes: 41 additions & 16 deletions pykwasm/src/pykwasm/kdist/wasm-semantics/data/sparse-bytes.k
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,6 +1,5 @@

module SPARSE-BYTES
imports BOOL
module SPARSE-BYTES-SYNTAX
imports BYTES
imports INT

Expand All @@ -9,9 +8,18 @@ module SPARSE-BYTES


syntax SBItemChunk ::= SBChunk(SBItem)

syntax SparseBytes ::= List{SBItemChunk, ""}

endmodule

module SPARSE-BYTES
imports BOOL
imports REPLACE-AT-CONCRETE
imports REPLACE-AT-SYNTAX
imports REPLACE-AT-SYMBOLIC
imports SPARSE-BYTES-SYNTAX

syntax Bytes ::= unwrap(SparseBytes)
[function, total, symbol, klabel(SparseBytes:unwrap)]
// -----------------------------------------------------------------
Expand Down Expand Up @@ -88,10 +96,6 @@ module SPARSE-BYTES
requires 0 <=Int S andBool S <=Int E
andBool S <Int lengthBytes(Bs)


syntax SparseBytes ::= replaceAt(SparseBytes, Int, Bytes)
[function, total, symbol, klabel(SparseBytes:replaceAt)]
// --------------------------------------------------------
// invalid argument
rule replaceAt(_, S, _) => .SparseBytes
requires S <Int 0
Expand All @@ -108,14 +112,7 @@ module SPARSE-BYTES
rule replaceAt(SBChunk(SBI) REST, S, Bs)
=> SBChunk(SBI) replaceAt(REST, S -Int size(SBI), Bs)
requires size(SBI) <=Int S

rule replaceAt(SBChunk(#empty(N)) REST, S, Bs) => replaceAtZ(N, REST, S, Bs)
requires S <Int N
rule replaceAt(SBChunk(#bytes(B)) REST, S, Bs) => replaceAtB(B, REST, S, Bs)
requires S <Int lengthBytes(B)

syntax SparseBytes ::= replaceAtZ(Int, SparseBytes, Int, Bytes)
[function, total, symbol, klabel(SparseBytes:replaceAtZ)]
// ---------------------------------------------------------------
////////////// S < 0
rule replaceAtZ(_, _, S, _) => .SparseBytes
Expand Down Expand Up @@ -155,8 +152,6 @@ module SPARSE-BYTES
andBool lengthBytes(Bs) >Int N


syntax SparseBytes ::= replaceAtB(Bytes, SparseBytes, Int, Bytes)
[function, total, symbol, klabel(SparseBytes:replaceAtB)]
// ---------------------------------------------------------------
////////// S + len(Bs) <= len(MB)
rule replaceAtB(MB, REST, S, Bs)
Expand Down Expand Up @@ -190,5 +185,35 @@ module SPARSE-BYTES
rule joinUntil(Bs, .SparseBytes, I)
=> SBChunk(#bytes( padRightBytes(Bs, I, 0) ))
requires I >Int lengthBytes(Bs)
endmodule

module REPLACE-AT-SYNTAX
imports SPARSE-BYTES-SYNTAX

syntax SparseBytes ::= replaceAt(SparseBytes, Int, Bytes)
[function, total, symbol, klabel(SparseBytes:replaceAt)]
syntax SparseBytes ::= replaceAtZ(Int, SparseBytes, Int, Bytes)
[function, total, symbol, klabel(SparseBytes:replaceAtZ)]
syntax SparseBytes ::= replaceAtB(Bytes, SparseBytes, Int, Bytes)
[function, total, symbol, klabel(SparseBytes:replaceAtB)]
endmodule

module REPLACE-AT-CONCRETE [concrete]
imports REPLACE-AT-SYNTAX

rule replaceAt(SBChunk(#empty(N)) REST, S, Bs) => replaceAtZ(N, REST, S, Bs)
requires S <Int N
rule replaceAt(SBChunk(#bytes(B)) REST, S, Bs) => replaceAtB(B, REST, S, Bs)
requires S <Int lengthBytes(B)
endmodule

module REPLACE-AT-SYMBOLIC [symbolic]
imports REPLACE-AT-SYNTAX

rule replaceAt(SBChunk(#empty(N)) REST, S, Bs) => replaceAtZ(N, REST, S, Bs)
requires S <Int N
[simplification, concrete]
rule replaceAt(SBChunk(#bytes(B)) REST, S, Bs) => replaceAtB(B, REST, S, Bs)
requires S <Int lengthBytes(B)
[simplification, concrete]
endmodule
113 changes: 74 additions & 39 deletions pykwasm/src/pykwasm/kdist/wasm-semantics/kwasm-lemmas.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,12 +6,19 @@ They are part of the *trusted* base, and so should be scrutinized carefully.

```k
requires "wasm-text.md"
requires "symbolic/symbolic.md"

module KWASM-LEMMAS [symbolic]
module KWASM-LEMMAS
imports WASM-SYMBOLIC
imports KWASM-LEMMAS-SYMBOLIC
endmodule

module KWASM-LEMMAS-SYMBOLIC [symbolic]
imports WASM-TEXT
imports BYTES-KORE
imports INT-SYMBOLIC
imports MAP-SYMBOLIC
imports CEILS-SYNTAX
```

Basic logic
Expand Down Expand Up @@ -48,14 +55,14 @@ These are given in pure modulus form, and in form with `#wrap`, which is modulus
andBool X <Int (1 <<Int (N *Int 8))
[simplification]

rule _X modInt 1 => 0
rule _X modIntTotal 1 => 0
[simplification]
```

`modInt` selects the least non-negative representative of a congruence class modulo `N`.

```k
rule (X modInt M) modInt N => X modInt M
rule (X modIntTotal M) modIntTotal N => X modInt M
requires M >Int 0
andBool M <=Int N
[simplification]
Expand All @@ -72,7 +79,7 @@ Since 0 <= x mod m < m <= n, (x mod m) mod n = x mod m
```

```k
rule (X modInt M) modInt N => X modInt N
rule (X modIntTotal M) modIntTotal N => X modInt N
requires M >Int 0
andBool N >Int 0
andBool M modInt N ==Int 0
Expand All @@ -98,24 +105,24 @@ x = m * q + r, for a unique q and r s.t. 0 <= r < m
#### Modulus Over Addition

```k
rule (_X *Int M +Int Y) modInt N => Y modInt N
rule (_X *Int M +Int Y) modIntTotal N => Y modInt N
requires M >Int 0
andBool N >Int 0
andBool M modInt N ==Int 0
[simplification]

rule (Y +Int _X *Int M) modInt N => Y modInt N
rule (Y +Int _X *Int M) modIntTotal N => Y modInt N
requires M >Int 0
andBool N >Int 0
andBool M modInt N ==Int 0
[simplification]

rule #wrap(N, (_X <<Int M) +Int Y) => #wrap(N, Y)
rule #wrap(N, (_X <<IntTotal M) +Int Y) => #wrap(N, Y)
requires 0 <=Int M
andBool (N *Int 8) <=Int M
[simplification]

rule #wrap(N, Y +Int (_X <<Int M)) => #wrap(N, Y)
rule #wrap(N, Y +Int (_X <<IntTotal M)) => #wrap(N, Y)
requires 0 <=Int M
andBool (N *Int 8) <=Int M
[simplification]
Expand All @@ -129,13 +136,13 @@ x * m + y mod n = x * (k * n) + y mod n = y mod n
```

```k
rule ((X modInt M) +Int Y) modInt N => (X +Int Y) modInt N
rule ((X modIntTotal M) +Int Y) modIntTotal N => (X +Int Y) modInt N
requires M >Int 0
andBool N >Int 0
andBool M modInt N ==Int 0
[simplification]

rule (X +Int (Y modInt M)) modInt N => (X +Int Y) modInt N
rule (X +Int (Y modIntTotal M)) modIntTotal N => (X +Int Y) modInt N
requires M >Int 0
andBool N >Int 0
andBool M modInt N ==Int 0
Expand Down Expand Up @@ -168,29 +175,51 @@ x mod m + y = r + y
We want K to understand what a bit-shift is.

```k
rule (_X <<Int N) modInt M => 0
requires (2 ^Int N) modInt M ==Int 0
// According to domains.md, shifting by negative amounts is #False, so
// all simplification rules must take that into account.

rule (_X <<IntTotal N) modIntTotal M => 0
requires 0 <=Int N andBool (2 ^Int N) modInt M ==Int 0
[simplification]

rule #wrap(M, _X <<Int N) => 0
requires (M *Int 8) <=Int N
rule #wrap(M, _X <<IntTotal N) => 0
requires 0 <=Int N andBool (M *Int 8) <=Int N
[simplification]

rule (X >>Int N) => 0 requires X <Int 2 ^Int N [simplification]
rule (_X <<Int N) modInt M => 0 requires M <Int 2 ^Int N [simplification]
rule (X >>IntTotal N) => 0
requires 0 <=Int N
andBool 0 <=Int X
andBool X <Int 2 ^Int N
[simplification]
rule (_X <<IntTotal N) modIntTotal M => 0
requires 0 <=Int N
andBool M <Int 2 ^Int N
[simplification]

rule (X >>Int N) >>Int M => X >>Int (N +Int M) [simplification]
rule (X <<Int N) <<Int M => X <<Int (N +Int M) [simplification]
rule (X >>IntTotal N) >>IntTotal M => X >>Int (N +Int M)
requires 0 <=Int N andBool 0 <=Int M
[simplification]
rule (X <<IntTotal N) <<IntTotal M => X <<Int (N +Int M)
requires 0 <=Int N andBool 0 <=Int M
[simplification]

// The Haskell backend accepts negative shifts (the LLVM backend does not).
// So removing the side conditions and keeping one of each rule here could give faster symbolic execution.
rule (X <<Int N) >>Int M => X <<Int (N -Int M) requires N >=Int M [simplification]
rule (X <<Int N) >>Int M => X >>Int (M -Int N) requires notBool (N >=Int M) [simplification]
rule (X <<IntTotal N) >>IntTotal M => X <<Int (N -Int M)
requires 0 <=Int M andBool M <=Int N
[simplification]
rule (X <<IntTotal N) >>IntTotal M => X >>Int (M -Int N)
requires 0 <=Int N andBool notBool (N >=Int M)
[simplification]
```

```k
rule ((X <<Int M) +Int Y) >>Int N => (X <<Int (M -Int N)) +Int (Y >>Int N) requires M >=Int N [simplification]
rule (Y +Int (X <<Int M)) >>Int N => (X <<Int (M -Int N)) +Int (Y >>Int N) requires M >=Int N [simplification]
rule ((X <<IntTotal M) +Int Y) >>IntTotal N => (X <<Int (M -Int N)) +Int (Y >>Int N)
requires M >=Int N andBool N >=Int 0
andBool 0 <=Int X andBool 0 <=Int Y
[simplification]
rule (Y +Int (X <<IntTotal M)) >>IntTotal N => (X <<Int (M -Int N)) +Int (Y >>Int N)
requires M >=Int N andBool N >=Int 0
andBool 0 <=Int X andBool 0 <=Int Y
[simplification]
```

Proof:
Expand All @@ -212,13 +241,14 @@ Let x' = x << m
The following rules decrease the modulus by rearranging it around a shift.

```k
rule (X modInt POW) >>Int N => (X >>Int N) modInt (POW /Int (2 ^Int N))
rule (X modIntTotal POW) >>IntTotal N => (X >>Int N) modInt (POW /Int (2 ^Int N))
requires N >=Int 0
andBool POW >Int 0
andBool POW modInt (2 ^Int N) ==Int 0
andBool 0 <=Int X
[simplification]

rule (X <<Int N) modInt POW => (X modInt (POW /Int (2 ^Int N))) <<Int N
rule (X <<IntTotal N) modIntTotal POW => (X modInt (POW /Int (2 ^Int N))) <<Int N
requires N >=Int 0
andBool POW >Int 0
andBool POW modInt (2 ^Int N) ==Int 0
Expand All @@ -231,13 +261,13 @@ Therefore, we may as well shift first and then take the modulus, only we need to
The argument for the left shift is similar.

```k
rule (X +Int (_Y <<Int N)) modInt POW => X modInt POW
rule (X +Int (_Y <<IntTotal N)) modIntTotal POW => X modInt POW
requires N >=Int 0
andBool POW >Int 0
andBool (2 ^Int N) modInt POW ==Int 0
[simplification]

rule ((_Y <<Int N) +Int X) modInt POW => X modInt POW
rule ((_Y <<IntTotal N) +Int X) modIntTotal POW => X modInt POW
requires N >=Int 0
andBool POW >Int 0
andBool (2 ^Int N) modInt POW ==Int 0
Expand All @@ -252,7 +282,7 @@ When reasoning about `#chop`, it's often the case that the precondition to the p
In this case, it's simpler (and safe) to simply discard the `#chop`, instead of evaluating it.

```k
rule X modInt #pow(ITYPE) => #unsigned(ITYPE, X)
rule X modIntTotal #pow(ITYPE) => #unsigned(ITYPE, X)
requires #inSignedRange (ITYPE, X)
[simplification]

Expand Down Expand Up @@ -280,15 +310,19 @@ Memory
Bounds on `#getRange`:

```k
rule 0 <=Int #getRange(_, _, _) => true [simplification]
rule 0 <=Int VAL <<Int SHIFT => true requires 0 <=Int VAL andBool 0 <=Int SHIFT [simplification]
rule 0 <=Int VAL1 +Int VAL2 => true requires 0 <=Int VAL1 andBool 0 <=Int VAL2 [simplification]

rule #getRange(_, _, WIDTH) <Int MAX => true requires 2 ^Int (8 *Int WIDTH) <=Int MAX [simplification]
rule #getRange(_, _, WIDTH) <<Int SHIFT <Int MAX => true requires 2 ^Int ((8 *Int WIDTH) +Int SHIFT) <=Int MAX [simplification]
rule (#getRange(_, _, WIDTH1) #as VAL1) +Int ((#getRange(_, _, WIDTH2) <<Int SHIFT) #as VAL2) <Int MAX => true
rule 0 <=Int #getRange(_, _, _) => true [simplification]
rule 0 <=Int VAL <<IntTotal SHIFT => true requires 0 <=Int VAL andBool 0 <=Int SHIFT [simplification]
rule 0 <=Int VAL1 +Int VAL2 => true requires 0 <=Int VAL1 andBool 0 <=Int VAL2 [simplification]

rule #getRange(_, _, WIDTH) <Int MAX => true requires 2 ^Int (8 *Int WIDTH) <=Int MAX [simplification]
rule #getRange(_, _, WIDTH) <<IntTotal SHIFT <Int MAX => true
requires 2 ^Int ((8 *Int WIDTH) +Int SHIFT) <=Int MAX
andBool 0 <=Int SHIFT
[simplification]
rule (#getRange(_, _, WIDTH1) #as VAL1) +Int ((#getRange(_, _, WIDTH2) <<IntTotal SHIFT) #as VAL2) <Int MAX => true
requires VAL1 <Int MAX
andBool VAL2 <Int MAX
andBool 0 <=Int SHIFT
andBool WIDTH1 *Int 8 <=Int SHIFT
andBool 2 ^Int ((8 *Int WIDTH2) +Int SHIFT) <=Int MAX
[simplification]
Expand All @@ -305,13 +339,13 @@ Bounds on `#getRange`:
Arithmetic over `#getRange`:

```k
rule #getRange(BM, ADDR, WIDTH) >>Int SHIFT => #getRange(BM, ADDR +Int 1, WIDTH -Int 1) >>Int (SHIFT -Int 8)
rule #getRange(BM, ADDR, WIDTH) >>IntTotal SHIFT => #getRange(BM, ADDR +Int 1, WIDTH -Int 1) >>Int (SHIFT -Int 8)
requires 0 <=Int ADDR
andBool 0 <Int WIDTH
andBool 8 <=Int SHIFT
[simplification]

rule #getRange(BM, ADDR, WIDTH) modInt MAX => #getRange(BM, ADDR, WIDTH -Int 1) modInt MAX
rule #getRange(BM, ADDR, WIDTH) modIntTotal MAX => #getRange(BM, ADDR, WIDTH -Int 1) modInt MAX
requires 0 <Int MAX andBool 0 <Int WIDTH
andBool 2 ^Int (8 *Int (WIDTH -Int 1)) modInt MAX ==Int 0
[simplification]
Expand All @@ -335,9 +369,10 @@ Arithmetic over `#getRange`:

```k
rule #setRange(BM, ADDR, #getRange(BM, ADDR, WIDTH), WIDTH) => BM [simplification]
rule #setRange(BM, ADDR, (#getRange(_, _, WIDTH1) #as VAL1) +Int (VAL2 <<Int SHIFT), WIDTH)
rule #setRange(BM, ADDR, (#getRange(_, _, WIDTH1) #as VAL1) +Int (VAL2 <<IntTotal SHIFT), WIDTH)
=> #setRange(#setRange(BM, ADDR, VAL1, minInt(WIDTH1, WIDTH)), ADDR +Int WIDTH1, VAL2, WIDTH -Int WIDTH1)
requires 0 <=Int ADDR
andBool 0 <=Int SHIFT
andBool 0 <Int WIDTH
andBool WIDTH1 *Int 8 ==Int SHIFT
[simplification]
Expand Down
Loading