Skip to content

Commit d67fb76

Browse files
SebTardifSebTardif
authored
fix(cli): JSON envelopes, MCP jail, and vacuous polarity (#1528)
## Summary MPI Cycle 1 (all 14 perspectives) plus Cycle 2 Test Auditor and Developer on one session branch. Agent-facing JSON, MCP jail, vacuous polarity, Windows CLI tests, and CI pins. ## Product / agent contract - Vacuous infer and check now use success: true plus acuous: true (exit 0). Agents should branch on acuous, not on success. - CLI check --json keeps ile_info.vacuous and also emits top-level success / acuous / acuous_reason (shared �ssura_pipeline::vacuous_status). - check-rust JSON includes success next to ok. - infer --json -o write-ok envelopes include success and ok (status: ok remains as an alias). - MCP �ssura_infer returns a JSON envelope. Write esult.text to a .assura file, not the whole object. - MCP file jail: relative to process cwd, extensions .assura / .rs / .ir, post-canonicalize extension check (symlink leak.rs to .env is rejected). - Jail and resolve errors are JSON with �rror_kind: PATH_NOT_ALLOWED, SOURCE_TOO_LARGE, SOURCE_NOT_UTF8, MISSING_SOURCE, PROMPT_FAILED. - Source reads capped at 16 MiB with ake(max+1) on CLI, MCP, and check-rust. - infer --function applies to .rs sources (unknown name exits 1). - �udit --timeout is honored via �erify_typed. - �erify.solver is accepted as an alias of smt-solver. ## Correctness / CI - Parallel SMT verify injects sibling lemmas (same as the non-parallel path). - Codegen float/u128 detection walks all expression children. - check-rust directory scan fails closed on unparseable .rs and names the file. - Auto-approve allowlists Dependabot and assura-auto-approve bots (not any [bot]). - CVC5 prebuilt pin cvc5-1.3.1; rust-cache v2.9.2; mdBook 0.5.4; fuzz nightly pin. - Dependabot ignore floors for ariadne >=0.7 and z3 >=0.21. - LLM HTTP and parse errors do not dump provider bodies (�xtract_json no longer panics when } precedes {). ## Windows - workspace_root() walks two parents from CARGO_MANIFEST_DIR (no Unix-slash replace). - Write-fail tests use a file-as-parent path so mkdir fails on Windows and Unix. ## Held Release-please #1519 (0.4.4) is not part of this PR. Do not merge it without an explicit yes. Human/upstream leftovers unchanged: #1410, #1411, #1396, #436. --------- Signed-off-by: Sebastien Tardif <SebTardif@ncf.ca>
1 parent 053e9fe commit d67fb76

65 files changed

Lines changed: 3644 additions & 507 deletions

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

‎.github/actions/setup-rust-ci/action.yml‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -21,7 +21,7 @@ runs:
2121
components: ${{ inputs.toolchain-components }}
2222

2323
- name: Cache dependencies
24-
uses: Swatinem/rust-cache@42dc69e1aa15d09112580998cf2ef0119e2e91ae # v2
24+
uses: Swatinem/rust-cache@6323deb102c322ba6fcbdcafc7e3dddab59af2b6 # v2.9.2
2525
with:
2626
shared-key: ${{ inputs.shared-key }}
2727

‎.github/dependabot.yml‎

Lines changed: 6 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -17,13 +17,14 @@ updates:
1717
prefix: "deps"
1818
ignore:
1919
# Architectural pins -- see AGENTS.md "Crate Versioning (CRITICAL)"
20-
# ariadne 0.5+ changes the Report/Label API.
20+
# ariadne 0.6 is current (Report::build takes (kind, span)); 0.7+
21+
# would be a new API break. Allow 0.6.x patches through.
2122
- dependency-name: ariadne
22-
versions: [">=0.5"]
23-
# z3 0.13+ has significant API changes and must match the system
24-
# libz3 version installed in CI.
23+
versions: [">=0.7"]
24+
# z3 0.20 is current (no lifetime params, no &ctx first arg);
25+
# 0.21+ is a new major. Allow 0.20.x patches through.
2526
- dependency-name: z3
26-
versions: [">=0.13"]
27+
versions: [">=0.21"]
2728
groups:
2829
# tonic, prost, and tonic-build must be upgraded together;
2930
# individual PRs always fail because of version coupling.

‎.github/workflows/auto-approve.yml‎

Lines changed: 5 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -33,11 +33,13 @@ jobs:
3333
permissions:
3434
contents: write
3535
pull-requests: write
36-
# Skip self-approve deadlock. Run for maintainer actor, Dependabot, bots,
37-
# or any PR when dispatched manually with pr_number.
36+
# Skip self-approve deadlock. Run for maintainer actor, Dependabot,
37+
# the same-org auto-approve App, or any PR when dispatched manually
38+
# with pr_number.
3839
# Same-repo PRs (Dependabot) use pull_request only. Forks use
3940
# pull_request_target only (secrets). Running both on the same PR
4041
# cancelled one job and painted a false red check.
42+
# Do not allowlist endsWith('[bot]'): a fork PR from any login ending in [bot] would be approved and auto-merged.
4143
if: >-
4244
github.event_name == 'workflow_dispatch' ||
4345
(github.event.pull_request.user.login != 'github-actions[bot]' &&
@@ -47,7 +49,7 @@ jobs:
4749
github.event.pull_request.head.repo.full_name != github.repository)) &&
4850
(github.actor == 'SebTardif' ||
4951
github.event.pull_request.user.login == 'dependabot[bot]' ||
50-
endsWith(github.event.pull_request.user.login, '[bot]')))
52+
github.event.pull_request.user.login == 'assura-auto-approve[bot]'))
5153
steps:
5254
- name: Harden runner
5355
uses: step-security/harden-runner@05e31511f85b41b11d1cf0ef85d0992719546e2c # v2.21.0

