Skip to content

Releases: runtimeverification/komet

v0.1.57: `komet prove` options for advanced users (#64)

18 Feb 10:02
548aeea
Compare
Choose a tag to compare
* 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)

06 Feb 18:02
2a143ed
Compare
Choose a tag to compare
* 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)

06 Feb 15:27
cbfb8fc
Compare
Choose a tag to compare
* 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)

04 Feb 14:02
f240ca0
Compare
Choose a tag to compare
* 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)

04 Feb 10:43
bddbd66
Compare
Choose a tag to compare
* 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)

04 Feb 10:02
12c938f
Compare
Choose a tag to compare
* 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)

04 Feb 09:26
7fe5db5
Compare
Choose a tag to compare
* 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)

10 Jan 08:28
9d24395
Compare
Choose a tag to compare
* 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)

10 Jan 07:48
a12f3bb
Compare
Choose a tag to compare
* 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)

10 Jan 07:20
19f8fcd
Compare
Choose a tag to compare
* 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>