Releases: runtimeverification/komet
Releases · runtimeverification/komet
v0.1.57: `komet prove` options for advanced users (#64)
* implement `--extra-module` * implement `--view-node` and `--remove-node` * add progress display to `komet prove run` * Set Version: 0.1.57 --------- Co-authored-by: devops <devops@runtimeverification.com>
v0.1.56: Update dependency: deps/kwasm_release (#63)
* deps/kwasm_release: Set Version 0.1.120 * Set Version: 0.1.55 * Sync Poetry files 0.1.120 * flake.{nix,lock}: update Nix derivations * Set Version: 0.1.56 --------- Co-authored-by: devops <devops@runtimeverification.com> Co-authored-by: Burak Bilge Yalçınkaya <bbyalcinkaya@gmail.com>
v0.1.55: Test harness for lemmas (#60)
* implement the harness * add lemma tests * Set Version: 0.1.51 * add CI job for lemma tests * format * update soroban sdk * Fix typo Co-authored-by: Everett Hildenbrandt <everett.hildenbrandt@runtimeverification.com> * Set Version: 0.1.55 * add `EqualityProof` support --------- Co-authored-by: devops <devops@runtimeverification.com> Co-authored-by: Everett Hildenbrandt <everett.hildenbrandt@runtimeverification.com>
v0.1.54: Update dependency: deps/kwasm_release (#59)
* deps/kwasm_release: Set Version 0.1.119 * Set Version: 0.1.51 * Sync Poetry files 0.1.119 * deps/k_release: sync release file version 7.1.191 * flake.{nix,lock}: update Nix derivations * Set Version: 0.1.54 * Sync Poetry files 0.1.119 * flake.{nix,lock}: update Nix derivations --------- Co-authored-by: devops <devops@runtimeverification.com> Co-authored-by: Burak Bilge Yalçınkaya <bbyalcinkaya@gmail.com>
v0.1.53: Add `--always-allocate` Flag to Reduce Branching (#58)
* add config cell and cli option * add semantics * add test and lemmas * Set Version: 0.1.51 * Set Version: 0.1.52 * Set Version: 0.1.53 --------- Co-authored-by: devops <devops@runtimeverification.com> Co-authored-by: automergerpr-permission-manager[bot] <190534181+automergerpr-permission-manager[bot]@users.noreply.github.com>
v0.1.52: Add host functions for `Bytes` operations (#61)
* implement `bytes_copy_from_linear_memory` * implement `bytes_new` * implement `bytes_put` * implement `bytes_get` * refactor `bytes_copy_from_linear_memory` * implement `bytes_del` * refactor hostcall implementations to use `hostCallAux` * implement `bytes_push` * implement `bytes_pop` * implement `bytes_front` `bytes_back` * implement `bytes_insert` * implement `bytes_append` * implement `bytes_slice` * allow 0 length in `bytes_insert` * add property tests * Set Version: 0.1.51 * update soroban sdk * implement `symbol_len` * Set Version: 0.1.52 --------- Co-authored-by: devops <devops@runtimeverification.com> Co-authored-by: automergerpr-permission-manager[bot] <190534181+automergerpr-permission-manager[bot]@users.noreply.github.com>
v0.1.51: Add new vector operations and some refactoring (#62)
* update soroban sdk * refactor using `hostCallAux` * refactor `vec.wast` test * implement `vec_put` * implement `vec_del` * implement `vector_push_front` and some refactoring * implement `vec_pop_front` `vec_pop_back` * implement `vec_front` `vec_back` * implement `vec_insert` * implement `vec_append` * implement `vec_slice` * Set Version: 0.1.51 --------- Co-authored-by: devops <devops@runtimeverification.com>
v0.1.50: Update dependency: deps/kwasm_release (#51)
* deps/kwasm_release: Set Version 0.1.116 * Set Version: 0.1.46 * Sync Poetry files 0.1.116 * deps/k_release: sync release file version 7.1.182 * flake.{nix,lock}: update Nix derivations * Sync Poetry files 0.1.116 * Sync Poetry files 0.1.116 * deps/kwasm_release: Set Version 0.1.117 * Sync Poetry files 0.1.117 * deps/k_release: sync release file version 7.1.186 * flake.{nix,lock}: update Nix derivations * Set Version: 0.1.50 * Sync Poetry files 0.1.117 * flake.{nix,lock}: update Nix derivations --------- Co-authored-by: devops <devops@runtimeverification.com> Co-authored-by: Burak Bilge Yalçınkaya <bbyalcinkaya@gmail.com>
v0.1.49: Improve `komet test` UI with progress bar and failure reporting (#56)
* add progress bar * display failing tests * refactor fuzzer to map individual arguments to strategies * output falsifying examples * Set Version: 0.1.48 * run pyupgrade * format * `falsifying_example => counterexample` * Set Version: 0.1.49 --------- Co-authored-by: devops <devops@runtimeverification.com>
v0.1.48: Implement Remaining Map Host Functions (#54)
* implement `map_key_by_pos`, `map_val_by_pos` * implement `map_keys` and `map_vals` * Set Version: 0.1.48 --------- Co-authored-by: devops <devops@runtimeverification.com>