‎.github/workflows/ci.yml‎

Lines changed: 5 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -390,15 +390,18 @@ jobs:
390390

391391

392392
- name: Install CVC5 prebuilt library
393+
env:
394+
# Same tag as scripts/setup-cvc5.sh (cvc5 crate 0.4 wraps 1.3.1).
395+
CVC5_RELEASE_TAG: cvc5-1.3.1
393396
run: |
394397
if [ "$(uname)" = "Darwin" ]; then
395398
ARCH=$(uname -m)
396-
curl -sL "https://github.com/cvc5/cvc5/releases/latest/download/cvc5-macOS-${ARCH}-static.zip" -o /tmp/cvc5.zip
399+
curl -sL "https://github.com/cvc5/cvc5/releases/download/${CVC5_RELEASE_TAG}/cvc5-macOS-${ARCH}-static.zip" -o /tmp/cvc5.zip
397400
unzip -o /tmp/cvc5.zip -d /tmp/cvc5-install
398401
echo "CVC5_LIB_DIR=/tmp/cvc5-install/cvc5-macOS-${ARCH}-static/lib" >> "$GITHUB_ENV"
399402
echo "CVC5_INCLUDE_DIR=/tmp/cvc5-install/cvc5-macOS-${ARCH}-static/include" >> "$GITHUB_ENV"
400403
else
401-
curl -sL "https://github.com/cvc5/cvc5/releases/latest/download/cvc5-Linux-x86_64-static.zip" -o /tmp/cvc5.zip
404+
curl -sL "https://github.com/cvc5/cvc5/releases/download/${CVC5_RELEASE_TAG}/cvc5-Linux-x86_64-static.zip" -o /tmp/cvc5.zip
402405
unzip -o /tmp/cvc5.zip -d /tmp/cvc5-install
403406
echo "CVC5_LIB_DIR=/tmp/cvc5-install/cvc5-Linux-x86_64-static/lib" >> "$GITHUB_ENV"
404407
echo "CVC5_INCLUDE_DIR=/tmp/cvc5-install/cvc5-Linux-x86_64-static/include" >> "$GITHUB_ENV"

‎.github/workflows/docs.yml‎

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -31,7 +31,8 @@ jobs:
3131
- name: Install mdBook
3232
uses: peaceiris/actions-mdbook@ee69d230fe19748b7abf22df32acaa93833fad08 # v2
3333
with:
34-
mdbook-version: 'latest'
34+
# Pin a released mdBook. 'latest' floats and can break Pages builds.
35+
mdbook-version: '0.5.4'
3536

3637
- name: Build docs
3738
run: mdbook build docs/

‎.github/workflows/fuzz.yml‎

Lines changed: 32 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -34,36 +34,63 @@ jobs:
3434
persist-credentials: false
3535

3636
# cargo-fuzz needs nightly (-Zsanitizer=address, coverage passes).
37+
# Dated pin: floating `nightly` breaks when a rustc snapshot rejects sanitizers.
3738
- name: Install nightly + rust-src
3839
uses: dtolnay/rust-toolchain@4be7066ada62dd38de10e7b70166bc74ed198c30 # stable action; pin toolchain below
3940
with:
40-
toolchain: nightly
41+
toolchain: nightly-2026-08-15
4142
components: rust-src
4243

