Repository navigation
Tags
Tags
[ci] Pin Kani job to ubuntu-24.04 runner GitHub Actions' rollout of the ubuntu-26.04 runner image for ubuntu-latest upgraded the default system compiler to GCC 15. In GCC 15, <stddef.h> introduces C23 `typedef __typeof__(nullptr) nullptr_t;`. CBMC's goto-cc compiler wrapper in Kani 0.60.0 fails to parse this C23 symbol in system headers, failing Kani verification jobs with: `error: failed to find symbol 'nullptr'`. Pin the `kani` job in .github/workflows/ci.yml to ubuntu-24.04 so Kani runs against GCC 13/14 headers where `nullptr` is not present in C mode. gherrit-pr-id: Gt4vhuy7vi5cegikntednwwsuospcpdnp Agent-authored-by: AI agent acting on joshlf's behalf
[exocrate] Bump to 0.3.0 Bump `exocrate` from 0.1.0 to 0.3.0, and add package metadata (`description`, `license`, and `repository`) to `exocrate/Cargo.toml`. Synchronize the updated version in `exocrate/Cargo.lock`, `anneal/Cargo.lock`, and `anneal/v1/Cargo.lock`. gherrit-pr-id: Gdyb42ih4bwueat7h4gts2tqudohw3r6v Agent-authored-by: AI agent acting on joshlf's behalf
[ci] Audit all commits in origin/main..HEAD for XODO markers On pull_request triggers, actions/checkout checks out GitHub's synthetic merge ref (refs/remotes/pull/<PR>/merge) with fetch-depth: 1, whose commit message is 'Merge <head> into <base>'. As a result, inspecting only git log -1 --pretty=%B on HEAD missed XODO markers in the PR's own commit messages (and in earlier commits of a multi-commit PR or stack). Fetch full history (fetch-depth: 0) in check-todo and update ci/check_todo.sh to enumerate all commits in origin/main..HEAD (falling back to HEAD when on main itself), auditing both the commit message and tracked file tree of each commit. Do not pass --no-merges: on a GitHub pull_request checkout, HEAD is a synthetic merge of main (HEAD^1) and the PR tip (HEAD^2), so origin/main..HEAD traverses HEAD^2 to audit every commit in the PR (including authored merge commits) as well as the merged tree at HEAD. gherrit-pr-id: Gqqvieb2pqp2bcmej7ch7x4mwzcdndsdf Agent-authored-by: AI agent acting on joshlf's behalf
[ci] Audit all commits in origin/main..HEAD for XODO markers On pull_request triggers, actions/checkout checks out GitHub's synthetic merge ref (refs/remotes/pull/<PR>/merge) with fetch-depth: 1, whose commit message is 'Merge <head> i D055 nto <base>'. As a result, inspecting only git log -1 --pretty=%B on HEAD missed XODO markers in the PR's own commit messages (and in earlier commits of a multi-commit PR or stack). Fetch full history (fetch-depth: 0) in check-todo and update ci/check_todo.sh to enumerate all non-merge commits in origin/main..HEAD (falling back to HEAD when on main itself), auditing both the commit message and tracked file tree of each commit. gherrit-pr-id: Gqqvieb2pqp2bcmej7ch7x4mwzcdndsdf Agent-authored-by: AI agent acting on joshlf's behalf
[WIP] Introduce `TryFromBytes::Uninit` gherrit-pr-id: Geec83fc8d47be6b2e51a15b84a2735bbc909ce68
[wip] Introduce `Ptr::project_map` Enables piecewise initialization. gherrit-pr-id: Gc3e9ee9afa6945e10c35be84d30c970894395c96
Require initialized storage for uninhabited `AsInitialized` referents Require all bytes, including padding, to be initialized when no valid instance of the referent type exists at its length. This closes the vacuous case in AsInitialized without changing inhabited referents. gherrit-pr-id: G8e817072d200a742ce8c9e388e161142f04f2654
[WIP] Introduce compound `Ptr` validity ..and implement projection for compound-valid tuples. gherrit-pr-id: G06edd27f8b77b5ad480ca94749098bb4b0808342 Agent-authored-by: AI agent acting on Jack Wrenn's behalf (content only)
Prove the numerical bounds used by split operations Factor the split-length calculation and zero-padding decision into proved helpers used by the production pointer paths. A Rust assertion harness compares complete sizes with the independent reference and checks physical tail containment. Prove counts, bounds and disjoint numerical intervals, including empty and zero-sized tails, under the visible witness and containment guards. Pointer validity, provenance and access permissions remain separate Rust obligations. Refresh UI diagnostics for the shifted source lines. gherrit-pr-id: Gytt7syk4w4f52xlmszabgwlaiofsu7p6 Agent-authored-by: AI agent acting on joshlf's behalf
Prove the numerical bounds used by split operations Factor the split-length calculation and zero-padding decision into proved helpers used by the production pointer paths. A Rust assertion harness compares complete sizes with the independent reference and checks physical tail containment. Prove counts, bounds and disjoint numerical intervals, including empty and zero-sized tails, under the visible witness and containment guards. Pointer validity, provenance and access permissions remain separate Rust obligations. Refresh UI diagnostics for the shifted source lines. gherrit-pr-id: Gytt7syk4w4f52xlmszabgwlaiofsu7p6 Agent-authored-by: AI agent acting on joshlf's behalf
PreviousNext