Skip to content

Releases: runtimeverification/riscv-semantics

v0.1.104: Add `optimize_kcfg` parameter in `SymTool` (#134)

13 Jun 06:59
db011d7

Choose a tag to compare

This is needed when the `max_depth` is small but `max_iteractions` is
big.

---------

Co-authored-by: devops <[email protected]>
Co-authored-by: Tamás Tóth <[email protected]>

v0.1.103: Simp rule 4 `(A +Int B) &Int 4294967295 <Int A` (#130)

12 Jun 14:58
c72b80f

Choose a tag to compare

Also fix a bug for `bytes2int-upperbound`

---------

Co-authored-by: devops <[email protected]>
Co-authored-by: Tamás Tóth <[email protected]>

v0.1.102: Update dependency: deps/k_release (#127)

11 Jun 14:53
0d09047

Choose a tag to compare

v0.1.101: Add extensible prover implementation (#103)

11 Jun 14:39
fca8f9f

Choose a tag to compare

This PR introduces a module `kprovex` that defines an extensible prover
based on `APRPRover`. It has the the following submodules:
* `kprovex.api`: the plugin API definition. A plugin provides the K
definition to the prover, as well as functions for loading and printing
proofs of that definition.
* `kprovex._default`: semantics-agnostic defaults for loading and
printing proofs.
* `kprovex._loader`: plugin loader.
* `kprovex._kprovex`: prover implementation.

Furthermore, it adds a simple plugin implementation for
`riscv-semantics`.

The advantage of this architecture is that `kprovex` can be upstreamed
to `pyk` without breaking it or the `riscv-semantics` prover.
(Naturally, imports still need to be adjusted.)

---------

Co-authored-by: devops <[email protected]>

v0.1.100: fix version of `uv` in CI (#133)

11 Jun 13:13
fb931c8

Choose a tag to compare

Fix version of `uv` in CI. The version is derived from the `uv2nix`
repository even though there is no official nix support for this
repository yet. This will be required for a future implementation of a
nix derivation for `riscv-semantics` anyway.

---------

Co-authored-by: devops <[email protected]>

v0.1.99: Fix version in `uv.lock` (#131)

11 Jun 12:30
c77e2a5

Choose a tag to compare

v0.1.98: Add simp rules for revsersed `substrBytes` concat (#128)

10 Jun 13:46
570e0f4

Choose a tag to compare

v0.1.97

10 Jun 13:31
2fc0603

Choose a tag to compare

Add simp rules 4 `Bytes2Int o Int2Bytes` and `substrBytes o Int2Bytes…

v0.1.96: Migrate from `poetry` to `uv` (#125)

04 Jun 14:42
711f12b

Choose a tag to compare

v0.1.95: Remove attribute `source_dir` from `SymTools` (#126)

03 Jun 09:27
07180df

Choose a tag to compare

A claim can be loaded even if the source of the definition is not
included, as long as it is not explicitly required by the specification.

---------

Co-authored-by: devops <[email protected]>