44+
- name: Cache cargo and fuzz workspaces
45+
uses: Swatinem/rust-cache@6323deb102c322ba6fcbdcafc7e3dddab59af2b6 # v2.9.2
46+
with:
47+
workspaces: |
48+
.
49+
fuzz
50+
shared-key: fuzz
51+
cache-on-failure: true
52+
4353
- name: Install cargo-fuzz
44-
run: cargo +nightly install cargo-fuzz --locked
54+
uses: taiki-e/install-action@0c80bcf54d007ab0e714c95f3bcc43c387707535 # v2
55+
with:
56+
tool: cargo-fuzz
57+
env:
58+
HOME: ${{ runner.temp }}/install-action-home
59+
60+
- name: Build fuzz targets
61+
env:
62+
RUSTUP_TOOLCHAIN: nightly-2026-08-15
63+
run: |
64+
cargo +nightly-2026-08-15 fuzz build || (
65+
echo "::warning::retrying fuzz build"
66+
sleep 5
67+
cargo +nightly-2026-08-15 fuzz build
68+
)
4569
4670
- name: Fuzz lexer
4771
env:
4872
FUZZ_DURATION: ${{ inputs.duration || '60' }}
73+
RUSTUP_TOOLCHAIN: nightly-2026-08-15
4974
run: |
50-
cargo +nightly fuzz run fuzz_lex -- \
75+
cargo +nightly-2026-08-15 fuzz run fuzz_lex -- \
5176
-max_total_time="${FUZZ_DURATION}" \
5277
-max_len=4096
5378
5479
- name: Fuzz parser
5580
env:
5681
FUZZ_DURATION: ${{ inputs.duration || '60' }}
82+
RUSTUP_TOOLCHAIN: nightly-2026-08-15
5783
run: |
58-
cargo +nightly fuzz run fuzz_parse -- \
84+
cargo +nightly-2026-08-15 fuzz run fuzz_parse -- \
5985
-max_total_time="${FUZZ_DURATION}" \
6086
-max_len=4096
6187
6288
- name: Fuzz type checker
6389
env:
6490
FUZZ_DURATION: ${{ inputs.duration || '60' }}
91+
RUSTUP_TOOLCHAIN: nightly-2026-08-15
6592
run: |
66-
cargo +nightly fuzz run fuzz_typecheck -- \
93+
cargo +nightly-2026-08-15 fuzz run fuzz_typecheck -- \
6794
-max_total_time="${FUZZ_DURATION}" \
6895
-max_len=4096
6996

‎.github/workflows/nightly.yml‎

Lines changed: 7 additions & 58 deletions
Original file line numberDiff line numberDiff line change
@@ -12,9 +12,12 @@ concurrency:
1212
permissions:
1313
contents: read
1414

15+
# Daily CI (ci.yml schedule 0 3 * * *) already runs fmt, clippy, workspace
16+
# test, cargo-package, CVC5, demo check/codegen, and no-z3. Nightly keeps
17+
# only coverage CI still skips: examples/**/*.assura.
1518
jobs:
16-
full-test:
17-
name: Full test suite
19+
examples:
20+
name: E2E check all examples
1821
runs-on: ubuntu-latest
1922
timeout-minutes: 45
2023
env:
@@ -31,17 +34,15 @@ jobs:
3134

3235
- name: Setup Rust toolchain
3336
uses: dtolnay/rust-toolchain@4be7066ada62dd38de10e7b70166bc74ed198c30 # stable
34-
with:
35-
components: clippy, rustfmt
3637

3738
- name: Cache dependencies
38-
uses: Swatinem/rust-cache@6323deb102c322ba6fcbdcafc7e3dddab59af2b6 # v2
39+
uses: Swatinem/rust-cache@6323deb102c322ba6fcbdcafc7e3dddab59af2b6 # v2.9.2
3940
with:
4041
shared-key: ci-nightly
4142

4243
- name: Install system dependencies (Linux)
4344
if: runner.os == 'Linux'
44-
run: sudo apt-get install -y protobuf-compiler libz3-dev z3 ripgrep
45+
run: sudo apt-get install -y protobuf-compiler libz3-dev z3
4546
env:
4647
DEBIAN_FRONTEND: noninteractive
4748

@@ -54,27 +55,9 @@ jobs:
5455
echo "LIBRARY_PATH=/usr/lib/x86_64-linux-gnu"
5556
} >> "$GITHUB_ENV"
5657
57-
- name: Format check
58-
run: cargo fmt --check --all
59-
60-
- name: Clippy
61-
run: cargo clippy --workspace --locked -- -D warnings
62-
63-
- name: Full test suite
64-
run: cargo test --workspace --locked
65-
6658
- name: Build compiler
6759
run: cargo build --locked --bin assura
6860

