Upstream lemmas from Wormhole engagement #1866

qian-hu · 2023-05-27T05:19:45Z

Part of: #1588

This PR includes lemmas from previous Wormhole engagement.

This reverts commit 22f8392.

include/kframework/word.md

include/kframework/lemmas/bitwise-simplification.k

include/kframework/lemmas/bytes-simplification.k

Co-authored-by: Everett Hildenbrandt <everett.hildenbrandt@gmail.com>

palinatolmach · 2023-09-22T02:06:04Z

@qian-hu @PetarMax could you please provide an update on this PR? Do you think we should merge it? Thanks!

palinatolmach · 2023-09-28T11:45:32Z

Should be done by 10/03.

PetarMax · 2023-10-02T09:22:47Z

I have done a pass and added a few more lemmas - now it's up to the CI

ehildenb · 2023-10-02T16:25:34Z

I don't see any tests of the new lemmas added. Are there any from the Wormhole engagement which can be added here, like runlemma => donelemma style lemmas? We also can just write them as functional claims in some places. But we should have tests of them, regression tests are important.

PetarMax · 2023-10-02T17:26:50Z

I don't see any tests of the new lemmas added. Are there any from the Wormhole engagement which can be added here, like runlemma => donelemma style lemmas? We also can just write them as functional claims in some places. But we should have tests of them, regression tests are important.

This I don't know - @qian-hu, @lucasmt?

qian-hu · 2023-10-03T04:20:30Z

I've added the claims needed to test the newly added lemmas.

PetarMax · 2023-10-03T10:33:32Z

tests/specs/functional/lemmas-spec.k

