From 42e19cf74ad80893d5ad792b5d2aa5c13c1efd81 Mon Sep 17 00:00:00 2001 From: Virgil Date: Fri, 31 May 2024 20:37:07 +0300 Subject: [PATCH 1/2] Refactor sparse-bytes --- .../kdist/wasm-semantics/data/sparse-bytes.k | 99 +++++++++++++------ 1 file changed, 70 insertions(+), 29 deletions(-) diff --git a/pykwasm/src/pykwasm/kdist/wasm-semantics/data/sparse-bytes.k b/pykwasm/src/pykwasm/kdist/wasm-semantics/data/sparse-bytes.k index 595cd85f7..6372996ad 100644 --- a/pykwasm/src/pykwasm/kdist/wasm-semantics/data/sparse-bytes.k +++ b/pykwasm/src/pykwasm/kdist/wasm-semantics/data/sparse-bytes.k @@ -1,6 +1,4 @@ - -module SPARSE-BYTES - imports BOOL +module SPARSE-BYTES-SYNTAX imports BYTES imports INT @@ -9,11 +7,33 @@ module SPARSE-BYTES syntax SBItemChunk ::= SBChunk(SBItem) - + syntax SparseBytes ::= List{SBItemChunk, ""} syntax Bytes ::= unwrap(SparseBytes) [function, total, symbol, klabel(SparseBytes:unwrap)] + + syntax Bytes ::= unwrap(SBItem) + [function, total, symbol, klabel(SBItem:unwrap)] + + syntax Int ::= size(SparseBytes) + [function, total, klabel(SparseBytes:size), symbol] + + syntax Int ::= size(SBItem) + [function, total, symbol, klabel(SBItem:size)] + + syntax Bytes ::= zeros(Int) [function, total, symbol, klabel(zeros)] +endmodule + +module SPARSE-BYTES + imports BOOL + imports SPARSE-BYTES-SYNTAX + imports REPLACE-AT-COMMON + imports REPLACE-AT-CONCRETE + imports REPLACE-AT-SYMBOLIC + + // syntax Bytes ::= unwrap(SparseBytes) + // [function, total, symbol, klabel(SparseBytes:unwrap)] // ----------------------------------------------------------------- rule unwrap(SBChunk(SBI) REST) => unwrap(SBI) +Bytes unwrap(REST) rule unwrap(.SparseBytes) => .Bytes @@ -23,24 +43,24 @@ module SPARSE-BYTES // --------------------------------------------------------- rule fromBytes(Bs) => SBChunk(#bytes(Bs)) - syntax Bytes ::= unwrap(SBItem) - [function, total, symbol, klabel(SBItem:unwrap)] + // syntax Bytes ::= unwrap(SBItem) + // [function, total, symbol, klabel(SBItem:unwrap)] // ----------------------------------------------- rule unwrap(#bytes(Bs)) => Bs rule unwrap(#empty(N)) => zeros(N) - syntax Bytes ::= zeros(Int) [function, total, symbol, klabel(zeros)] + // syntax Bytes ::= zeros(Int) [function, total, symbol, klabel(zeros)] // ------------------------------------------------------------------- rule zeros(N) => padLeftBytes(.Bytes, size(#empty(N)), 0) - syntax Int ::= size(SparseBytes) - [function, total, klabel(SparseBytes:size), symbol] + // syntax Int ::= size(SparseBytes) + // [function, total, klabel(SparseBytes:size), symbol] // --------------------------------------------------- rule size(SBChunk(SBI) SBS) => size(SBI) +Int size(SBS) rule size(.SparseBytes) => 0 - syntax Int ::= size(SBItem) - [function, total, symbol, klabel(SBItem:size)] + // syntax Int ::= size(SBItem) + // [function, total, symbol, klabel(SBItem:size)] // ----------------------------------------------- rule size(#bytes(Bs)) => lengthBytes(Bs) rule size(#empty(N)) => maxInt(N,0) @@ -59,7 +79,7 @@ module SPARSE-BYTES requires 0 <=Int S andBool S <=Int E andBool size(SBI) <=Int S - rule substrSparseBytes(SBChunk(SBI) REST, S, E) + rule substrSparseBytes(SBChunk(SBI) REST, S, E) => #let SUB = substrSBItem(SBI, S, E) #in SUB substrSparseBytes(REST, 0, E -Int size(SBI)) requires 0 <=Int S andBool S <=Int E @@ -78,22 +98,27 @@ module SPARSE-BYTES rule substrSBItem(#empty(N), S, E) => SBChunk( #empty( minInt(E, N) -Int S) ) requires 0 <=Int S andBool S <=Int E andBool S .SparseBytes requires 0 <=Int S andBool S <=Int E andBool lengthBytes(Bs) <=Int S - rule substrSBItem(#bytes(Bs), S, E) + rule substrSBItem(#bytes(Bs), S, E) => SBChunk(#bytes( substrBytes(Bs, S, minInt(E, lengthBytes(Bs))) )) requires 0 <=Int S andBool S <=Int E - andBool S .SparseBytes + rule replaceAt(_, S, _) => .SparseBytes requires S 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 replaceAtB(B, REST, S, Bs) - requires S .SparseBytes + rule replaceAtZ(_, _, S, _) => .SparseBytes requires S 0 // split zeros: 0 < S < N rule replaceAtZ(N, REST, S, Bs) - => SBChunk(#empty(S)) replaceAtZ(N -Int S, REST, 0, Bs) + => SBChunk(#empty(S)) replaceAtZ(N -Int S, REST, 0, Bs) requires 0 SBChunk(#empty(N)) replaceAt(REST, S -Int N, Bs) + => SBChunk(#empty(N)) replaceAt(REST, S -Int N, Bs) requires 0 SBChunk(#bytes(Bs)) SBChunk(#empty(N -Int lengthBytes(Bs))) REST + => SBChunk(#bytes(Bs)) SBChunk(#empty(N -Int lengthBytes(Bs))) REST requires 0 ==Int S andBool lengthBytes(Bs) SBChunk(#bytes(Bs)) REST + => SBChunk(#bytes(Bs)) REST requires 0 ==Int S andBool lengthBytes(Bs) ==Int N ///////// len(Bs) > N rule replaceAtZ(N, REST, S, Bs) - => replaceAt(SBChunk(#bytes(zeros(N))) REST, S, Bs) + => replaceAt(SBChunk(#bytes(zeros(N))) REST, S, Bs) requires 0 ==Int S andBool lengthBytes(Bs) >Int N @@ -172,7 +192,7 @@ module SPARSE-BYTES Bs ) requires 0 <=Int S - andBool lengthBytes(MB) SBChunk(#bytes( padRightBytes(Bs, I, 0) )) requires I >Int lengthBytes(Bs) +endmodule + +module REPLACE-AT-CONCRETE [concrete] + imports REPLACE-AT-COMMON + + rule replaceAt(SBChunk(#empty(N)) REST, S, Bs) => replaceAtZ(N, REST, S, Bs) + requires S replaceAtB(B, REST, S, Bs) + requires S replaceAtZ(N, REST, S, Bs) + requires S replaceAtB(B, REST, S, Bs) + requires S Date: Mon, 3 Jun 2024 17:51:25 +0000 Subject: [PATCH 2/2] Set Version: 0.1.59 --- package/version | 2 +- pykwasm/pyproject.toml | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/package/version b/package/version index 61671068e..09d8256ac 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -0.1.58 +0.1.59 diff --git a/pykwasm/pyproject.toml b/pykwasm/pyproject.toml index 8725d6860..2d76dc206 100644 --- a/pykwasm/pyproject.toml +++ b/pykwasm/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api" [tool.poetry] name = "pykwasm" -version = "0.1.58" +version = "0.1.59" description = "" authors = [ "Runtime Verification, Inc. ",