From 5fb78ed1a6c12896457c198a5acc426886b53fca Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com> Date: Wed, 4 Nov 2026 21:05:47 +0000 Subject: [PATCH 01/15] Fix/148 creusot execution evidence (#2) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit ## Summary Closes # ## Type of change - [ ] ๐Ÿ› Bug fix (non-breaking change that fixes an issue) - [ ] โœจ New feature (non-breaking change that adds functionality) - [ ] ๐Ÿ’ฅ Breaking change (would change existing behaviour) - [ ] ๐Ÿ•ณ๏ธ Soundness fix (fixes a checker/proof false-negative) - [ ] ๐Ÿ“– Documentation - [ ] ๐Ÿงน Refactor / tech debt (behaviour-preserving) - [ ] โšก Performance - [ ] ๐Ÿ”ง Build / CI / tooling ## How has this been verified? ## Checklist - [ ] My commits are **signed** (`git commit -S`). - [ ] I ran the project's own checks/tests locally and they pass. - [ ] New files carry the correct `SPDX-License-Identifier` (code/config `MPL-2.0`, prose `CC-BY-SA-4.0`); I did not relicense existing files. - [ ] Docs are updated, and no public claim now overstates what the code does. - [ ] I have not introduced a soundness hole (or I have flagged where I might have). ## Notes for reviewers --------- Signed-off-by: Jonathan D.A. Jewell <6759885+hyperpolymath@users.noreply.github.com> --- .github/workflows/creusot-gate.yml | 67 ++- .../workflows/language-gates-self-test.yml | 7 +- .mise.toml | 4 +- actions/creusot-check/action.yml | 2 +- actions/creusot-check/check.sh | 268 ++++++++-- actions/creusot-check/source-facts/Cargo.lock | 46 ++ actions/creusot-check/source-facts/Cargo.toml | 12 + .../creusot-check/source-facts/src/main.rs | 463 ++++++++++++++++++ actions/creusot-check/test.sh | 226 ++++++++- actions/creusot-check/verdict-test.sh | 80 +++ actions/creusot-check/verdict.sh | 100 ++++ docs/assurance/CREUSOT-EXECUTION.adoc | 124 +++++ docs/assurance/LOCK-SCOPE.adoc | 9 +- 13 files changed, 1310 insertions(+), 98 deletions(-) create mode 100644 actions/creusot-check/source-facts/Cargo.lock create mode 100644 actions/creusot-check/source-facts/Cargo.toml create mode 100644 actions/creusot-check/source-facts/src/main.rs create mode 100644 actions/creusot-check/verdict-test.sh create mode 100644 actions/creusot-check/verdict.sh create mode 100644 docs/assurance/CREUSOT-EXECUTION.adoc diff --git a/.github/workflows/creusot-gate.yml b/.github/workflows/creusot-gate.yml index f4a1536..5b5b012 100644 --- a/.github/workflows/creusot-gate.yml +++ b/.github/workflows/creusot-gate.yml @@ -54,7 +54,7 @@ on: required: false default: false prove_args: - description: Extra arguments for `cargo creusot` + description: 'Scope-preserving options only: --no-cache, --why3session, -j N (positive decimal)' type: string required: false default: "" @@ -77,6 +77,7 @@ jobs: permissions: contents: read outputs: + suite_sha: ${{ steps.suite.outputs.sha }} obligations: ${{ steps.facts.outputs.obligations }} claims: ${{ steps.facts.outputs.claims }} creusot_version: ${{ steps.facts.outputs.creusot_version }} @@ -235,6 +236,19 @@ jobs: contents: read env: CREUSOT_VERSION: ${{ inputs.creusot_version }} + outputs: + proof_step_outcome: ${{ steps.proof.outcome }} + execution_stage: ${{ steps.proof.outputs.execution_stage }} + execution_outcome: ${{ steps.proof.outputs.execution_outcome }} + controls_passed: ${{ steps.proof.outputs.controls_passed }} + proof_started: ${{ steps.proof.outputs.proof_started }} + proof_completed: ${{ steps.proof.outputs.proof_completed }} + crates_expected: ${{ steps.proof.outputs.crates_expected }} + crates_attempted: ${{ steps.proof.outputs.crates_attempted }} + crates_completed: ${{ steps.proof.outputs.crates_completed }} + source_revision: ${{ steps.proof.outputs.source_revision }} + suite_revision: ${{ steps.proof.outputs.suite_revision }} + proof_exit_code: ${{ steps.proof.outputs.proof_exit_code }} steps: - name: Check out the calling repository uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1 @@ -337,8 +351,10 @@ jobs: cargo creusot --help >/dev/null cargo creusot version - name: Planted controls, then every crate with obligations + id: proof env: CREUSOT_GATE_PHASE: prove + CREUSOT_SUITE_REVISION: ${{ steps.suite.outputs.sha }} WORKING_DIRECTORY: ${{ inputs.working_directory }} PROVE_ARGS: ${{ inputs.prove_args }} run: bash .cicd-suite/actions/creusot-check/check.sh @@ -358,23 +374,38 @@ jobs: R_DETECT: ${{ needs.detect.result }} R_THEATRE: ${{ needs.theatre.result }} R_PROVE: ${{ needs.prove.result }} + PROOF_STEP_OUTCOME: ${{ needs.prove.outputs.proof_step_outcome }} + EXECUTION_STAGE: ${{ needs.prove.outputs.execution_stage }} + EXECUTION_OUTCOME: ${{ needs.prove.outputs.execution_outcome }} + CONTROLS_PASSED: ${{ needs.prove.outputs.controls_passed }} + PROOF_STARTED: ${{ needs.prove.outputs.proof_started }} + PROOF_COMPLETED: ${{ needs.prove.outputs.proof_completed }} + CRATES_EXPECTED: ${{ needs.prove.outputs.crates_expected }} + CRATES_ATTEMPTED: ${{ needs.prove.outputs.crates_attempted }} + CRATES_COMPLETED: ${{ needs.prove.outputs.crates_completed }} + SOURCE_REVISION: ${{ needs.prove.outputs.source_revision }} + SUITE_REVISION: ${{ needs.prove.outputs.suite_revision }} + PROOF_EXIT_CODE: ${{ needs.prove.outputs.proof_exit_code }} + EXPECTED_SOURCE_REVISION: ${{ github.sha }} + EXPECTED_SUITE_REVISION: ${{ needs.detect.outputs.suite_sha }} steps: - - name: Adjudicate + - name: Require a resolved gate before reading its execution evidence run: | set -euo pipefail - fail=0 - [ "$R_DETECT" = success ] || { echo "::error::detect: $R_DETECT"; fail=1; } - [ "$R_THEATRE" = success ] || { echo "::error::theatre: $R_THEATRE"; fail=1; } - case "$R_PROVE" in - success) echo " ok prove (trusted axioms: ${TRUSTED:-?})" ;; - failure|cancelled) echo "::error::prove: $R_PROVE"; fail=1 ;; - skipped) - if [ "$OBLIGATIONS" = true ]; then - echo "::error::prove was SKIPPED although obligations exist โ€” VOID, not green."; fail=1 - else - echo "::notice::No Creusot obligations in this tree: nothing was proved. This verdict is silent, not green-as-assurance (claims=${CLAIMS:-false})." - fi ;; - *) echo "::error::prove: unknown result '$R_PROVE'"; fail=1 ;; - esac - [ "$fail" -eq 0 ] || { echo "::error::Creusot verdict: RED."; exit 1; } - echo "Creusot verdict: GREEN." + if [[ ! "$EXPECTED_SUITE_REVISION" =~ ^[0-9a-f]{40}$ ]]; then + echo "::error::Creusot execution: PreflightFailed โ€” the gate source was not resolved; no proof verdict is available." + exit 2 + fi + - name: Check out the resolved verdict implementation + uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1 + with: + repository: hyperpolymath/cicd-suite + ref: ${{ needs.detect.outputs.suite_sha }} + path: .cicd-suite + persist-credentials: false + - name: Refuse an unverified verdict implementation + env: + EXPECTED: ${{ needs.detect.outputs.suite_sha }} + run: bash .cicd-suite/scripts/verify-suite-checkout.sh + - name: Adjudicate + run: bash .cicd-suite/actions/creusot-check/verdict.sh diff --git a/.github/workflows/language-gates-self-test.yml b/.github/workflows/language-gates-self-test.yml index 67725f0..cd1f25d 100644 --- a/.github/workflows/language-gates-self-test.yml +++ b/.github/workflows/language-gates-self-test.yml @@ -4,14 +4,15 @@ # language-gates-self-test.yml โ€” the four language gates must be able to # FAIL, for each thing they claim to check, before any consumer calls them. # -# This repository has no Rust, Ada or Scheme of its own, so a self-run of -# the reusables would be silent and prove nothing. Instead each gate's +# Gate fixtures establish that each reusable can reject its named defects; +# a self-run cannot establish that its consumers were verified. Each gate's # test.sh builds a fixture, plants a defect, asserts the gate goes red for # that defect under the exact composite shell, and kills a mutant where one # exists (tests/composite-shell-contract.sh explains the -e trap that made # that necessary). The prover tiers run against stand-in oracles here; the # planted controls inside the check scripts exercise the real provers on -# every live run. +# every live run. The Creusot source reader also runs its real Rust unit, +# formatting and Clippy checks before the stand-in prover controls. name: Language Gates Self-Test diff --git a/.mise.toml b/.mise.toml index 9159c55..717a934 100644 --- a/.mise.toml +++ b/.mise.toml @@ -1,5 +1,5 @@ [tools] -# = "The actions in this repository are bash + composite YAML and need no build" -# = "toolchain of their own. `just` is pinned because recipes-set-check installs" +# = "The actions are Bash + composite YAML; the Creusot source reader additionally" +# = "requires Rust >= 1.85 and its checked-in Cargo.lock. `just` is pinned because recipes-set-check installs" # = "and invokes it, so this is the version that gate is tested against." just = "1.36.0" diff --git a/actions/creusot-check/action.yml b/actions/creusot-check/action.yml index 39beef0..02b282a 100644 --- a/actions/creusot-check/action.yml +++ b/actions/creusot-check/action.yml @@ -20,7 +20,7 @@ inputs: required: false default: 'false' prove_args: - description: 'Args appended to cargo creusot' + description: 'Scope-preserving options only: --no-cache, --why3session, -j N (positive decimal)' required: false default: '' runs: diff --git a/actions/creusot-check/check.sh b/actions/creusot-check/check.sh index 5a729d7..c7fb159 100755 --- a/actions/creusot-check/check.sh +++ b/actions/creusot-check/check.sh @@ -21,39 +21,75 @@ # CREUSOT_GATE_PHASE=theatre (the anti-theatre tier, mirrors # standards' SPARK Theatre Gate T1/T2) # T1 a claim with no obligations behind it: hard failure, always. -# T2 a Creusot dependency with ZERO contract attributes anywhere: a -# hollow dependency proves nothing. Warning by default; a hard -# failure when ENFORCE_HOLLOW=true. -# T3 every `#[trusted]` is printed. `trusted` is an axiom the prover -# takes on faith; the gate never fails on it, but it never lets one -# pass unlisted either (the residue list of the proof). +# T2 a Creusot dependency without a supported function-bound contract: +# warning by default; a hard failure when ENFORCE_HOLLOW=true. +# T3 every supported source `#[trusted]` declaration is printed. +# `trusted` is an axiom the prover takes on faith. Source inspection +# is bounded; macro expansion and module reachability remain compiler +# responsibilities, not a claimed complete proof-residue ledger. # # CREUSOT_GATE_PHASE=prove # Requires `cargo creusot` on PATH (the workflow installs it, pinned). # FIRST proves a planted known-failing contract and REQUIRES a non-zero -# exit; then a planted known-good one and requires zero. A prover that +# exit; then a planted known-good one and requires zero plus a nonzero +# proved-file denominator. A prover that # cannot say no is not a prover, and the verdict over the caller's # crate would be VOID โ€” so the gate refuses (exit 2) rather than report # green. Only then does it run `cargo creusot` in every crate -# directory that carries obligations, failing on any non-zero exit. +# directory that carries obligations, failing on any non-zero exit or +# missing/zero proved-file report. # # Exit codes: 0 silent, 1 defect found, 2 NO CHECK WAS PERFORMED (tool # missing, planted control misbehaved, unreadable tree). 2 is never a pass. # # Env: WORKING_DIRECTORY (default "."), ENFORCE_HOLLOW (default false), -# PROVE_ARGS (appended to `cargo creusot`), CREUSOT_FACTS (path +# PROVE_ARGS (--no-cache, --why3session, -j N only), CREUSOT_FACTS (path # the detect phase writes its crate list to; default $RUNNER_TEMP or # /tmp). set -uo pipefail phase="${CREUSOT_GATE_PHASE:?CREUSOT_GATE_PHASE is required: detect|theatre|prove}" +reader_manifest="$(cd "$(dirname "${BASH_SOURCE[0]}")" && pwd)/source-facts/Cargo.toml" dir="${WORKING_DIRECTORY:-.}" enforce_hollow="${ENFORCE_HOLLOW:-false}" prove_args="${PROVE_ARGS:-}" facts_dir="${CREUSOT_FACTS:-${RUNNER_TEMP:-/tmp}/creusot-facts}" mkdir -p "$facts_dir" +facts_dir="$(cd "$facts_dir" && pwd)" + +# These are observations of this invocation, not an authenticated proof +# certificate. The workflow also checks the actual step/job conclusions. +# A setup failure must never be promoted to a failure of the caller's contracts. +execution_stage=setup +execution_outcome=unavailable +controls_passed=false +proof_started=false +proof_completed=false +crates_expected=0 +crates_attempted=0 +crates_completed=0 +source_revision="" +record_execution() { + local rc=$? + if [[ "$phase" = prove ]] && [[ -n "${GITHUB_OUTPUT:-}" ]]; then + # Fixed keys and validated scalar values only. In particular, no compiler + # output is allowed to write additional GitHub Actions output records. + [[ "$source_revision" =~ ^[0-9a-f]{40}$ ]] || source_revision="" + local suite_revision="${CREUSOT_SUITE_REVISION:-}" + [[ "$suite_revision" =~ ^[0-9a-f]{40}$ ]] || suite_revision="" + { + printf 'execution_stage=%s\nexecution_outcome=%s\n' "$execution_stage" "$execution_outcome" + printf 'controls_passed=%s\nproof_started=%s\nproof_completed=%s\n' "$controls_passed" "$proof_started" "$proof_completed" + printf 'crates_expected=%s\ncrates_attempted=%s\ncrates_completed=%s\n' "$crates_expected" "$crates_attempted" "$crates_completed" + printf 'source_revision=%s\nsuite_revision=%s\nproof_exit_code=%s\n' "$source_revision" "$suite_revision" "$rc" + } >> "$GITHUB_OUTPUT" || return 2 + fi + return "$rc" +} +trap 'record_execution' EXIT cd "$dir" || { echo "::error::creusot-check[$phase]: cannot enter $dir โ€” NO CHECK WAS PERFORMED." >&2; exit 2; } +source_revision="$(git rev-parse HEAD 2>/dev/null || true)" # Tracked files only: an untracked checkout of this suite (.cicd-suite/) or a # target/ tree must never count as the caller's sources. @@ -71,30 +107,46 @@ manifests="$(list_files '(^|/)Cargo\.toml$')" obligation_manifests="" creusot_version="" while IFS= read -r m; do - [ -n "$m" ] || continue + [[ -n "$m" ]] || continue # A dependency line for the proof library, under any dependency table. if grep -qE '^[[:space:]]*(creusot-std|creusot-contracts)[[:space:]]*=' "$m" \ || grep -qE '^[[:space:]]*\[(workspace\.)?dependencies\.(creusot-std|creusot-contracts)\]' "$m"; then obligation_manifests="${obligation_manifests}${m}"$'\n' - if [ -z "$creusot_version" ]; then + if [[ -z "$creusot_version" ]]; then creusot_version="$(sed -nE 's/^[[:space:]]*(creusot-std|creusot-contracts)[[:space:]]*=[[:space:]]*(\{[^}]*version[[:space:]]*=[[:space:]]*)?"([^"]+)".*$/\3/p' "$m" | head -n 1 || true)" fi fi done <<< "$manifests" -contract_re='#\[(requires|ensures|invariant|variant|logic|law|open|predicate|terminates|pure|trusted)(\(|\])|proof_assert!|#\[creusot::' rust_sources="$(list_files '\.rs$')" contract_files="" contract_count=0 trusted_count=0 -if [ -n "$rust_sources" ]; then - contract_files="$(printf '%s\n' "$rust_sources" | xargs -r grep -lE "$contract_re" 2>/dev/null || true)" - contract_count="$({ printf '%s\n' "$rust_sources" | xargs -r grep -cE '#\[(requires|ensures)\(' 2>/dev/null || true; } | awk -F: '{s+=$NF} END {print s+0}')" - trusted_count="$({ printf '%s\n' "$rust_sources" | xargs -r grep -cE '#\[trusted\]' 2>/dev/null || true; } | awk -F: '{s+=$NF} END {print s+0}')" +if [[ -n "$rust_sources" ]]; then + # Parse Rust attributes on function nodes instead of counting prose, string + # literals or tokens quoted inside macros. Build from the pinned gate source + # and Cargo.lock, outside the caller cwd so its Cargo config is not selected. + command -v cargo >/dev/null 2>&1 || { + echo "::error::creusot-check[$phase]: Cargo is required for the pinned Rust source reader. NO CHECK WAS PERFORMED." >&2 + exit 2 + } + if ! (cd "${RUNNER_TEMP:-/tmp}" && cargo build --quiet --locked \ + --manifest-path "$reader_manifest" --target-dir "$facts_dir/source-target"); then + echo "::error::creusot-check[$phase]: the pinned Rust source reader could not be built. NO CHECK WAS PERFORMED." >&2 + exit 2 + fi + mapfile -t source_files <<< "$rust_sources" + if ! "$facts_dir/source-target/debug/creusot-source-facts" "${source_files[@]}" > "$facts_dir/source-facts.tsv"; then + echo "::error::creusot-check[$phase]: Rust source facts are unavailable. NO CHECK WAS PERFORMED." >&2 + exit 2 + fi + contract_files="$(cut -f2 "$facts_dir/source-facts.tsv" | sort -u)" + contract_count="$(awk -F '\t' '$1 == "contract" { count++ } END { print count+0 }' "$facts_dir/source-facts.tsv")" + trusted_count="$(awk -F '\t' '$1 == "trusted" { count++ } END { print count+0 }' "$facts_dir/source-facts.tsv")" fi obligations=false -if [ -n "$obligation_manifests" ] || [ -n "$contract_files" ]; then obligations=true; fi +if [[ -n "$obligation_manifests" ]] || [[ -n "$contract_files" ]]; then obligations=true; fi # A claim is a sentence in prose or a source HEADER that asserts the proof # exists. Scoped to README*/docs/** and to the leading comment block of a @@ -107,15 +159,15 @@ plan_re='(planned|proposal|proposed|roadmap|not yet|would|future|todo|intend)' claim_sites="" prose="$(list_files '(^|/)(README[^/]*|[^/]*\.(adoc|md))$' | grep -vE '^(\.cicd-suite|target)/' || true)" while IFS= read -r f; do - [ -n "$f" ] || continue + [[ -n "$f" ]] || continue while IFS= read -r hit; do - [ -n "$hit" ] || continue + [[ -n "$hit" ]] || continue printf '%s' "$hit" | grep -qiE "$plan_re" && continue claim_sites="${claim_sites}${f}:${hit%%:*}"$'\n' done < <(grep -niE "$claim_re" "$f" 2>/dev/null || true) done <<< "$prose" while IFS= read -r f; do - [ -n "$f" ] || continue + [[ -n "$f" ]] || continue header="$(awk '/^[[:space:]]*(\/\/|\/\*|\*)/ || /^[[:space:]]*$/ { print; next } { exit }' "$f")" if printf '%s\n' "$header" | grep -qiE "$claim_re" \ && ! printf '%s\n' "$header" | grep -qiE "$plan_re"; then @@ -123,7 +175,7 @@ while IFS= read -r f; do fi done <<< "$rust_sources" claims=false -[ -n "$claim_sites" ] && claims=true +[[ -n "$claim_sites" ]] && claims=true crate_dirs="$(printf '%s' "$obligation_manifests" | sed -E 's#(^|/)Cargo\.toml$##; s#^$#.#' | sort -u)" printf '%s\n' "$crate_dirs" | sed '/^$/d' > "$facts_dir/crates" @@ -142,44 +194,140 @@ case "$phase" in theatre) fail=0 - if [ "$claims" = true ] && [ "$obligations" = false ]; then + if [[ "$claims" = true ]] && [[ "$obligations" = false ]]; then while IFS= read -r site; do - [ -n "$site" ] || continue + [[ -n "$site" ]] || continue echo "::error file=${site%%:*},line=${site##*:}::T1 Creusot theatre: this says the code is verified with Creusot, but no crate depends on creusot-std and no #[requires]/#[ensures] exists. Add the contracts and the dependency, or remove the claim (standards#692: Rust + Creusot, without proof theatre)." done <<< "$claim_sites" fail=1 fi - if [ "$obligations" = true ] && [ "$contract_count" -eq 0 ]; then - msg="T2 hollow Creusot dependency: creusot-std/creusot-contracts is a dependency but no #[requires]/#[ensures] appears in any tracked .rs file, so 'cargo creusot' would discharge nothing. Write a contract on at least one function, or drop the dependency." - if [ "$enforce_hollow" = true ]; then + if [[ "$obligations" = true ]] && [[ "$contract_count" -eq 0 ]]; then + msg="T2 hollow Creusot dependency: no supported requires/ensures attribute is bound to a function in the tracked Rust source. Add a real contract or inspect unsupported macro/configuration forms; no proof coverage is established by a dependency alone." + if [[ "$enforce_hollow" = true ]]; then echo "::error::$msg"; fail=1 else echo "::warning::$msg (escalates to a failure with enforce_hollow: true)" fi fi - if [ "$trusted_count" -gt 0 ]; then - echo "::notice::T3 residue: $trusted_count #[trusted] item(s) are taken as axioms by the prover. They are listed below; a proof is only as strong as its trusted set." - printf '%s\n' "$rust_sources" | xargs -r grep -nE '#\[trusted\]' 2>/dev/null | sed 's/^/ trusted: /' || true + if [[ "$trusted_count" -gt 0 ]]; then + echo "::notice::T3 residue: $trusted_count #[trusted] function declaration(s) found in the inspected source. These are assumptions, not discharged obligations; macro expansion and module reachability still belong to the compiler." + awk -F '\t' '$1 == "trusted" { printf " trusted: %s:%s\n", $2, $3 }' "$facts_dir/source-facts.tsv" fi - if [ "$obligations" = false ] && [ "$claims" = false ]; then + if [[ "$obligations" = false ]] && [[ "$claims" = false ]]; then echo "::notice::creusot-check: no Creusot obligations and no verification claims in this tree. Nothing was proved and nothing claims to be โ€” this gate is silent, not green-as-assurance." fi - [ "$fail" -eq 0 ] || { echo "::error::creusot-check[theatre]: FAILED โ€” see annotations."; exit 1; } + [[ "$fail" -eq 0 ]] || { echo "::error::creusot-check[theatre]: FAILED โ€” see annotations."; exit 1; } echo "creusot-check[theatre]: no theatre found (obligations=$obligations claims=$claims contracts=$contract_count trusted=$trusted_count)." exit 0 ;; prove) - if [ "$obligations" = false ]; then + if [[ "$obligations" = false ]]; then echo "::error::creusot-check[prove]: no Creusot obligations in this tree โ€” NO PROOF WAS PERFORMED. The prove job must only run when detect reported obligations=true." >&2 exit 2 fi - command -v cargo >/dev/null 2>&1 && cargo creusot --help >/dev/null 2>&1 || { + # Unrestricted CLI arguments can narrow the proof to a positional pattern, + # select other packages, skip translation/proving, or replace the compiler. + # Controls do not establish coverage of omitted caller obligations. Accept + # only operational v0.14 options that preserve package and proof scope. + reject_prove_args() { + echo "::error::creusot-check[prove]: unsupported PROVE_ARGS. Only --no-cache, --why3session and -j N (positive decimal) preserve this gate's proof scope. NO PROOF WAS PERFORMED." >&2 + exit 2 + } + [[ "$prove_args" != *$'\n'* && "$prove_args" != *$'\r'* ]] || reject_prove_args + requested_options=() + read -r -a requested_options <<< "$prove_args" + prove_options=() + for ((i=0; i<${#requested_options[@]}; i++)); do + case "${requested_options[$i]}" in + --no-cache|--why3session) prove_options+=("${requested_options[$i]}") ;; + -j) + i=$((i + 1)) + [[ "${requested_options[$i]:-}" =~ ^[1-9][0-9]*$ ]] || reject_prove_args + prove_options+=(-j "${requested_options[$i]}") + ;; + -j*) + jobs="${requested_options[$i]#-j}" + [[ "$jobs" =~ ^[1-9][0-9]*$ ]] || reject_prove_args + prove_options+=(-j "$jobs") + ;; + *) reject_prove_args ;; + esac + done + + if ! command -v cargo >/dev/null 2>&1 || ! cargo creusot --help >/dev/null 2>&1; then echo "::error::creusot-check[prove]: 'cargo creusot' is not available โ€” NO PROOF WAS PERFORMED. The workflow installs Creusot (pinned) before this step." >&2 exit 2 + fi + + # Creusot v0.14 resolves Why3find configuration at Cargo's workspace + # root, and its default package selection may include other members. + # Resolve the real workspace and select the identified package explicitly; + # a member-local or ambient configuration is not a valid substitute. + command -v jq >/dev/null 2>&1 || { + echo "::error::creusot-check[prove]: jq is required to read Cargo metadata. NO PROOF WAS PERFORMED." >&2 + exit 2 } + source_root="$(git rev-parse --show-toplevel 2>/dev/null || pwd)" + source_root="$(cd "$source_root" && pwd -P)" || exit 2 + : > "$facts_dir/proof-plan" + while IFS= read -r crate; do + [[ -n "$crate" ]] || continue + manifest_path="$(realpath -e -- "$crate/Cargo.toml")" || exit 2 + case "$manifest_path" in + "$source_root"/*) ;; + *) echo "::error::creusot-check[prove]: selected manifest escapes the source repository. NO PROOF WAS PERFORMED." >&2; exit 2 ;; + esac + if ! metadata="$(cargo metadata --format-version 1 --no-deps --manifest-path "$manifest_path")"; then + echo "::error file=$crate/Cargo.toml::creusot-check[prove]: Cargo metadata could not resolve this crate. NO PROOF WAS PERFORMED." >&2 + exit 2 + fi + workspace_root="$(jq -er '.workspace_root | select(type == "string" and length > 0)' <<< "$metadata")" || exit 2 + workspace_root="$(cd "$workspace_root" && pwd -P)" || exit 2 + case "$workspace_root" in + "$source_root"|"$source_root"/*) ;; + *) echo "::error::creusot-check[prove]: Cargo workspace is outside the source repository. NO PROOF WAS PERFORMED." >&2; exit 2 ;; + esac + package="$(jq -er --arg manifest "$manifest_path" '[.packages[] | select(.manifest_path == $manifest) | .name] | if length == 1 then .[0] else empty end' <<< "$metadata")" || { + # A virtual workspace can declare creusot-std for its members, but is + # not itself an executable package. Member manifests are selected by + # the same detector; zero actual packages below remains unavailable. + if [[ "$manifest_path" = "$workspace_root/Cargo.toml" ]]; then + continue + fi + echo "::error file=$crate/Cargo.toml::creusot-check[prove]: no unique package matches the selected manifest. NO PROOF WAS PERFORMED." >&2 + exit 2 + } + if [[ ! "$package" =~ ^[A-Za-z0-9_-]+$ ]] || [[ "$crate" = *$'\t'* ]]; then + echo "::error::creusot-check[prove]: unsupported package or manifest path. NO PROOF WAS PERFORMED." >&2 + exit 2 + fi + if [[ ! -s "$workspace_root/why3find.json" ]]; then + echo "::error file=$workspace_root/why3find.json::creusot-check[prove]: missing Cargo workspace Why3find configuration. NO PROOF WAS PERFORMED." >&2 + exit 2 + fi + configuration_path="$(realpath -e -- "$workspace_root/why3find.json")" || exit 2 + case "$configuration_path" in + "$source_root"/*) ;; + *) echo "::error::creusot-check[prove]: Why3find configuration escapes the source repository. NO PROOF WAS PERFORMED." >&2; exit 2 ;; + esac + if ! jq -e 'type == "object"' "$configuration_path" >/dev/null; then + echo "::error file=$workspace_root/why3find.json::creusot-check[prove]: malformed Why3find configuration. NO PROOF WAS PERFORMED." >&2 + exit 2 + fi + printf '%s\t%s\n' "$crate" "$package" >> "$facts_dir/proof-plan" + crates_expected=$((crates_expected + 1)) + done < "$facts_dir/crates" + # Source-level attributes alone do not identify an executable Cargo target. + # An empty crate list must not execute zero commands and still pass. + if [[ "$crates_expected" -eq 0 ]]; then + echo "::error::creusot-check[prove]: obligations were detected but no Cargo package was selected. NO PROOF WAS PERFORMED." >&2 + exit 2 + fi # ---- planted controls: the prover must be able to say NO ------------- + execution_stage=harness + execution_outcome=failed ctl="$(mktemp -d)" # Create a named control crate under $ctl from the supplied Rust source. # If initialisation fails or why3find.json is missing or empty, remove $ctl @@ -197,7 +345,7 @@ TOML printf '%s\n' "$2" > "$ctl/$1/src/lib.rs" # v0.14 init copies the installed Why3find configuration into this # private control crate. Never initialise or rewrite the caller's tree. - if ! (cd "$ctl/$1" && cargo creusot init "$1") || [ ! -s "$ctl/$1/why3find.json" ]; then + if ! (cd "$ctl/$1" && cargo creusot init "$1") || [[ ! -s "$ctl/$1/why3find.json" ]]; then echo "::error::creusot-check[prove]: control initialisation did not supply why3find.json. NO PROOF WAS PERFORMED." >&2 rm -rf "$ctl"; exit 2 fi @@ -209,8 +357,7 @@ pub fn planted_must_fail() -> u32 { 1 }' #[ensures(result == 2u32)] pub fn planted_must_pass() -> u32 { 2 }' echo "::group::planted control: a false postcondition must NOT prove" - # shellcheck disable=SC2086 - if (cd "$ctl/creusot-control-failing" && cargo creusot $prove_args); then + if (cd "$ctl/creusot-control-failing" && cargo creusot "${prove_options[@]}"); then echo "::endgroup::" echo "::error::creusot-check[prove]: the planted FALSE contract was reported proved (exit 0). This prover cannot fail, so any verdict it gives over the caller's crate is VOID. NO PROOF WAS PERFORMED." >&2 rm -rf "$ctl"; exit 2 @@ -218,34 +365,59 @@ pub fn planted_must_pass() -> u32 { 2 }' echo "::endgroup::" echo "planted control: false contract refused โ€” the oracle can say no." echo "::group::planted control: a true postcondition must prove" - # shellcheck disable=SC2086 - if ! (cd "$ctl/creusot-control-passing" && cargo creusot $prove_args); then + if ! (cd "$ctl/creusot-control-passing" && cargo creusot "${prove_options[@]}") > "$facts_dir/positive-control.log" 2>&1; then echo "::endgroup::" + cat "$facts_dir/positive-control.log" echo "::error::creusot-check[prove]: the planted TRUE contract did not prove. The toolchain is broken (solver or prelude), so a red on the caller's crate would be misattributed. NO PROOF WAS PERFORMED." >&2 rm -rf "$ctl"; exit 2 fi + cat "$facts_dir/positive-control.log" + if ! grep -qE '^Proved \([1-9][0-9]* files\)' "$facts_dir/positive-control.log"; then + echo "::endgroup::" + echo "::error::creusot-check[prove]: the positive control reported no nonzero proved-file denominator. NO CALLER PROOF WAS PERFORMED." >&2 + rm -rf "$ctl"; exit 2 + fi echo "::endgroup::" rm -rf "$ctl" echo "planted control: true contract proved โ€” the oracle can say yes." + controls_passed=true # ---- the caller's crates --------------------------------------------- + execution_stage=substantive + execution_outcome=unavailable fail=0 - while IFS= read -r crate; do - [ -n "$crate" ] || continue - echo "::group::cargo creusot โ€” $crate" - # shellcheck disable=SC2086 - if (cd "$crate" && cargo creusot $prove_args); then + unavailable=0 + while IFS=$'\t' read -r crate package; do + [[ -n "$crate" ]] || continue + echo "::group::cargo creusot โ€” $crate (package $package)" + proof_started=true + crates_attempted=$((crates_attempted + 1)) + proof_log="$facts_dir/caller-$crates_attempted.log" + if (cd "$crate" && cargo creusot -p "$package" "${prove_options[@]}") > "$proof_log" 2>&1; then + cat "$proof_log" echo "::endgroup::" - echo "ok: $crate โ€” every obligation discharged" + if grep -qE '^Proved \([1-9][0-9]* files\)' "$proof_log"; then + echo "ok: $crate โ€” cargo creusot completed with a nonzero proved-file denominator" + else + echo "::error file=$crate/Cargo.toml::creusot-check[prove]: the command exited zero but reported no nonzero proved-file denominator; proof coverage is unavailable." + unavailable=1 + fi else rc=$? + cat "$proof_log" echo "::endgroup::" - echo "::error file=$crate/Cargo.toml::creusot-check[prove]: 'cargo creusot' exited $rc in $crate โ€” at least one obligation is unproved. Fix the contract or the code; never mark it #[trusted] to get green." + echo "::error file=$crate/Cargo.toml::creusot-check[prove]: 'cargo creusot' exited $rc in $crate. The policy step ran; inspect its report to distinguish translation, dependency, solver and obligation failures. This exit alone does not show that a contract is false." fail=1 fi - done < "$facts_dir/crates" - [ "$fail" -eq 0 ] || exit 1 - echo "creusot-check[prove]: all Creusot obligations discharged (trusted axioms: $trusted_count)." + crates_completed=$((crates_completed + 1)) + done < "$facts_dir/proof-plan" + proof_completed=true + execution_outcome=failed + [[ "$fail" -eq 0 ]] || exit 1 + execution_outcome=unavailable + [[ "$unavailable" -eq 0 ]] || exit 2 + execution_outcome=passed + echo "creusot-check[prove]: controls passed and all $crates_completed selected crate commands completed successfully (source-detected trusted axioms: $trusted_count)." exit 0 ;; *) diff --git a/actions/creusot-check/source-facts/Cargo.lock b/actions/creusot-check/source-facts/Cargo.lock new file mode 100644 index 0000000..e5e1b67 --- /dev/null +++ b/actions/creusot-check/source-facts/Cargo.lock @@ -0,0 +1,46 @@ +# This file is automatically @generated by Cargo. +# It is not intended for manual editing. +version = 4 + +[[package]] +name = "creusot-source-facts" +version = "0.1.0" +dependencies = [ + "proc-macro2", + "syn", +] + +[[package]] +name = "proc-macro2" +version = "1.0.107" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "985e7ec9bb745e6ce6535b544d84d6cd6f7ad8bd711c398938ae983b91a766d9" +dependencies = [ + "unicode-ident", +] + +[[package]] +name = "quote" +version = "1.0.47" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "1fbf4db142a473a8d80c26bbf18454ed458bf8d26c8219c331daecfdbd079001" +dependencies = [ + "proc-macro2", +] + +[[package]] +name = "syn" +version = "2.0.119" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "872831b642d1a07999a962a351ed35b955ea2cfc8f3862091e2a240a84f17297" +dependencies = [ + "proc-macro2", + "quote", + "unicode-ident", +] + +[[package]] +name = "unicode-ident" +version = "1.0.27" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "a2c754d6c33795a1c324727428e5a7dedb5b06195f9890bdbcba760d3e246563" diff --git a/actions/creusot-check/source-facts/Cargo.toml b/actions/creusot-check/source-facts/Cargo.toml new file mode 100644 index 0000000..ca21ded --- /dev/null +++ b/actions/creusot-check/source-facts/Cargo.toml @@ -0,0 +1,12 @@ +# SPDX-License-Identifier: MPL-2.0 +[package] +name = "creusot-source-facts" +version = "0.1.0" +edition = "2021" +rust-version = "1.85" +license = "MPL-2.0" +publish = false + +[dependencies] +proc-macro2 = { version = "=1.0.107", features = ["span-locations"] } +syn = { version = "=2.0.119", features = ["full", "visit"] } diff --git a/actions/creusot-check/source-facts/src/main.rs b/actions/creusot-check/source-facts/src/main.rs new file mode 100644 index 0000000..cb480a1 --- /dev/null +++ b/actions/creusot-check/source-facts/src/main.rs @@ -0,0 +1,463 @@ +// SPDX-License-Identifier: MPL-2.0 +// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +// Syntax facts only: syn removes comments/literals from the attribute tree. +// This does not expand macros, resolve modules, or discharge proof obligations. +use std::{collections::HashSet, env, fs, process::ExitCode}; +use syn::{ + parse::Parser, punctuated::Punctuated, spanned::Spanned, visit::Visit, Attribute, Meta, Token, +}; + +#[derive(Clone, Copy, Debug, PartialEq, Eq)] +enum Active { + Yes, + No, + Unknown, +} +impl Active { + fn and(self, other: Self) -> Self { + match (self, other) { + (Self::No, _) | (_, Self::No) => Self::No, + (Self::Yes, Self::Yes) => Self::Yes, + _ => Self::Unknown, + } + } + fn not(self) -> Self { + match self { + Self::Yes => Self::No, + Self::No => Self::Yes, + Self::Unknown => Self::Unknown, + } + } +} + +fn parts(meta: &Meta) -> syn::Result> { + let Meta::List(list) = meta else { + return Err(syn::Error::new(meta.span(), "expected attribute arguments")); + }; + Ok(Punctuated::::parse_terminated + .parse2(list.tokens.clone())? + .into_iter() + .collect()) +} + +// Only facts independent of target/features are evaluated. Unknown conditions +// on proof declarations are unavailable, never guessed active or inactive. +fn condition(meta: &Meta) -> syn::Result { + if matches!(meta, Meta::Path(path) if path.is_ident("creusot")) { + return Ok(Active::Yes); + } + if matches!(meta, Meta::Path(path) if path.is_ident("test")) { + return Ok(Active::No); + } + if meta.path().is_ident("not") { + let values = parts(meta)?; + if values.len() != 1 { + return Err(syn::Error::new(meta.span(), "not requires one condition")); + } + return condition(&values[0]).map(Active::not); + } + if meta.path().is_ident("all") || meta.path().is_ident("any") { + let any = meta.path().is_ident("any"); + let mut result = Active::Yes; + for value in parts(meta)? { + let value = condition(&value)?; + result = result.and(if any { value.not() } else { value }); + } + return Ok(if any { result.not() } else { result }); + } + Ok(Active::Unknown) +} + +fn expand( + meta: &Meta, + active: Active, + result: &mut Vec<(Meta, Active)>, + depth: usize, +) -> syn::Result<()> { + if depth > 64 { + return Err(syn::Error::new( + meta.span(), + "cfg_attr nesting exceeds inspection bound", + )); + } + if meta.path().is_ident("cfg_attr") { + let values = parts(meta)?; + let Some((predicate, attributes)) = values.split_first() else { + return Err(syn::Error::new(meta.span(), "cfg_attr has no condition")); + }; + let active = active.and(condition(predicate)?); + for attribute in attributes { + expand(attribute, active, result, depth + 1)?; + } + } else { + result.push((meta.clone(), active)); + } + Ok(()) +} + +fn expanded(attributes: &[Attribute]) -> syn::Result> { + let mut result = Vec::new(); + for attribute in attributes { + expand(&attribute.meta, Active::Yes, &mut result, 0)?; + } + Ok(result) +} + +fn scope(attributes: &[Attribute], parent: Active) -> syn::Result { + let mut active = parent; + for (meta, included) in expanded(attributes)? { + if !meta.path().is_ident("cfg") || included == Active::No { + continue; + } + let values = parts(&meta)?; + if values.len() != 1 { + return Err(syn::Error::new(meta.span(), "cfg requires one condition")); + } + let value = condition(&values[0])?; + active = active.and(if included == Active::Yes || value == Active::Yes { + value + } else { + Active::Unknown + }); + } + Ok(active) +} + +fn proof_name(meta: &Meta) -> Option { + let names: Vec = meta + .path() + .segments + .iter() + .map(|part| part.ident.to_string()) + .collect(); + let allowed_path = names.len() == 1 + || (names.len() == 2 && matches!(names[0].as_str(), "creusot" | "creusot_contracts")) + || (names.len() == 3 && names[0] == "creusot_std" && names[1] == "macros"); + let name = names.last()?; + if allowed_path + && matches!( + name.as_str(), + "requires" + | "ensures" + | "trusted" + | "invariant" + | "variant" + | "logic" + | "law" + | "open" + | "predicate" + | "terminates" + | "pure" + ) + { + Some(name.clone()) + } else { + None + } +} + +struct Facts { + active: Active, + seen: HashSet<(usize, usize)>, + rows: Vec<(&'static str, usize)>, + error: Option, +} +impl Facts { + fn attributes(&mut self, attributes: &[Attribute], function: bool) { + for attribute in attributes { + let start = attribute.span().start(); + if !self.seen.insert((start.line, start.column)) { + continue; + } + let mut items = Vec::new(); + if let Err(error) = expand(&attribute.meta, self.active, &mut items, 0) { + self.error = Some(error); + continue; + } + for (meta, active) in items { + let Some(name) = proof_name(&meta) else { + continue; + }; + if active == Active::No { + continue; + } + if active == Active::Unknown { + self.error = Some(syn::Error::new( + meta.span(), + "proof attribute has an unresolved cfg condition", + )); + continue; + } + let kind = match name.as_str() { + "requires" | "ensures" if function && matches!(meta, Meta::List(_)) => { + "contract" + } + "trusted" if function => "trusted", + "requires" | "ensures" | "trusted" => { + self.error = Some(syn::Error::new( + meta.span(), + "contract/trusted attribute is not bound to a supported function", + )); + continue; + } + _ => "obligation", + }; + self.rows.push((kind, meta.span().start().line)); + } + } + } + fn enter(&mut self, attributes: &[Attribute]) -> Active { + let previous = self.active; + match scope(attributes, previous) { + Ok(active) => self.active = active, + Err(error) => self.error = Some(error), + } + previous + } +} + +macro_rules! visit_scope { + ($method:ident, $node:ty, $function:expr) => { + fn $method(&mut self, node: &'ast $node) { + let previous = self.enter(&node.attrs); + self.attributes(&node.attrs, $function); + syn::visit::$method(self, node); + self.active = previous; + } + }; +} +impl<'ast> Visit<'ast> for Facts { + // Every attributed node in pinned syn 2.0.119 propagates its cfg scope. + // Functions may occur inside consts, local initializers and expressions, + // not only modules. Recheck this inventory when changing the parser pin. + visit_scope!(visit_arm, syn::Arm, false); + visit_scope!(visit_bare_fn_arg, syn::BareFnArg, false); + visit_scope!(visit_bare_variadic, syn::BareVariadic, false); + visit_scope!(visit_const_param, syn::ConstParam, false); + visit_scope!(visit_derive_input, syn::DeriveInput, false); + visit_scope!(visit_expr_array, syn::ExprArray, false); + visit_scope!(visit_expr_assign, syn::ExprAssign, false); + visit_scope!(visit_expr_async, syn::ExprAsync, false); + visit_scope!(visit_expr_await, syn::ExprAwait, false); + visit_scope!(visit_expr_binary, syn::ExprBinary, false); + visit_scope!(visit_expr_block, syn::ExprBlock, false); + visit_scope!(visit_expr_break, syn::ExprBreak, false); + visit_scope!(visit_expr_call, syn::ExprCall, false); + visit_scope!(visit_expr_cast, syn::ExprCast, false); + visit_scope!(visit_expr_closure, syn::ExprClosure, false); + visit_scope!(visit_expr_const, syn::ExprConst, false); + visit_scope!(visit_expr_continue, syn::ExprContinue, false); + visit_scope!(visit_expr_field, syn::ExprField, false); + visit_scope!(visit_expr_for_loop, syn::ExprForLoop, false); + visit_scope!(visit_expr_group, syn::ExprGroup, false); + visit_scope!(visit_expr_if, syn::ExprIf, false); + visit_scope!(visit_expr_index, syn::ExprIndex, false); + visit_scope!(visit_expr_infer, syn::ExprInfer, false); + visit_scope!(visit_expr_let, syn::ExprLet, false); + visit_scope!(visit_expr_lit, syn::ExprLit, false); + visit_scope!(visit_expr_loop, syn::ExprLoop, false); + visit_scope!(visit_expr_macro, syn::ExprMacro, false); + visit_scope!(visit_expr_match, syn::ExprMatch, false); + visit_scope!(visit_expr_method_call, syn::ExprMethodCall, false); + visit_scope!(visit_expr_paren, syn::ExprParen, false); + visit_scope!(visit_expr_path, syn::ExprPath, false); + visit_scope!(visit_expr_range, syn::ExprRange, false); + visit_scope!(visit_expr_raw_addr, syn::ExprRawAddr, false); + visit_scope!(visit_expr_reference, syn::ExprReference, false); + visit_scope!(visit_expr_repeat, syn::ExprRepeat, false); + visit_scope!(visit_expr_return, syn::ExprReturn, false); + visit_scope!(visit_expr_struct, syn::ExprStruct, false); + visit_scope!(visit_expr_try, syn::ExprTry, false); + visit_scope!(visit_expr_try_block, syn::ExprTryBlock, false); + visit_scope!(visit_expr_tuple, syn::ExprTuple, false); + visit_scope!(visit_expr_unary, syn::ExprUnary, false); + visit_scope!(visit_expr_unsafe, syn::ExprUnsafe, false); + visit_scope!(visit_expr_while, syn::ExprWhile, false); + visit_scope!(visit_expr_yield, syn::ExprYield, false); + visit_scope!(visit_field, syn::Field, false); + visit_scope!(visit_field_pat, syn::FieldPat, false); + visit_scope!(visit_field_value, syn::FieldValue, false); + visit_scope!(visit_file, syn::File, false); + visit_scope!(visit_foreign_item_fn, syn::ForeignItemFn, true); + visit_scope!(visit_foreign_item_macro, syn::ForeignItemMacro, false); + visit_scope!(visit_foreign_item_static, syn::ForeignItemStatic, false); + visit_scope!(visit_foreign_item_type, syn::ForeignItemType, false); + visit_scope!(visit_impl_item_const, syn::ImplItemConst, false); + visit_scope!(visit_impl_item_fn, syn::ImplItemFn, true); + visit_scope!(visit_impl_item_macro, syn::ImplItemMacro, false); + visit_scope!(visit_impl_item_type, syn::ImplItemType, false); + visit_scope!(visit_item_const, syn::ItemConst, false); + visit_scope!(visit_item_enum, syn::ItemEnum, false); + visit_scope!(visit_item_extern_crate, syn::ItemExternCrate, false); + visit_scope!(visit_item_fn, syn::ItemFn, true); + visit_scope!(visit_item_foreign_mod, syn::ItemForeignMod, false); + visit_scope!(visit_item_impl, syn::ItemImpl, false); + visit_scope!(visit_item_macro, syn::ItemMacro, false); + visit_scope!(visit_item_mod, syn::ItemMod, false); + visit_scope!(visit_item_static, syn::ItemStatic, false); + visit_scope!(visit_item_struct, syn::ItemStruct, false); + visit_scope!(visit_item_trait, syn::ItemTrait, false); + visit_scope!(visit_item_trait_alias, syn::ItemTraitAlias, false); + visit_scope!(visit_item_type, syn::ItemType, false); + visit_scope!(visit_item_union, syn::ItemUnion, false); + visit_scope!(visit_item_use, syn::ItemUse, false); + visit_scope!(visit_lifetime_param, syn::LifetimeParam, false); + visit_scope!(visit_local, syn::Local, false); + visit_scope!(visit_pat_ident, syn::PatIdent, false); + visit_scope!(visit_pat_or, syn::PatOr, false); + visit_scope!(visit_pat_paren, syn::PatParen, false); + visit_scope!(visit_pat_reference, syn::PatReference, false); + visit_scope!(visit_pat_rest, syn::PatRest, false); + visit_scope!(visit_pat_slice, syn::PatSlice, false); + visit_scope!(visit_pat_struct, syn::PatStruct, false); + visit_scope!(visit_pat_tuple, syn::PatTuple, false); + visit_scope!(visit_pat_tuple_struct, syn::PatTupleStruct, false); + visit_scope!(visit_pat_type, syn::PatType, false); + visit_scope!(visit_pat_wild, syn::PatWild, false); + visit_scope!(visit_receiver, syn::Receiver, false); + visit_scope!(visit_stmt_macro, syn::StmtMacro, false); + visit_scope!(visit_trait_item_const, syn::TraitItemConst, false); + visit_scope!(visit_trait_item_fn, syn::TraitItemFn, true); + visit_scope!(visit_trait_item_macro, syn::TraitItemMacro, false); + visit_scope!(visit_trait_item_type, syn::TraitItemType, false); + visit_scope!(visit_type_param, syn::TypeParam, false); + visit_scope!(visit_variadic, syn::Variadic, false); + visit_scope!(visit_variant, syn::Variant, false); + fn visit_attribute(&mut self, node: &'ast Attribute) { + self.attributes(std::slice::from_ref(node), false); + } + fn visit_macro(&mut self, node: &'ast syn::Macro) { + if node.path.is_ident("proof_assert") { + match self.active { + Active::Yes => self.rows.push(("obligation", node.span().start().line)), + Active::Unknown => { + self.error = Some(syn::Error::new( + node.span(), + "proof assertion has an unresolved cfg condition", + )) + } + Active::No => {} + } + } + // Macro bodies are intentionally opaque: a macro definition or a + // quoted token tree is not an expanded, bound function declaration. + } +} + +fn inspect(source: &str) -> syn::Result> { + let syntax = syn::parse_file(source)?; + let mut facts = Facts { + active: Active::Yes, + seen: HashSet::new(), + rows: Vec::new(), + error: None, + }; + facts.visit_file(&syntax); + match facts.error { + Some(error) => Err(error), + None => Ok(facts.rows), + } +} + +fn run() -> Result<(), String> { + let files: Vec = env::args().skip(1).collect(); + if files.is_empty() { + return Err("no source files supplied".into()); + } + let mut output = String::new(); + for file in files { + if file.contains(['\t', '\n', '\r']) { + return Err("source path contains an unsupported control character".into()); + } + let source = fs::read_to_string(&file).map_err(|error| format!("{file}: {error}"))?; + let facts = inspect(&source) + .map_err(|error| format!("{file}:{}: {error}", error.span().start().line))?; + for (kind, line) in facts { + output.push_str(&format!("{kind}\t{file}\t{line}\n")); + } + } + // Emit only a complete inspection: a later parse failure cannot leave a + // partial count that a shell pipeline could mistake for complete evidence. + print!("{output}"); + Ok(()) +} + +fn main() -> ExitCode { + match run() { + Ok(()) => ExitCode::SUCCESS, + Err(error) => { + eprintln!("creusot-source-facts: NOT INSPECTED: {error}"); + ExitCode::from(2) + } + } +} + +#[cfg(test)] +mod tests { + use super::inspect; + #[test] + fn conditional_qualified_multiline_contracts_bind_to_functions() { + let rows = inspect("#[cfg_attr(creusot, creusot_std::macros::ensures(\n result == x\n))]\npub fn id(x: u32) -> u32 { x }\n#[cfg_attr(creusot, creusot_std::macros::trusted)]\nfn oracle() {}\n").expect("valid source"); + assert_eq!(rows, vec![("contract", 1), ("trusted", 5)]); + } + #[test] + fn comments_strings_and_unexpanded_macro_tokens_are_not_attributes() { + let rows = inspect( + r####"/* nested /* #[ensures(false)] */ #[trusted] */ +// #[ensures(false)] +/// `#[trusted]` +fn text() { let _ = r###"#[ensures(false)]"###; let _ = "#[trusted]"; } +macro_rules! quoted { () => { #[ensures(false)] fn quoted() {} }; } +"####, + ) + .expect("valid source"); + assert!(rows.is_empty()); + } + #[test] + fn inactive_functions_and_inline_modules_are_not_credited() { + let rows = inspect("#[cfg(not(creusot))] mod native { #[ensures(false)] fn no() {} }\n#[cfg(test)] #[ensures(false)] fn test_only() {}\n#[cfg_attr(not(creusot), ensures(false))] fn other() {}\n").expect("valid source"); + assert!(rows.is_empty()); + } + #[test] + fn every_enclosing_item_and_expression_keeps_its_cfg_scope() { + let sources = [ + "#[cfg(not(creusot))] const _: () = { #[ensures(true)] fn hidden() {} };", + "#[cfg(not(creusot))] static X: () = { #[ensures(true)] fn hidden() {} };", + r#"#[cfg(not(creusot))] extern "C" { #[trusted] fn hidden(); }"#, + "#[cfg(not(creusot))] enum E { V = { #[ensures(true)] fn hidden() {} 0 } }", + "#[cfg(not(creusot))] struct S;", + "fn outer() { #[cfg(not(creusot))] let _ = { #[ensures(true)] fn hidden() {} }; }", + "fn outer() { #[cfg(not(creusot))] if true { #[ensures(true)] fn hidden() {} } }", + "fn outer() { #[cfg(not(creusot))] for _ in 0..1 { #[ensures(true)] fn hidden() {} } }", + "fn outer() { #[cfg(not(creusot))] match 0 { _ => { #[ensures(true)] fn hidden() {} } } }", + "fn outer() { match 0 { #[cfg(not(creusot))] 0 => { #[ensures(true)] fn hidden() {} }, _ => {} } }", + "fn outer() { #[cfg(not(creusot))] const { #[ensures(true)] fn hidden() {} }; }", + ]; + for source in sources { + assert!( + inspect(source).expect("valid inactive source").is_empty(), + "{source}" + ); + let unresolved = source.replace("not(creusot)", r#"feature = "conditional""#); + assert!(inspect(&unresolved).is_err(), "{unresolved}"); + let active = source.replace("not(creusot)", "creusot"); + assert_eq!( + inspect(&active).expect("valid active source").len(), + 1, + "{active}" + ); + } + } + #[test] + fn methods_and_boolean_cfg_are_supported() { + let rows = inspect("struct S; impl S { #[cfg_attr(all(creusot, not(test)), ensures(true))] fn f() {} }\ntrait T { #[cfg_attr(any(test, creusot), requires(true))] fn f(); }\n").expect("valid source"); + assert_eq!(rows.len(), 2); + } + #[test] + fn unresolved_conditions_and_unbound_contracts_are_unavailable() { + assert!(inspect("#[cfg_attr(feature = \"proof\", ensures(true))] fn f() {}").is_err()); + assert!(inspect("#[cfg_attr(creusot = \"unknown\", ensures(true))] fn f() {}").is_err()); + assert!(inspect("#[ensures(true)] struct NotAFunction;").is_err()); + assert!(inspect("#[ensures(true)] fn broken(").is_err()); + } +} diff --git a/actions/creusot-check/test.sh b/actions/creusot-check/test.sh index 2b5d2fb..9f07220 100755 --- a/actions/creusot-check/test.sh +++ b/actions/creusot-check/test.sh @@ -8,7 +8,8 @@ # The prove phase is exercised against a stand-in `cargo-creusot` on PATH. The # stub says "unproved" for any crate whose lib.rs contains the planted # failing marker or a `// UNPROVED` line, and "proved" otherwise โ€” which is -# exactly the contract the real tool must honour (exit code is the oracle). +# the contract the real tool must honour (exit code and nonzero proved-file +# denominator are the oracle). # A second stub that can only say yes must make the gate refuse (exit 2). # This does NOT prove Why3/SMT integration; the planted controls in check.sh # do that at runtime, against the real tool, on every run. @@ -25,6 +26,15 @@ WORK="$(mktemp -d)" trap 'rm -rf "$WORK"' EXIT OUT="$WORK/out" FIX="$WORK/fixture" +ln -s "$here/source-facts" "$WORK/source-facts" + +echo "== the pinned source reader compiles and its syntax controls pass ==" +if ! cargo test --locked --manifest-path "$here/source-facts/Cargo.toml" --target-dir "$WORK/facts/source-target" \ + || ! cargo fmt --manifest-path "$here/source-facts/Cargo.toml" --check \ + || ! cargo clippy --locked --manifest-path "$here/source-facts/Cargo.toml" --target-dir "$WORK/facts/source-target" --all-targets -- -D warnings; then + echo "source reader validation failed" >&2 + exit 1 +fi fresh_fixture() { rm -rf "$FIX"; mkdir -p "$FIX/src" "$FIX/docs" @@ -34,11 +44,15 @@ fresh_fixture() { printf '[package]\nname = "fx"\nversion = "0.1.0"\nedition = "2021"\n\n[dependencies]\n' > "$FIX/Cargo.toml" printf '//! fixture\npub fn id(x: u32) -> u32 { x }\n' > "$FIX/src/lib.rs" printf '= fx\n\nA small crate.\n' > "$FIX/README.adoc" + printf '{"packages":["creusot"],"provers":["z3"]}\n' > "$FIX/why3find.json" git -C "$FIX" add -A && git -C "$FIX" commit -qm fixture } commit() { git -C "$FIX" add -A && git -C "$FIX" commit -qm change >/dev/null; } run_phase() { # [env...] - ( cd "$FIX" && env CREUSOT_GATE_PHASE="$1" CREUSOT_FACTS="$WORK/facts" "${@:2}" \ + local phase="$1"; shift + : > "$WORK/receipt" + ( cd "$FIX" && env CREUSOT_GATE_PHASE="$phase" CREUSOT_FACTS="$WORK/facts" \ + GITHUB_OUTPUT="$WORK/receipt" CREUSOT_SUITE_REVISION=1111111111111111111111111111111111111111 "$@" \ bash --noprofile --norc -e -o pipefail "$checker" ) > "$OUT" 2>&1 RC=$? } @@ -46,27 +60,27 @@ run_phase() { # [env...] echo "== a plain crate: no obligations, no claims, silent ==" fresh_fixture run_phase detect -[ "$RC" -eq 0 ] && ok "detect exits 0" || { bad "detect exits $RC"; cat "$OUT"; } +[[ "$RC" -eq 0 ]] && ok "detect exits 0" || { bad "detect exits $RC"; cat "$OUT"; } grep -qx 'obligations=false' "$OUT" && ok "obligations=false" || bad "obligations misreported: $(cat "$OUT")" grep -qx 'claims=false' "$OUT" && ok "claims=false" || bad "claims misreported" run_phase theatre -[ "$RC" -eq 0 ] && ok "theatre exits 0" || bad "theatre exits $RC" +[[ "$RC" -eq 0 ]] && ok "theatre exits 0" || bad "theatre exits $RC" grep -q 'nothing claims to be' "$OUT" && ok "says it is silent, not green-as-assurance" || bad "no silence notice" run_phase prove -[ "$RC" -eq 2 ] && ok "prove on a crate without obligations is exit 2 (no proof performed)" || bad "prove exits $RC, expected 2" +[[ "$RC" -eq 2 ]] && ok "prove on a crate without obligations is exit 2 (no proof performed)" || bad "prove exits $RC, expected 2" echo "== T1: a README claim with nothing behind it is a hard failure ==" printf '= fx\n\nThis crate is verified with Creusot.\n' > "$FIX/README.adoc"; commit run_phase detect grep -qx 'claims=true' "$OUT" && ok "detect sees the claim" || bad "claim not seen: $(cat "$OUT")" run_phase theatre -[ "$RC" -eq 1 ] && ok "theatre exits 1" || bad "theatre exits $RC, expected 1" +[[ "$RC" -eq 1 ]] && ok "theatre exits 1" || bad "theatre exits $RC, expected 1" grep -q '::error file=README.adoc,line=3::T1 Creusot theatre' "$OUT" && ok "annotates the claim at its line" || bad "T1 annotation missing: $(cat "$OUT")" echo "== a roadmap sentence is not a claim ==" printf '= fx\n\nIt is planned to have this crate verified with Creusot.\n' > "$FIX/README.adoc"; commit run_phase theatre -[ "$RC" -eq 0 ] && ok "planned work does not fire T1" || bad "a plan fired T1 (exit $RC)" +[[ "$RC" -eq 0 ]] && ok "planned work does not fire T1" || bad "a plan fired T1 (exit $RC)" echo "== T2: a Creusot dependency with no contracts is hollow ==" printf '= fx\n\nA small crate.\n' > "$FIX/README.adoc" @@ -75,10 +89,56 @@ run_phase detect grep -qx 'obligations=true' "$OUT" && ok "the dependency counts as an obligation" || bad "dependency not seen" grep -qx 'creusot_version=0.14' "$OUT" && ok "reads the creusot-std version" || bad "version not read: $(cat "$OUT")" run_phase theatre -[ "$RC" -eq 0 ] && ok "hollow is a warning by default" || bad "hollow failed by default (exit $RC)" +[[ "$RC" -eq 0 ]] && ok "hollow is a warning by default" || bad "hollow failed by default (exit $RC)" grep -q '::warning::T2 hollow' "$OUT" && ok "and is named" || bad "T2 warning missing" run_phase theatre ENFORCE_HOLLOW=true -[ "$RC" -eq 1 ] && ok "hollow is a failure with ENFORCE_HOLLOW=true" || bad "ENFORCE_HOLLOW did not fail (exit $RC)" +[[ "$RC" -eq 1 ]] && ok "hollow is a failure with ENFORCE_HOLLOW=true" || bad "ENFORCE_HOLLOW did not fail (exit $RC)" + +echo "== comments, literals and unexpanded tokens cannot make a hollow crate pass ==" +cat > "$FIX/src/lib.rs" <<'RS' +/* nested /* #[ensures(false)] */ #[trusted] */ +// #[requires(false)] +/// Example only: `#[trusted]`. +pub fn text() { let _ = r###"#[ensures(false)]"###; let _ = "#[trusted]"; } +macro_rules! quoted { () => { #[ensures(false)] fn not_expanded() {} }; } +RS +commit +run_phase detect +[[ "$RC" -eq 0 ]] && grep -qx 'contract_count=0' "$OUT" && grep -qx 'trusted_count=0' "$OUT" \ + && ok "comment, string and macro token lookalikes are not declarations" || { bad "source lookalikes were credited"; cat "$OUT"; } +run_phase theatre ENFORCE_HOLLOW=true +[[ "$RC" -eq 1 ]] && ok "lookalikes cannot defeat the enforcing hollow gate" || bad "lookalikes exit $RC" + +echo "== conditional qualified contracts are bound to active functions ==" +cat > "$FIX/src/lib.rs" <<'RS' +#[cfg_attr(creusot, creusot_std::macros::ensures( + result == x +))] +pub fn id(x: u32) -> u32 { x } +#[cfg_attr(creusot, creusot_std::macros::trusted)] +pub fn oracle() -> u32 { 7 } +#[cfg(not(creusot))] +mod native { #[ensures(false)] fn inactive() {} } +#[cfg(test)] #[trusted] fn test_only() {} +RS +commit +run_phase detect +[[ "$RC" -eq 0 ]] && grep -qx 'contract_count=1' "$OUT" && grep -qx 'trusted_count=1' "$OUT" \ + && ok "multiline conditional contract and trusted function are counted exactly" || { bad "conditional facts wrong"; cat "$OUT"; } +run_phase theatre ENFORCE_HOLLOW=true +[[ "$RC" -eq 0 ]] && grep -q 'trusted: src/lib.rs:5' "$OUT" \ + && ok "conditional contract satisfies admission and residue reports the declaration line" || { bad "conditional theatre exits $RC"; cat "$OUT"; } + +echo "== unsupported or malformed declarations cannot provide partial evidence ==" +for source in '#[cfg_attr(feature = "proof", ensures(true))] fn f() {}' '#[ensures(true)] struct NotAFunction;' '#[ensures(true)] fn broken('; do + printf '%s\n' "$source" > "$FIX/src/lib.rs"; commit + run_phase detect + if [[ "$RC" -eq 2 ]] && ! grep -q '^contract_count=' "$OUT"; then + ok "unresolved, unbound or malformed source is unavailable: $source" + else + bad "unsupported source produced facts (exit $RC): $source"; cat "$OUT" + fi +done echo "== contracts present: T2 silent, T3 lists trusted ==" cat > "$FIX/src/lib.rs" <<'RS' @@ -94,7 +154,7 @@ run_phase detect grep -qx 'contract_count=1' "$OUT" && ok "counts one contract" || bad "contract count wrong: $(cat "$OUT")" grep -qx 'trusted_count=1' "$OUT" && ok "counts one trusted" || bad "trusted count wrong" run_phase theatre ENFORCE_HOLLOW=true -[ "$RC" -eq 0 ] && ok "theatre exits 0 with a real contract" || bad "theatre exits $RC" +[[ "$RC" -eq 0 ]] && ok "theatre exits 0 with a real contract" || bad "theatre exits $RC" grep -q 'T3 residue: 1 #\[trusted\]' "$OUT" && ok "the trusted residue is listed" || bad "residue not listed" echo "== prove: stub oracle that CAN say no ==" @@ -103,35 +163,81 @@ cat > "$STAND_IN/cargo-creusot" <<'SH' #!/usr/bin/env bash # v0.14 compiles/proves without a subcommand. A CLI parse error must not # be mistaken for a rejected proof: reject the obsolete invocation here. -[ "${1:-}" = "creusot" ] || exit 64 # cargo supplies the plugin name -[ "${2:-}" != "--help" ] || exit 0 -if [ "${2:-}" = "prove" ]; then +[[ "${1:-}" = "creusot" ]] || exit 64 # cargo supplies the plugin name +[[ "${2:-}" != "--help" ]] || exit 0 +if [[ "${2:-}" = "prove" ]]; then echo "obsolete prove subcommand" >&2; exit 64 fi -if [ "${2:-}" = "init" ]; then +if [[ "${2:-}" = "init" ]]; then # Stand-in only: real init copies the installed tool's configured template. printf '{"stand_in":true}\n' > why3find.json exit 0 fi -if [ -f Cargo.toml ] && grep -q 'name = "creusot-control-' Cargo.toml && [ ! -s why3find.json ]; then +if [[ -f Cargo.toml ]] && grep -q 'name = "creusot-control-' Cargo.toml && [[ ! -s why3find.json ]]; then echo "missing control Why3find configuration" >&2; exit 65 fi +if ! grep -q 'name = "creusot-control-' Cargo.toml; then + package="$(sed -nE 's/^name = "([^"]+)"/\1/p' Cargo.toml)" + if [[ "${2:-}" != -p ]] || [[ "${3:-}" != "$package" ]]; then + echo "caller package was not selected explicitly" >&2; exit 66 + fi + echo "stub: selected package $package" +fi if grep -qE 'planted_must_fail|// UNPROVED' src/lib.rs 2>/dev/null; then echo "stub: 1 goal unproved"; exit 1 fi -echo "stub: all goals proved"; exit 0 +echo "Proved (1 files) [stand-in oracle]"; exit 0 SH chmod +x "$STAND_IN/cargo-creusot" run_phase prove PATH="$STAND_IN:$PATH" -[ "$RC" -eq 0 ] && ok "prove exits 0 when every crate proves" || { bad "prove exits $RC"; cat "$OUT"; } +[[ "$RC" -eq 0 ]] && ok "prove exits 0 when every crate proves" || { bad "prove exits $RC"; cat "$OUT"; } +for fact in execution_stage=substantive execution_outcome=passed controls_passed=true proof_started=true proof_completed=true crates_expected=1 crates_attempted=1 crates_completed=1 proof_exit_code=0; do + grep -qx "$fact" "$WORK/receipt" && ok "execution receipt: $fact" || bad "missing execution fact: $fact" +done +grep -qx "source_revision=$(git -C "$FIX" rev-parse HEAD)" "$WORK/receipt" && ok "records actual checked-out revision" || bad "wrong receipt revision" grep -q 'false contract refused' "$OUT" && ok "planted failing control was exercised" || bad "failing control not run" grep -q 'true contract proved' "$OUT" && ok "planted passing control was exercised" || bad "passing control not run" +echo "== exit zero without a proved-file denominator is not proof evidence ==" +cp "$STAND_IN/cargo-creusot" "$WORK/denominator-oracle" +for output in 'Proved (0 files)' 'completed without a proof report'; do + sed "s/Proved (1 files) \[stand-in oracle\]/$output/" "$WORK/denominator-oracle" > "$STAND_IN/cargo-creusot" + run_phase prove PATH="$STAND_IN:$PATH" + if [[ "$RC" -eq 2 ]] && grep -qx 'execution_stage=harness' "$WORK/receipt" && grep -qx 'proof_started=false' "$WORK/receipt"; then + ok "positive control without work refuses caller execution: $output" + else + bad "empty positive control was credited (exit $RC)"; cat "$OUT" + fi +done +awk '/echo "Proved \(1 files\)/ { print "if ! grep -q '\''name = \"creusot-control-'\'' Cargo.toml; then echo '\''Proved (0 files)'\''; exit 0; fi" } { print }' \ + "$WORK/denominator-oracle" > "$STAND_IN/cargo-creusot" +run_phase prove PATH="$STAND_IN:$PATH" +if [[ "$RC" -eq 2 ]] && grep -qx 'execution_stage=substantive' "$WORK/receipt" && grep -qx 'execution_outcome=unavailable' "$WORK/receipt" \ + && grep -qx 'proof_completed=true' "$WORK/receipt"; then + ok "completed caller command with zero proof work stays unavailable" +else + bad "empty caller proof was credited (exit $RC)"; cat "$OUT" +fi +cp "$WORK/denominator-oracle" "$STAND_IN/cargo-creusot" +echo "== caller proof scope cannot be overridden with extra arguments ==" +run_phase prove PATH="$STAND_IN:$PATH" PROVE_ARGS='--no-cache --why3session -j 2' +[[ "$RC" -eq 0 ]] && ok "supported operational options preserve caller execution" || { bad "supported options exit $RC"; cat "$OUT"; } +run_phase prove PATH="$STAND_IN:$PATH" PROVE_ARGS='-j2' +[[ "$RC" -eq 0 ]] && ok "compact positive prover concurrency is normalised safely" || bad "compact concurrency exits $RC" +for unsafe in '--only coma' '--only=prove' '--dry-run-why3find' '--package fx' '-pfx' '--workspace' '--manifest-path elsewhere/Cargo.toml' '-- --no-default-features' '--why3find-arg=--help' 'planted_*' '--replay' '--no-check-version' '--creusot-rustc=/tmp/fake' 'doc' '-j' '-j 0' '-j=-1' $'--no-cache\n--only coma'; do + run_phase prove PATH="$STAND_IN:$PATH" PROVE_ARGS="$unsafe" + if [[ "$RC" -eq 2 ]] && grep -qx 'execution_stage=setup' "$WORK/receipt" && grep -qx 'proof_started=false' "$WORK/receipt"; then + ok "scope-changing or malformed arguments refused before execution: $unsafe" + else + bad "unsafe arguments accepted or misattributed: $unsafe (exit $RC)" + cat "$OUT" + fi +done echo "== obsolete CLI mutation must not produce a proof verdict ==" original_checker="$checker" -sed 's/cargo creusot \$prove_args/cargo creusot prove $prove_args/g' "$checker" > "$WORK/obsolete-check.sh" +sed 's/cargo creusot "${prove_options\[@\]}"/cargo creusot prove "${prove_options[@]}"/g' "$checker" > "$WORK/obsolete-check.sh" checker="$WORK/obsolete-check.sh" run_phase prove PATH="$STAND_IN:$PATH" -[ "$RC" -eq 2 ] && ok "obsolete subcommand is NOT RUN, never proof success" || bad "obsolete CLI exited $RC" +[[ "$RC" -eq 2 ]] && ok "obsolete subcommand is NOT RUN, never proof success" || bad "obsolete CLI exited $RC" grep -q 'obsolete prove subcommand' "$OUT" && ok "strict v0.14 oracle rejected the obsolete CLI" || bad "CLI mutant was not exercised" checker="$original_checker" echo "== control initialisation must supply configuration ==" @@ -139,32 +245,102 @@ sed '/printf.*stand_in.*why3find.json/d' "$STAND_IN/cargo-creusot" > "$WORK/no-c cp "$STAND_IN/cargo-creusot" "$WORK/good-oracle" cp "$WORK/no-config-oracle" "$STAND_IN/cargo-creusot" run_phase prove PATH="$STAND_IN:$PATH" -[ "$RC" -eq 2 ] && ok "missing control configuration is NOT RUN" || bad "missing configuration exited $RC" +[[ "$RC" -eq 2 ]] && ok "missing control configuration is NOT RUN" || bad "missing configuration exited $RC" grep -q 'control initialisation did not supply why3find.json' "$OUT" && ok "names the actual setup failure" || bad "configuration failure not explained" cp "$WORK/good-oracle" "$STAND_IN/cargo-creusot" +echo "== caller prerequisites must be distinguished from a failed proof ==" +mv "$FIX/why3find.json" "$WORK/caller-config" +run_phase prove PATH="$STAND_IN:$PATH" +[[ "$RC" -eq 2 ]] && ok "missing caller configuration is NOT RUN" || bad "missing caller configuration exited $RC" +grep -qx 'execution_stage=setup' "$WORK/receipt" && grep -qx 'proof_started=false' "$WORK/receipt" && ok "configuration failure is setup, not a caller proof result" || bad "wrong configuration failure attribution" +mv "$WORK/caller-config" "$FIX/why3find.json" +cp "$FIX/Cargo.toml" "$WORK/caller-manifest" +sed -i '/^creusot-std = /d' "$FIX/Cargo.toml" +run_phase prove PATH="$STAND_IN:$PATH" +[[ "$RC" -eq 2 ]] && ok "attributes with zero selected crates cannot pass" || bad "zero crate commands exited $RC" +grep -qx 'crates_attempted=0' "$WORK/receipt" && ok "zero commands recorded honestly" || bad "invented a caller command" +mv "$WORK/caller-manifest" "$FIX/Cargo.toml" +echo "== Cargo workspace configuration and package scope use real metadata ==" +cp -a "$FIX" "$WORK/single-package" +mkdir -p "$FIX/member" +mv "$FIX/src" "$FIX/member/src" +cat > "$FIX/Cargo.toml" <<'TOML' +[workspace] +members = ["member"] +resolver = "2" +[workspace.dependencies] +creusot-std = "0.14" +TOML +cat > "$FIX/member/Cargo.toml" <<'TOML' +[package] +name = "fx-member" +version = "0.1.0" +edition = "2021" +[dependencies] +creusot-std = { workspace = true } +TOML +commit +run_phase prove PATH="$STAND_IN:$PATH" +[[ "$RC" -eq 0 ]] && ok "workspace root configuration serves a real member package" || { bad "workspace root configuration exits $RC"; cat "$OUT"; } +grep -qx 'crates_expected=1' "$WORK/receipt" && ok "virtual workspace is not counted as a second proof package" || bad "virtual workspace was counted" +grep -q 'stub: selected package fx-member' "$OUT" && ok "caller command selects the discovered Cargo package explicitly" || bad "caller package selection missing" +run_phase prove PATH="$STAND_IN:$PATH" WORKING_DIRECTORY=member +[[ "$RC" -eq 0 ]] && ok "member working directory uses the same repository workspace root" || { bad "member working directory exits $RC"; cat "$OUT"; } +mv "$FIX/why3find.json" "$FIX/member/why3find.json" +run_phase prove PATH="$STAND_IN:$PATH" WORKING_DIRECTORY=member +[[ "$RC" -eq 2 ]] && ok "member-local configuration cannot substitute for the workspace configuration" || bad "member-only configuration exits $RC" +grep -qx 'proof_started=false' "$WORK/receipt" && ok "workspace configuration failure precedes caller execution" || bad "workspace configuration failure started a caller command" +mv "$FIX/member/why3find.json" "$WORK/ambient-why3find.json" +ln -s "$WORK/ambient-why3find.json" "$FIX/why3find.json" +run_phase prove PATH="$STAND_IN:$PATH" +[[ "$RC" -eq 2 ]] && ok "configuration symlink outside the source repository is refused" || bad "ambient configuration exits $RC" +rm "$FIX/why3find.json" +mv "$WORK/ambient-why3find.json" "$FIX/why3find.json" +printf 'not JSON\n' > "$FIX/why3find.json" +run_phase prove PATH="$STAND_IN:$PATH" +[[ "$RC" -eq 2 ]] && ok "malformed workspace configuration is a prerequisite failure" || bad "malformed configuration exits $RC" +printf '{"packages":["creusot"],"provers":["z3"]}\n' > "$FIX/why3find.json" +printf '\n[invalid TOML\n' >> "$FIX/member/Cargo.toml" +run_phase prove PATH="$STAND_IN:$PATH" +[[ "$RC" -eq 2 ]] && ok "unresolvable Cargo metadata cannot become a proof result" || bad "invalid Cargo metadata exits $RC" +rm -rf "$FIX" +cp -a "$WORK/single-package" "$FIX" +# A valid Cargo workspace may itself live above the Git repository. The gate +# must refuse its config rather than accept ambient state outside the subject. +printf '[workspace]\nmembers = ["fixture"]\n' > "$WORK/Cargo.toml" +sed -i '/^edition = /a workspace = ".."' "$FIX/Cargo.toml" +run_phase prove PATH="$STAND_IN:$PATH" +[[ "$RC" -eq 2 ]] && ok "a Cargo workspace outside the subject repository is refused" || bad "external Cargo workspace exits $RC" +grep -q 'Cargo workspace is outside the source repository' "$OUT" && ok "external workspace boundary failure is explicit" || { bad "workspace boundary failure not explained"; cat "$OUT"; } +rm "$WORK/Cargo.toml" +rm -rf "$FIX" +mv "$WORK/single-package" "$FIX" printf '// UNPROVED\n' >> "$FIX/src/lib.rs"; commit run_phase prove PATH="$STAND_IN:$PATH" -[ "$RC" -eq 1 ] && ok "an unproved crate fails the gate" || bad "unproved crate exits $RC, expected 1" +[[ "$RC" -eq 1 ]] && ok "an unproved crate fails the gate" || bad "unproved crate exits $RC, expected 1" +grep -qx 'execution_stage=substantive' "$WORK/receipt" && grep -qx 'execution_outcome=failed' "$WORK/receipt" && grep -qx 'proof_completed=true' "$WORK/receipt" && ok "a completed failing invocation is distinguished from a prerequisite" || bad "wrong caller failure attribution" grep -q "::error file=./Cargo.toml::creusot-check\[prove\]" "$OUT" && ok "the failing crate is annotated" || bad "crate not annotated: $(cat "$OUT")" echo "== prove: an oracle that can only say yes makes the verdict VOID ==" cat > "$STAND_IN/cargo-creusot" <<'SH' #!/usr/bin/env bash # Initialise normally, but lie about every proof, including the false control. -if [ "${2:-}" = "init" ]; then +if [[ "${2:-}" = "init" ]]; then printf '{"stand_in":true}\n' > why3find.json fi echo yes; exit 0 SH run_phase prove PATH="$STAND_IN:$PATH" -[ "$RC" -eq 2 ] && ok "exits 2 (NO PROOF WAS PERFORMED)" || bad "exits $RC, expected 2" +[[ "$RC" -eq 2 ]] && ok "exits 2 (NO PROOF WAS PERFORMED)" || bad "exits $RC, expected 2" +grep -qx 'execution_stage=harness' "$WORK/receipt" && grep -qx 'proof_started=false' "$WORK/receipt" && ok "oracle failure is a harness outcome without caller execution" || bad "oracle failure misattributed" grep -q 'cannot fail' "$OUT" && ok "says the prover cannot fail" || bad "no explanation" echo "== prove: no cargo creusot at all is exit 2 ==" rm -f "$STAND_IN/cargo-creusot" run_phase prove PATH="$STAND_IN:/usr/bin:/bin" -[ "$RC" -eq 2 ] && ok "exits 2 without the tool" || bad "exits $RC without the tool, expected 2" +[[ "$RC" -eq 2 ]] && ok "exits 2 without the tool" || bad "exits $RC without the tool, expected 2" echo echo "PASS=$PASS FAIL=$FAIL" -[ "$FAIL" -eq 0 ] +[[ "$FAIL" -eq 0 ]] || exit 1 +bash "$here/verdict-test.sh" diff --git a/actions/creusot-check/verdict-test.sh b/actions/creusot-check/verdict-test.sh new file mode 100644 index 0000000..d0ee38e --- /dev/null +++ b/actions/creusot-check/verdict-test.sh @@ -0,0 +1,80 @@ +#!/usr/bin/env bash +# SPDX-License-Identifier: MPL-2.0 +# SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell +# Tests of the reducer's attribution and acceptance boundary, not proof runs. +set -euo pipefail +here=$(cd "$(dirname "${BASH_SOURCE[0]}")" && pwd) +work=$(mktemp -d) +trap 'rm -rf "$work"' EXIT +passed=0 +case_verdict() { #