+    claim <k> runLemma ( notMaxUInt5   &Int X ) => doneLemma( 0 ) ... </k> requires #rangeUInt (   5 , X )
+    claim <k> runLemma ( notMaxUInt8   &Int X ) => doneLemma( 0 ) ... </k> requires #rangeUInt (   8 , X )
+    claim <k> runLemma ( notMaxUInt16  &Int X ) => doneLemma( 0 ) ... </k> requires #rangeUInt (  16 , X )
+    claim <k> runLemma ( notMaxUInt32  &Int X ) => doneLemma( 0 ) ... </k> requires #rangeUInt (  32 , X )
+    claim <k> runLemma ( notMaxUInt64  &Int X ) => doneLemma( 0 ) ... </k> requires #rangeUInt (  64 , X )
+    claim <k> runLemma ( notMaxUInt96  &Int X ) => doneLemma( 0 ) ... </k> requires #rangeUInt (  96 , X )
+    claim <k> runLemma ( notMaxUInt128 &Int X ) => doneLemma( 0 ) ... </k> requires #rangeUInt ( 128 , X )
+    claim <k> runLemma ( notMaxUInt160 &Int X ) => doneLemma( 0 ) ... </k> requires #rangeUInt ( 160 , X )
+    claim <k> runLemma ( notMaxUInt192 &Int X ) => doneLemma( 0 ) ... </k> requires #rangeUInt ( 192 , X )
+    claim <k> runLemma ( notMaxUInt208 &Int X ) => doneLemma( 0 ) ... </k> requires #rangeUInt ( 208 , X )
+    claim <k> runLemma ( notMaxUInt224 &Int X ) => doneLemma( 0 ) ... </k> requires #rangeUInt ( 224 , X )
+    claim <k> runLemma ( notMaxUInt240 &Int X ) => doneLemma( 0 ) ... </k> requires #rangeUInt ( 240 , X )
+    claim <k> runLemma ( notMaxUInt248 &Int X ) => doneLemma( 0 ) ... </k> requires #rangeUInt ( 248 , X )
+
+    claim <k> runLemma ( notMaxUInt240 &Int ( X <<Int 240 ) ) => doneLemma( X <<Int 240 ) ... </k> requires #rangeUInt ( 16 , X )
+    claim <k> runLemma ( notMaxUInt248 &Int ( X <<Int 248 ) ) => doneLemma( X <<Int 248 ) ... </k> requires #rangeUInt (  8 , X )
+
+    claim <k> runLemma ( maxUInt8   &Int ( X |Int ( notMaxUInt8   &Int Y ) ) ) => doneLemma( X ) ... </k> requires #rangeUInt (   8 , X )
+    claim <k> runLemma ( maxUInt16  &Int ( X |Int ( notMaxUInt16  &Int Y ) ) ) => doneLemma( X ) ... </k> requires #rangeUInt (  16 , X )
+    claim <k> runLemma ( maxUInt32  &Int ( X |Int ( notMaxUInt32  &Int Y ) ) ) => doneLemma( X ) ... </k> requires #rangeUInt (  32 , X )
+    claim <k> runLemma ( maxUInt64  &Int ( X |Int ( notMaxUInt64  &Int Y ) ) ) => doneLemma( X ) ... </k> requires #rangeUInt (  64 , X )
+    claim <k> runLemma ( maxUInt96  &Int ( X |Int ( notMaxUInt96  &Int Y ) ) ) => doneLemma( X ) ... </k> requires #rangeUInt (  96 , X )
+    claim <k> runLemma ( maxUInt128 &Int ( X |Int ( notMaxUInt128 &Int Y ) ) ) => doneLemma( X ) ... </k> requires #rangeUInt ( 128 , X )
+    claim <k> runLemma ( maxUInt160 &Int ( X |Int ( notMaxUInt160 &Int Y ) ) ) => doneLemma( X ) ... </k> requires #rangeUInt ( 160 , X )
+    claim <k> runLemma ( maxUInt192 &Int ( X |Int ( notMaxUInt192 &Int Y ) ) ) => doneLemma( X ) ... </k> requires #rangeUInt ( 192 , X )
+    claim <k> runLemma ( maxUInt208 &Int ( X |Int ( notMaxUInt208 &Int Y ) ) ) => doneLemma( X ) ... </k> requires #rangeUInt ( 208 , X )
+    claim <k> runLemma ( maxUInt224 &Int ( X |Int ( notMaxUInt224 &Int Y ) ) ) => doneLemma( X ) ... </k> requires #rangeUInt ( 224 , X )
+    claim <k> runLemma ( maxUInt240 &Int ( X |Int ( notMaxUInt240 &Int Y ) ) ) => doneLemma( X ) ... </k> requires #rangeUInt ( 240 , X )
+    claim <k> runLemma ( maxUInt248 &Int ( X |Int ( notMaxUInt248 &Int Y ) ) ) => doneLemma( X ) ... </k> requires #rangeUInt ( 248 , X )


These are direct uses of the simplifications - @qian-hu, have we got anything from the engagament that needed them? I have others from the other engagement, but they require further simplifications to pass.

I think we can merge with this for now, and then I will add mine once these further simplifications are upstreamed.

* Add notMaxUInt constants * Add bitwise-arithmetic lemmas * Upstream bytes-simplification lemmas from Wormhole * Upstream lemmas from Wormhole engagement * Set Version: 1.0.187 * Revert "Upstream lemmas from Wormhole engagement" This reverts commit 22f8392. * Set Version: 1.0.210 * Update include/kframework/word.md Co-authored-by: Everett Hildenbrandt <everett.hildenbrandt@gmail.com> * Set Version: 1.0.211 * Set Version: 1.0.212 * Set Version: 1.0.213 * Set Version: 1.0.219 * Set Version: 1.0.227 * Set Version: 1.0.228 * generalize lemmas * Set Version: 1.0.244 * Set Version: 1.0.249 * Set Version: 1.0.296 * Set Version: 1.0.309 * cleanup * simplification fix * Set Version: 1.0.310 * removing simplification * Fix simplification * Add claims for lemmas * Update bytes-simplification.k * Add more claims for lemmas --------- Co-authored-by: devops <devops@runtimeverification.com> Co-authored-by: Everett Hildenbrandt <everett.hildenbrandt@gmail.com> Co-authored-by: Petar Maksimovic <petar.maksimovic@runtimeverification.com> Co-authored-by: Petar Maksimović <PetarMax@users.noreply.github.com>

