Skip to content

Commit b4bedbe

Browse files
LysxiaLysxia
authored
Release 0.4 (#1389)
2 parents 3efadc9 + ee88f7b commit b4bedbe

File tree

16 files changed

+131
-32
lines changed

16 files changed

+131
-32
lines changed

‎CHANGELOG.md

Lines changed: 98 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -11,6 +11,104 @@ Creusot is currently best suited for the verification of code like data-structur
1111
<!-- next-header -->
1212

1313
## [Unreleased] - ReleaseDate
14+
15+
## [0.4.0] - 2025-03-03
16+
17+
### Main features
18+
19+
#### Bitwise mode
20+
21+
The new `#[bitwise_proof]` attribute makes Creusot interpret machine integers as bit vectors instead of bounded integers,
22+
giving meaning to bitwise operations.
23+
Bitwise operators have an abstract specification when this attribute is not on.
24+
25+
Along with this feature, Pearlite is also extended with:
26+
27+
- arithmetic operations on machine integers, with a wrapping semantics;
28+
- casts (`n as usize`).
29+
30+
Thanks to Laurent Schneider @laurentder.
31+
32+
#### Closure inference
33+
34+
Contracts for closures can now be omitted, to be inferred through Coma's novel `extspec` mechanism.
35+
36+
#### Prove with Why3find
37+
38+
The new command `cargo creusot prove` launches Why3find to automatically
39+
generate proofs. This removes the need for manually editing sessions through
40+
the Why3 IDE. The Why3 IDE remains useful to debug incomplete proofs,
41+
via `cargo creusot prove -i`.
42+
43+
This more automated solution prevents the use of manual transformations,
44+
such as `exists` to instantiate existential quantifiers.
45+
This may require restructuring code to be more proof-friendly.
46+
There are known challenges of that sort surrounding the specification
47+
of iterators in `creusot-contracts`.
48+
49+
#### Documentation
50+
51+
- The [Creusot tutorial](https://creusot-rs.github.io/creusot/guide/tutorial.html) is an introduction to verify Rust programs with Creusot.
52+
- The `creusot-contracts` API documentation is [available online](https://creusot-rs.github.io/creusot/doc/creusot_contracts/). It contains information about Creusot's attributes and macros (supplementing the [guide](https://creusot-rs.github.io/creusot/guide/)), and lists available functions and methods along with their contracts, including logic functions (which would be omitted by a simple `cargo doc`).
53+
54+
### Other improvements
55+
56+
#### Installation
57+
58+
The new `./INSTALL` script handles installing Creusot and tools (Why3, Why3find, and SMT solvers). It assumes that `cargo` and `opam` are installed.
59+
In particular, `./INSTALL` creates an Opam switch dedicated to Creusot to ensure Why3 and Why3find remain available at their expected versions.
60+
61+
Just run `./INSTALL`.
62+
63+
#### Setting up new projects
64+
65+
The `cargo creusot new` and `cargo creusot init` generate the boilerplate to
66+
get you started with a new verified Rust project.
67+
68+
#### Build with stable Rust compiler
69+
70+
Rust code containing Creusot contracts can now be compiled with a stable Rust compiler.
71+
This is made possible by the following changes:
72+
73+
- make `creusot-contracts` buildable with a stable Rust compiler;
74+
- hide `#[invariant(...)]` attributes, whose parsing requires the unstable features `proc_macro_hygiene` and `stmt_expr_attributes`.
75+
76+
#### Coma
77+
78+
Type translations are inlined in modules that use them. With this change, every Rust function is translated to a standalone module.
79+
80+
Improved metadata on goals: source spans are more accurate and labels are more informative (ensures, requires, and invariants are numbered).
81+
82+
The `prelude` (the Coma library imported by Creusot-translated artifacts) has been renamed to `creusot`.
83+
84+
### Standard library (`creusot-contracts`)
85+
86+
- Add extern specs for `get_unchecked` and `get_unchecked_mut` (slice methods) (#1382).
87+
- Add `Mapping::index_logic` (you can write `f[x]`) and `such_that` (#1296).
88+
- Implement `Clone` on `Seq`, `FMap`, `FSet` (#1289).
89+
- Add `FMap::index_logic` (#1254).
90+
- Rename `Seq::{push,pop}` to `{push_back,pop_back}`, add `{push_front,pop_front}` (#1224).
91+
- Add `std::cmp` and `Ord` functions (#1305).
92+
- Add specs for `HashSet`, `FSet`, and some iterators (ranges, `filter_map`, `rev`) (#1313).
93+
- Implement `View`, `DeepModel`, and `Default` for `char` (#1381).
94+
95+
#### Iterators
96+
97+
- Add `Iterator` impls for `[T;N]` and `&mut I` (#1290).
98+
- Add specs for iterators of `HashMap` and `HashSet` (#1306).
99+
- Remove redundant `inv` in iterator specs (#1291).
100+
101+
#### Ghosts
102+
103+
- Add `PCell`: interior mutability with ghost ownership (#1262).
104+
- Enable logic data structures to be used in ghost code (#1073).
105+
- Add `Int` literals for ghost code, e.g, `1int` (#1256).
106+
- Allow arithmetic operators on `Int` in ghost code (#1281).
107+
- Add specs for raw pointers and ghost ownership for pointers (#1169).
108+
- Add `FMap::split_mut_ghost` (#1356).
109+
- Fix spec of `FMap::get_mut_ghost` (#1253).
110+
- Strengthen `PtrOwn::disjoint_lemma` (#1295).
111+
14112
## [0.3.0] - 2024-10-27
15113

16114
### Cargo Creusot

‎Cargo.lock

Lines changed: 14 additions & 14 deletions
Some generated files are not rendered by default. Learn more about customizing how changed files appear on GitHub.

‎cargo-creusot/Cargo.toml

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
[package]
22
name = "cargo-creusot"
3-
version = "0.3.0"
3+
version = "0.4.0"
44
edition = "2024"
55
publish = false
66

‎creusot-args/Cargo.toml

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
[package]
22
name = "creusot-args"
3-
version = "0.3.0"
3+
version = "0.4.0"
44
edition = "2024"
55
publish = false
66

‎creusot-contracts-dummy/Cargo.toml

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
[package]
22
name = "creusot-contracts-dummy"
3-
version = "0.3.0"
3+
version = "0.4.0"
44
edition = "2021"
55
homepage = "https://github.com/creusot-rs/creusot"
66
license = "LGPL-2.1-or-later"

‎creusot-contracts-proc/Cargo.toml

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
[package]
22
name = "creusot-contracts-proc"
3-
version = "0.3.0"
3+
version = "0.4.0"
44
authors = ["Xavier Denis <[email protected]>"]
55
edition = "2018"
66
repository = "https://github.com/creusot-rs/creusot"
@@ -14,7 +14,7 @@ proc-macro = true
1414
[dependencies]
1515
quote = "1.0"
1616
uuid = { version = "1.12", features = ["v4"] }
17-
pearlite-syn = { version = "0.3", path = "../pearlite-syn", features = ["full"] }
17+
pearlite-syn = { version = "0.4", path = "../pearlite-syn", features = ["full"] }
1818
syn = { version = "2.0"}
1919
proc-macro2 = "1.0"
2020

‎creusot-contracts/Cargo.toml

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
[package]
22
name = "creusot-contracts"
3-
version = "0.3.0"
3+
version = "0.4.0"
44
authors = ["Xavier Denis <[email protected]>"]
55
edition = "2018"
66
homepage = "https://github.com/creusot-rs/creusot"
@@ -11,10 +11,10 @@ description = "Provides contracts and logic helpers for Creusot"
1111

1212
[target.'cfg(creusot)'.dependencies]
1313
num-rational = "0.4"
14-
creusot-contracts-proc = { path = "../creusot-contracts-proc", version = "0.3.0" }
14+
creusot-contracts-proc = { path = "../creusot-contracts-proc", version = "0.4.0" }
1515

1616
[target.'cfg(not(creusot))'.dependencies]
17-
creusot-contracts-dummy = { path = "../creusot-contracts-dummy", version = "0.3.0" }
17+
creusot-contracts-dummy = { path = "../creusot-contracts-dummy", version = "0.4.0" }
1818

1919
[features]
2020
# Enabled by creusot.

‎creusot-dev-config/Cargo.toml

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
[package]
22
name = "creusot-dev-config"
3-
version = "0.3.0"
3+
version = "0.4.0"
44
edition = "2024"
55
publish = false
66

‎creusot-install/Cargo.toml

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,8 @@
11
[package]
22
name = "creusot-install"
3-
version = "0.1.0"
3+
version = "0.4.0"
44
edition = "2021"
5+
publish = false
56

67
[dependencies]
78
clap = { version = "4.5", features = ["derive", "env"] }

‎creusot-metadata/Cargo.toml

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
[package]
22
name = "creusot-metadata"
3-
version = "0.3.0"
3+
version = "0.4.0"
44
edition = "2024"
55
publish = false
66

‎creusot-rustc/Cargo.toml

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,14 +1,14 @@
11
[package]
22
name = "creusot-rustc"
3-
version = "0.3.0"
3+
version = "0.4.0"
44
edition = "2024"
55
publish = false
66

77
# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
88

99
[dependencies]
1010
serde_json = { version = "1.0" }
11-
creusot = { path = "../creusot", version = "0.3" }
11+
creusot = { path = "../creusot", version = "0.4" }
1212
toml = "0.8"
1313
env_logger = "0.11"
1414
serde = { version = "1.0", features = ["derive"] }

‎creusot-setup/Cargo.toml

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
[package]
22
name = "creusot-setup"
3-
version = "0.3.0"
3+
version = "0.4.0"
44
edition = "2024"
55
publish = false
66

‎creusot/Cargo.toml

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
[package]
22
name = "creusot"
3-
version = "0.3.0"
3+
version = "0.4.0"
44
authors = ["Xavier Denis <[email protected]>"]
55
edition = "2024"
66
license = "LGPL-2.1-or-later"

‎pearlite-syn/Cargo.toml

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
[package]
22
name = "pearlite-syn"
3-
version = "0.3.0"
3+
version = "0.4.0"
44
edition = "2024"
55
license = "MIT OR Apache-2.0"
66
repository = "https://github.com/creusot-rs/creusot"

‎why3/Cargo.toml

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
[package]
22
name = "why3"
3-
version = "0.3.0"
3+
version = "0.4.0"
44
authors = ["Xavier Denis <[email protected]>"]
55
edition = "2024"
66
repository = "https://github.com/creusot-rs/creusot"

‎why3tests/Cargo.toml

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
[package]
22
name = "why3tests"
3-
version = "0.3.0"
3+
version = "0.4.0"
44
edition = "2024"
55
publish = false
66

0 commit comments

Comments
 (0)