69-
- name: E2E check all demos
70-
run: |
71-
for demo in demos/*.assura; do
72-
# Audit demos have intentional counterexamples (real CVE models); skip them
73-
case "$demo" in *-audit*|*audit-*) echo "=== Skipping audit demo $demo ==="; continue;; esac
74-
echo "=== Checking $demo ==="
75-
cargo run --bin assura -- check "$demo"
76-
done
77-
7861
- name: E2E check all examples
7962
run: |
8063
failed=0
@@ -86,37 +69,3 @@ jobs:
8669
fi
8770
done
8871
exit $failed
89-
90-
- name: Codegen validation (demos)
91-
run: |
92-
for demo in demos/*.assura; do
93-
case "$demo" in *-audit*|*audit-*) continue;; esac
94-
echo "=== Building $demo ==="
95-
cargo run --bin assura -- build --no-check "$demo"
96-
# build writes to <input-parent>/generated/ (e.g. demos/generated/)
97-
gen_dir="$(dirname "$demo")/generated"
98-
echo "=== Checking generated Rust for $demo ==="
99-
(cd "$gen_dir" && cargo check)
100-
rm -rf "$gen_dir"
101-
done
102-
103-
no-z3-fallback:
104-
name: No-Z3 fallback
105-
runs-on: ubuntu-latest
106-
timeout-minutes: 10
107-
steps:
108-
- name: Harden runner
109-
uses: step-security/harden-runner@05e31511f85b41b11d1cf0ef85d0992719546e2c # v2.21.0
110-
with:
111-
egress-policy: audit
112-
- uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7
113-
with:
114-
persist-credentials: false
115-
- name: Setup Rust toolchain
116-
uses: dtolnay/rust-toolchain@4be7066ada62dd38de10e7b70166bc74ed198c30 # stable
117-
- name: Cache dependencies
118-
uses: Swatinem/rust-cache@6323deb102c322ba6fcbdcafc7e3dddab59af2b6 # v2
119-
with:
120-
shared-key: ci-nightly-no-z3
121-
- name: Build without Z3
122-
run: cargo check -p assura-smt --no-default-features --locked

‎.github/workflows/rebase-dependabot.yml‎

Lines changed: 12 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -100,11 +100,21 @@ jobs:
100100
git rebase --abort
101101
continue
102102
fi
103-
git push --force-with-lease="refs/heads/${branch}:${expected}" \
104-
"${remote_url}" "HEAD:refs/heads/${branch}"
103+
if ! git push --force-with-lease="refs/heads/${branch}:${expected}" \
104+
"${remote_url}" "HEAD:refs/heads/${branch}"; then
105+
echo "Lease rejected again on #${n}; leaving it for a later run."
106+
continue
107+
fi
105108
fi
106109
done
107110
111+
- name: Require App token to unstick CI
112+
if: steps.app-token.outputs.token == ''
113+
run: |
114+
echo "FAIL: App token is empty after rebase; cannot unstick Dependabot CI."
115+
echo "Set AUTO_APPROVE_CLIENT_ID and AUTO_APPROVE_PRIVATE_KEY."
116+
exit 1
117+
108118
- name: Start CI and re-approve after GITHUB_TOKEN rebase
109119
if: steps.app-token.outputs.token != ''
110120
env:

‎AGENTS.md‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1170,14 +1170,14 @@ brew install cmake gmp
11701170
11711171
# For CI or manual prebuilt setup:
11721172
# macOS ARM64
1173-
curl -sL "https://github.com/cvc5/cvc5/releases/latest/download/cvc5-macOS-arm64-static.zip" \
1173+
curl -sL "https://github.com/cvc5/cvc5/releases/download/cvc5-1.3.1/cvc5-macOS-arm64-static.zip" \
11741174
-o /tmp/cvc5.zip
11751175
unzip -o /tmp/cvc5.zip -d /tmp/cvc5-install
11761176
export CVC5_LIB_DIR=/tmp/cvc5-install/cvc5-macOS-arm64-static/lib
11771177
export CVC5_INCLUDE_DIR=/tmp/cvc5-install/cvc5-macOS-arm64-static/include
11781178
11791179
# Linux x86_64
1180-
curl -sL "https://github.com/cvc5/cvc5/releases/latest/download/cvc5-Linux-x86_64-static.zip" \
1180+
curl -sL "https://github.com/cvc5/cvc5/releases/download/cvc5-1.3.1/cvc5-Linux-x86_64-static.zip" \
11811181
-o /tmp/cvc5.zip
11821182
unzip -o /tmp/cvc5.zip -d /tmp/cvc5-install
11831183
export CVC5_LIB_DIR=/tmp/cvc5-install/cvc5-Linux-x86_64-static/lib

0 commit comments

Comments
 (0)