* Add '--smt-tactic <s-expression>' command-line option * Set Version: 1.0.305 * Set Version: 1.0.307 * Set Version: 1.0.308 * Small build updates for LLVM backend, timing updates (#2098) * kevm-pyk/{kompile,__main__}: do not turn on debug symbols by default * kevm-pyk/dist: parallelize plugin build * kevm-pyk/__main__: add proof timing information to info log * Set Version: 1.0.308 * kevm-pyk/dist: typo --------- Co-authored-by: devops <devops@runtimeverification.com> * Update dependency: kevm-pyk/src/kevm_pyk/kproj/plugin (#2100) * kevm-pyk/src/kevm_pyk/kproj/plugin: Set Version c095983f3aec21c52f00b2d433202052ad7db104 * Set Version: 1.0.309 * kevm-pyk/: sync poetry files pyk version v0.1.448 * deps/blockchain-k-plugin_release: sync release file version c095983f3aec21c52f00b2d433202052ad7db104 * flake.{nix,lock}: update Nix derivations --------- Co-authored-by: devops <devops@runtimeverification.com> * Upstream lemmas from Wormhole engagement (#1866) * Add notMaxUInt constants * Add bitwise-arithmetic lemmas * Upstream bytes-simplification lemmas from Wormhole * Upstream lemmas from Wormhole engagement * Set Version: 1.0.187 * Revert "Upstream lemmas from Wormhole engagement" This reverts commit 22f8392. * Set Version: 1.0.210 * Update include/kframework/word.md Co-authored-by: Everett Hildenbrandt <everett.hildenbrandt@gmail.com> * Set Version: 1.0.211 * Set Version: 1.0.212 * Set Version: 1.0.213 * Set Version: 1.0.219 * Set Version: 1.0.227 * Set Version: 1.0.228 * generalize lemmas * Set Version: 1.0.244 * Set Version: 1.0.249 * Set Version: 1.0.296 * Set Version: 1.0.309 * cleanup * simplification fix * Set Version: 1.0.310 * removing simplification * Fix simplification * Add claims for lemmas * Update bytes-simplification.k * Add more claims for lemmas --------- Co-authored-by: devops <devops@runtimeverification.com> Co-authored-by: Everett Hildenbrandt <everett.hildenbrandt@gmail.com> Co-authored-by: Petar Maksimovic <petar.maksimovic@runtimeverification.com> Co-authored-by: Petar Maksimović <PetarMax@users.noreply.github.com> * Add `setGas` cheatcode (#2101) * Add `setGas` cheatcode * Set Version: 1.0.310 * Set Version: 1.0.311 --------- Co-authored-by: devops <devops@runtimeverification.com> Co-authored-by: rv-jenkins <admin@runtimeverification.com> * .github/workflows: use z3-images repository for prebuilt z3 images (#2104) * .github/workflows: use z3-images repository for prebuilt z3 images * Set Version: 1.0.312 --------- Co-authored-by: devops <devops@runtimeverification.com> * Support for init bytecode (#2096) * Split off support for init bytecode for kevm * Set Version: 1.0.308 * Set Version: 1.0.308 * Fix formatting * Set Version: 1.0.309 * Set Version: 1.0.310 * Set Version: 1.0.312 * Fix formatting * Set Version: 1.0.313 --------- Co-authored-by: devops <devops@runtimeverification.com> * Run prover tests on fast CI machines (#2108) * .github/test-pr: run fonudry tests on fast CI runners * Set Version: 1.0.312 * .github/test-pr: also run normal KClaim style proofs on fast CI runners * Set Version: 1.0.313 * Set Version: 1.0.314 * .github/test-pr: reduce parallelism on test-suite * .github/test-pr: correct way to adjust parallelism --------- Co-authored-by: devops <devops@runtimeverification.com> Co-authored-by: rv-jenkins <admin@runtimeverification.com> * Update dependency: deps/pyk_release (#2092) * deps/pyk_release: Set Version v0.1.449 * Set Version: 1.0.307 * kevm-pyk/: sync poetry files pyk version v0.1.449 * deps/k_release: sync release file version 6.0.118 * flake.{nix,lock}: update Nix derivations * deps/pyk_release: Set Version v0.1.450 * Set Version: 1.0.308 * kevm-pyk/: sync poetry files pyk version v0.1.450 * flake.{nix,lock}: update Nix derivations * deps/pyk_release: Set Version v0.1.451 * kevm-pyk/: sync poetry files pyk version v0.1.451 * deps/k_release: sync release file version 6.0.119 * flake.{nix,lock}: update Nix derivations * deps/pyk_release: Set Version v0.1.452 * kevm-pyk/: sync poetry files pyk version v0.1.452 * flake.{nix,lock}: update Nix derivations * deps/pyk_release: Set Version v0.1.453 * kevm-pyk/: sync poetry files pyk version v0.1.453 * deps/k_release: sync release file version 6.0.120 * flake.{nix,lock}: update Nix derivations * kevm-pyk/src/kevm_pyk/kproj/plugin: Set Version 1aa2e24669529ea14d806d5b7f9116c65780f368 * deps/blockchain-k-plugin_release: sync release file version 1aa2e24669529ea14d806d5b7f9116c65780f368 * flake.{nix,lock}: update Nix derivations * deps/pyk_release: Set Version v0.1.454 * kevm-pyk/: sync poetry files pyk version v0.1.454 * flake.{nix,lock}: update Nix derivations * deps/pyk_release: Set Version v0.1.455 * kevm-pyk/: sync poetry files pyk version v0.1.455 * deps/k_release: sync release file version 6.0.121 * flake.{nix,lock}: update Nix derivations * deps/pyk_release: Set Version v0.1.456 * kevm-pyk/: sync poetry files pyk version v0.1.456 * flake.{nix,lock}: update Nix derivations * deps/pyk_release: Set Version v0.1.457 * kevm-pyk/: sync poetry files pyk version v0.1.457 * flake.{nix,lock}: update Nix derivations * Set Version: 1.0.309 * deps/pyk_release: Set Version v0.1.458 * kevm-pyk/: sync poetry files pyk version v0.1.458 * deps/k_release: sync release file version 6.0.124 * flake.{nix,lock}: update Nix derivations * deps/pyk_release: Set Version v0.1.459 * kevm-pyk/: sync poetry files pyk version v0.1.459 * flake.{nix,lock}: update Nix derivations * deps/blockchain-k-plugin_release: update to newest version * Set Version: 1.0.312 * kevm-pyk/: sync poetry files pyk version v0.1.459 * deps/blockchain-k-plugin_release: sync release file version c095983f3aec21c52f00b2d433202052ad7db104 * flake.{nix,lock}: update Nix derivations * bluckchain-k-plugin: update version * flake.{nix,lock}: update Nix derivations * deps/pyk_release: Set Version v0.1.460 * kevm-pyk/: sync poetry files pyk version v0.1.460 * deps/k_release: sync release file version 6.0.128 * flake.{nix,lock}: update Nix derivations * kevm-pyk/word: make sure #rangeUInt(5, ...) is defined * flake.{nix,lock}: update Nix derivations * deps/pyk_release: Set Version v0.1.461 * kevm-pyk/: sync poetry files pyk version v0.1.461 * deps/k_release: sync release file version 6.0.133 * flake.{nix,lock}: update Nix derivations * Set Version: 1.0.313 * kevm-pyk/: sync poetry files pyk version v0.1.461 * Set Version: 1.0.314 * Set Version: 1.0.315 * kevm-pyk/: sync poetry files pyk version v0.1.461 * Update expected output * kevm-pyk/: sync poetry files pyk version v0.1.461 --------- Co-authored-by: devops <devops@runtimeverification.com> Co-authored-by: Everett Hildenbrandt <everett.hildenbrandt@gmail.com> Co-authored-by: Tamás Tóth <tothtamas28@users.noreply.github.com> * Update Dockerfile (#2110) * Update Dockerfile Updating repository for image pull for z3 * Set Version: 1.0.316 --------- Co-authored-by: devops <devops@runtimeverification.com> * Make `kevm-dist` extensible (#2114) * Extract class `Target` and `KEVMTarget` * Use `Target` for building * Separate CLI, framework and targets * Load targets from plugins * Fix error message * Rename plugin group * Write directly to `output_dir` * Set Version: 1.0.317 --------- Co-authored-by: devops <devops@runtimeverification.com> * Extend prank rules for create (#2119) * extend prank rules for create * Set Version: 1.0.318 * Apply suggestions from code review Co-authored-by: Palina Tolmach <polina.tolmach@gmail.com> --------- Co-authored-by: devops <devops@runtimeverification.com> Co-authored-by: Palina Tolmach <polina.tolmach@gmail.com> * Remove `HASKELL_STANDALONE` and `FOUNDRY` from `KompileTarget` (#2121) * Remove `HASKELL_STANDALONE` and `FOUNDRY` from `KompileTarget` * Set Version: 1.0.318 * Set Version: 1.0.319 --------- Co-authored-by: devops <devops@runtimeverification.com> * Implement dependency handling for `kdist` (#2126) * Rename function `build` to `_build_target` * Extract function `build` * Remove parameter `command` * Add default values for parameters * Extract statement * Remove parameter `debug` * Refactor `build` * Remove unused private variable * Replace import * Make `DIST_DIR` private * Slide statements * Rename distribution directory * Add method `deps` to `Target` * Add optional parameter `deps` to `KEVMTarget.__init__` * Add `plugin` dependency to `llvm` * Do not expose loaded targets * Eliminate hard-coded dependency structure * Extract module `api` * Change parameter type * Add parameter `deps` to `build` * Inject dependency paths into build tasks * Set Version: 1.0.320 --------- Co-authored-by: devops <devops@runtimeverification.com> * Allow selecting fail_fast parameter for advance_proof (#2117) * Allow selecting fail_fast parameter for advance_proof * Set Version: 1.0.317 * Set Version: 1.0.318 * Set Version: 1.0.319 * Update kevm-pyk/src/kevm_pyk/cli.py Co-authored-by: Palina Tolmach <polina.tolmach@gmail.com> * Set Version: 1.0.320 * Set Version: 1.0.321 --------- Co-authored-by: devops <devops@runtimeverification.com> Co-authored-by: Palina Tolmach <polina.tolmach@gmail.com> * Disable testing of Foundry functionality (#2127) * .github/, package/version: remove tests of foundry functionality * Set Version: 1.0.320 * .github/test-pr: remove profile test which only ran kontrol tests * Revert ".github/test-pr: remove profile test which only ran kontrol tests" This reverts commit 4df1571. * kevm-pyk/src/tests/profiling/test_foundry_prove: remove test of kontrox functionality * Set Version: 1.0.322 --------- Co-authored-by: devops <devops@runtimeverification.com> * Use `Bytes` to represent byte strings instead of `String` (#2128) * Updated all calls to blockchain plugin to pass Bytes rather than String * Change rlpEncode/rlpDecode to use Bytes rather than String * Restore unintentionally deleted call to #unparseByteStack in #rplDecodeTransaction * Update verification.k for new Keccak256 interface * Add wrapper arounds new plugin interface. More pervasively use Bytes over Strings. * Set Version: 1.0.323 * Set Version: 1.0.323 * Formatting and small clean up. --------- Co-authored-by: devops <devops@runtimeverification.com> * Simplify job `kevm-pyk-profile` (#2132) * Simplify job `kevm-pyk-profile` This job no longer requires K, moved to public runner. * Set Version: 1.0.324 --------- Co-authored-by: devops <devops@runtimeverification.com> * Update dependency: deps/pyk_release (#2111) * deps/pyk_release: Set Version v0.1.463 * Set Version: 1.0.316 * kevm-pyk/: sync poetry files pyk version v0.1.463 * deps/k_release: sync release file version 6.0.138 * flake.{nix,lock}: update Nix derivations * deps/pyk_release: Set Version v0.1.464 * Set Version: 1.0.317 * kevm-pyk/: sync poetry files pyk version v0.1.464 * deps/k_release: sync release file version 6.0.139 * flake.{nix,lock}: update Nix derivations * deps/pyk_release: Set Version v0.1.465 * kevm-pyk/: sync poetry files pyk version v0.1.465 * deps/k_release: sync release file version 6.0.144 * flake.{nix,lock}: update Nix derivations * deps/pyk_release: Set Version v0.1.466 * kevm-pyk/: sync poetry files pyk version v0.1.466 * deps/k_release: sync release file version 6.0.145 * flake.{nix,lock}: update Nix derivations * deps/pyk_release: Set Version v0.1.467 * kevm-pyk/: sync poetry files pyk version v0.1.467 * flake.{nix,lock}: update Nix derivations * deps/pyk_release: Set Version v0.1.468 * kevm-pyk/: sync poetry files pyk version v0.1.468 * deps/k_release: sync release file version 6.0.146 * flake.{nix,lock}: update Nix derivations * deps/pyk_release: Set Version v0.1.469 * kevm-pyk/: sync poetry files pyk version v0.1.469 * flake.{nix,lock}: update Nix derivations * deps/pyk_release: Set Version v0.1.470 * kevm-pyk/: sync poetry files pyk version v0.1.470 * flake.{nix,lock}: update Nix derivations * Set Version: 1.0.318 * deps/pyk_release: Set Version v0.1.471 * kevm-pyk/: sync poetry files pyk version v0.1.471 * deps/k_release: sync release file version 6.0.148 * flake.{nix,lock}: update Nix derivations * deps/pyk_release: Set Version v0.1.472 * Set Version: 1.0.319 * kevm-pyk/: sync poetry files pyk version v0.1.472 * deps/k_release: sync release file version 6.0.150 * flake.{nix,lock}: update Nix derivations * deps/pyk_release: Set Version v0.1.473 * kevm-pyk/: sync poetry files pyk version v0.1.473 * deps/k_release: sync release file version 6.0.152 * flake.{nix,lock}: update Nix derivations * deps/pyk_release: Set Version v0.1.474 * kevm-pyk/: sync poetry files pyk version v0.1.474 * deps/k_release: sync release file version 6.0.153 * flake.{nix,lock}: update Nix derivations * Set Version: 1.0.320 * update poetry.lock * add inotify dependency * add fixture to run kserver * kevm-pyk/: sync poetry files pyk version v0.1.474 * create dir if it doesn't exist * deps/pyk_release: Set Version v0.1.475 * Set Version: 1.0.321 * kevm-pyk/: sync poetry files pyk version v0.1.475 * deps/k_release: sync release file version 6.0.156 * flake.{nix,lock}: update Nix derivations * Set Version: 1.0.323 * EXPERIMENT: reduce test parallelism to 4 * EXPERIMENT: remove normal label for runners * Revert "EXPERIMENT: reduce test parallelism to 4" This reverts commit e8a5a6f. * EXPERIMENT: reduce test parallelism to 4 * Set Version: 1.0.324 * kevm-pyk/: sync poetry files pyk version v0.1.475 * use newer pyk version * kevm-pyk/: sync poetry files pyk version v0.1.477 * deps/k_release: sync release file version 6.0.161 * flake.{nix,lock}: update Nix derivations * limit max_depth to 300 in pyk_prove tests (workaround) * run proof tests with different parallelism degree * deps/pyk_release: Set Version v0.1.478 * kevm-pyk/: sync poetry files pyk version v0.1.478 * deps/k_release: sync release file version 6.0.163 * flake.{nix,lock}: update Nix derivations * Revert "run proof tests with different parallelism degree" This reverts commit c8d2eaa. * Set Version: 1.0.325 --------- Co-authored-by: devops <devops@runtimeverification.com> Co-authored-by: Dwight Guth <dwight.guth@runtimeverification.com> Co-authored-by: Jost Berthold <jost.berthold@gmail.com> Co-authored-by: Everett Hildenbrandt <everett.hildenbrandt@gmail.com> * Use Proof names and IDs in bug report archives (#2125) * provide an ID when creating KoreClient * Set Version: 1.0.326 --------- Co-authored-by: devops <devops@runtimeverification.com> * Better directory management for `kdist` (#2134) * Lock target directories for `kevm-dist build` * Switch to `ProcessPoolExecutor` * Run build in temporary directory * Set Version: 1.0.327 --------- Co-authored-by: devops <devops@runtimeverification.com> * Remove testing infrastructure related to kontrolx (#2135) * .gitignore, tests/specs/examples: commit bin-runtime files * kevm-pyk/test_prove: simplify compilation process now that we dont need to generate K code * .gitmodules: remove forge-std * kevm-pyk/: remove more references to foundry tests * kevm-pyk/src/tests/integration/test-data: remove references to foundry tests * kevm-pyk/src/tests/integration/test_{foundry_prove,solc_to_k}: remove unused files * Set Version: 1.0.326 * tests/foundry/lib/forge-std: remove submodule * Set Version: 1.0.328 --------- Co-authored-by: devops <devops@runtimeverification.com> * Set Version: 1.0.329 * Set Version: 1.0.343 * Set Version: 1.0.344 * Set Version: 1.0.345 --------- Co-authored-by: devops <devops@runtimeverification.com> Co-authored-by: rv-jenkins <admin@runtimeverification.com> Co-authored-by: Everett Hildenbrandt <everett.hildenbrandt@gmail.com> Co-authored-by: qian-hu <88806138+qian-hu@users.noreply.github.com> Co-authored-by: Petar Maksimovic <petar.maksimovic@runtimeverification.com> Co-authored-by: Petar Maksimović <PetarMax@users.noreply.github.com> Co-authored-by: Palina Tolmach <polina.tolmach@gmail.com> Co-authored-by: Noah Watson <107630091+nwatson22@users.noreply.github.com> Co-authored-by: Tamás Tóth <tothtamas28@users.noreply.github.com> Co-authored-by: Freeman <105403280+F-WRunTime@users.noreply.github.com> Co-authored-by: Andrei Văcaru <16517508+anvacaru@users.noreply.github.com> Co-authored-by: Scott Guest <scott.guest@runtimeverification.com> Co-authored-by: Dwight Guth <dwight.guth@runtimeverification.com> Co-authored-by: Jost Berthold <jost.berthold@gmail.com> Co-authored-by: Andrei <andrei.vacaru@runtimeverification.com>

qian-hu and others added 6 commits May 26, 2023 23:56

Add notMaxUInt constants

aa76e2c

Add bitwise-arithmetic lemmas

8327f39

Upstream bytes-simplification lemmas from Wormhole

26a1589

Upstream lemmas from Wormhole engagement

22f8392

Set Version: 1.0.187

f45dcab

Revert "Upstream lemmas from Wormhole engagement"

dcca53c

This reverts commit 22f8392.

qian-hu self-assigned this May 27, 2023

ehildenb reviewed May 30, 2023

View reviewed changes

include/kframework/word.md Outdated Show resolved Hide resolved

PetarMax self-requested a review June 1, 2023 14:17

PetarMax reviewed Jun 1, 2023

View reviewed changes

include/kframework/lemmas/bitwise-simplification.k Outdated Show resolved Hide resolved

PetarMax reviewed Jun 1, 2023

View reviewed changes

include/kframework/lemmas/bitwise-simplification.k Outdated Show resolved Hide resolved

PetarMax reviewed Jun 1, 2023

View reviewed changes

include/kframework/lemmas/bytes-simplification.k Outdated Show resolved Hide resolved

PetarMax reviewed Jun 1, 2023

View reviewed changes

include/kframework/lemmas/bytes-simplification.k Outdated Show resolved Hide resolved

qian-hu and others added 17 commits June 14, 2023 12:56

Merge branch 'master' into wormhole-lemmas

1812eb9

Set Version: 1.0.210

a975eb5

Update include/kframework/word.md

2f1dfaf

Co-authored-by: Everett Hildenbrandt <everett.hildenbrandt@gmail.com>

Merge branch 'master' into wormhole-lemmas

214859c

Set Version: 1.0.211

eab32d5

Merge remote-tracking branch 'origin/master' into wormhole-lemmas

7137fac

Set Version: 1.0.212

97e4f9e

Merge branch 'master' into wormhole-lemmas

5789fc0

Set Version: 1.0.213

3a66b8e

Merge branch 'master' into wormhole-lemmas

93abade

Merge branch 'master' into wormhole-lemmas

ad7f4a4

Set Version: 1.0.219

c79870e

Merge branch 'master' into wormhole-lemmas

17bd534

Set Version: 1.0.227

384077f

Merge branch 'master' into wormhole-lemmas

e0b8a2d

Set Version: 1.0.228

5fd741c

generalize lemmas

e8814f3

qian-hu and others added 4 commits August 8, 2023 13:02

Merge branch 'master' into wormhole-lemmas

9b7bb4f

Set Version: 1.0.249

ec5beed

Merge branch 'master' into wormhole-lemmas

533dc1d

Set Version: 1.0.296

63c4407

PetarMax and others added 3 commits October 2, 2023 10:53

merge with master

d9262f5

Set Version: 1.0.309

4a80da5

cleanup

8cad2bb

PetarMax mentioned this pull request Oct 2, 2023

Lemmas on Boolean reasoning, set reasoning, map lookup #2037

Merged

PetarMax and others added 3 commits October 2, 2023 12:35

simplification fix

3365bcd

Merge branch 'master' into wormhole-lemmas

f575742

Set Version: 1.0.310

10f6b18

PetarMax marked this pull request as ready for review October 2, 2023 11:29

removing simplification

4a726fa

qian-hu requested a review from PetarMax October 2, 2023 15:36

qian-hu added 4 commits October 2, 2023 19:24

Fix simplification

5647759

Add claims for lemmas

b3f8251

Update bytes-simplification.k

8e0ff8c

Add more claims for lemmas

7d00d95

PetarMax reviewed Oct 3, 2023

View reviewed changes

PetarMax approved these changes Oct 3, 2023

View reviewed changes

PetarMax merged commit b1de680 into master Oct 3, 2023

PetarMax deleted the wormhole-lemmas branch October 3, 2023 10:36

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Upstream lemmas from Wormhole engagement #1866

Upstream lemmas from Wormhole engagement #1866

qian-hu commented May 27, 2023

palinatolmach commented Sep 22, 2023

palinatolmach commented Sep 28, 2023

PetarMax commented Oct 2, 2023

ehildenb commented Oct 2, 2023

PetarMax commented Oct 2, 2023

qian-hu commented Oct 3, 2023

PetarMax Oct 3, 2023

Upstream lemmas from Wormhole engagement #1866

Upstream lemmas from Wormhole engagement #1866

Conversation

qian-hu commented May 27, 2023

palinatolmach commented Sep 22, 2023

palinatolmach commented Sep 28, 2023

PetarMax commented Oct 2, 2023

ehildenb commented Oct 2, 2023

PetarMax commented Oct 2, 2023

qian-hu commented Oct 3, 2023

PetarMax Oct 3, 2023

Choose a reason for hiding this comment