From 8110261b6e608e3e722c77f16f13a75422d02c3b Mon Sep 17 00:00:00 2001 From: bordumb Date: Sat, 26 Sep 2026 05:29:24 +0100 Subject: [PATCH] fix(ci): run cold translation when protected-base evidence is missing A pull request whose translation, toolchain, and evidence closures are unchanged reused the formal translation evidence of its base commit's successful CI push run, and failed when there was none. That run is often absent: newer merges cancel superseded main runs, and a run can fail in an unrelated job, still be running, or have expired. Every pull request based on such a commit then failed `formal translation` and `CI qualified`, including the one that repairs main. The lookup now records whether it found evidence instead of failing. When it found none, the job runs the same two clean reproductions a cold plan does. Found evidence is still bound by `formal-translation-reuse`, and a binding failure still fails the job. A pull-request reproduction runs in update mode and rewrites drifted generated files in place, so the step that packages that drift now shares the reproduction's condition; otherwise drift found by the fallback would qualify. The formal workflow validator enforces both conditions and that only found evidence is bound, with a test for each and one against the committed workflow. docs/ci/formal-translation-evidence.md documents the selection and the manual recovery (dispatch ci.yml on the branch). The source closure, the assurance-manifest digests (including the stale digests on main that #172 also refreshes), and the semantic freeze are regenerated to match. --- .github/workflows/ci.yml | 77 +-- docs/PROGRAM_BOARD.md | 1 + docs/ci/formal-artifact-regeneration.md | 4 + docs/ci/formal-translation-evidence.md | 62 +++ formal/assurance-manifest-v1.toml | 484 +++++++++--------- .../qualification/aeneas/source-closure.json | 4 +- release/semantic-freeze-versions.toml | 10 +- release/semantic-freeze.json | 18 +- xtask/src/formal_qualification.rs | 130 ++++- 9 files changed, 495 insertions(+), 295 deletions(-) create mode 100644 docs/ci/formal-translation-evidence.md diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 50cd5118d..2323c7ccb 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -397,8 +397,48 @@ jobs: fi done < <(jq -r --arg repo "$GITHUB_REPOSITORY" --argjson pr "$AUTHS_PR_NUMBER" '.workflow_runs | map(select(.name == "CI" and .head_repository.full_name == $repo and any(.pull_requests[]?; .number == $pr))) | .[:10][] | [.id, .run_attempt, .head_sha] | @tsv' <<< "$runs") echo 'No applicable successful same-PR translation; using two clean reproductions.' >> "$GITHUB_STEP_SUMMARY" + # Protected-base evidence is an optimization, never a precondition. The + # base commit's run may have failed in another job, been cancelled by a + # newer push, still be running, or have expired; `found` then stays false + # and the two clean reproductions below run instead. Located evidence + # that does not bind to this checkout still fails the job. + - id: protected-base-translation + name: Locate protected-base translation evidence + if: needs.ci-plan.outputs.formal_cold_required != 'true' + env: + GH_TOKEN: ${{ github.token }} + AUTHS_BASE_SHA: ${{ github.event.pull_request.base.sha }} + shell: bash + run: | + set -euo pipefail + echo 'found=false' >> "$GITHUB_OUTPUT" + no_evidence() { + echo "Translation: no protected-base evidence for base ${AUTHS_BASE_SHA:-unknown} ($1); executing two clean reproductions." >> "$GITHUB_STEP_SUMMARY" + exit 0 + } + [[ "$AUTHS_BASE_SHA" =~ ^[0-9a-f]{40}$ ]] || no_evidence 'no base commit' + run_id="$(gh api --method GET "repos/${GITHUB_REPOSITORY}/actions/runs" -f head_sha="$AUTHS_BASE_SHA" -f status=success -f per_page=50 --jq '.workflow_runs | map(select(.name == "CI" and .event == "push" and .head_branch == "main")) | first | .id')" || no_evidence 'run lookup failed' + [[ -n "$run_id" && "$run_id" != null ]] || no_evidence 'no successful CI push run on main' + artifact_name="$(gh api --method GET "repos/${GITHUB_REPOSITORY}/actions/runs/${run_id}/artifacts" --jq '.artifacts | map(select(.expired == false and (.name | startswith("auths-formal-translation-")))) | first | .name')" || no_evidence "run ${run_id} artifact lookup failed" + [[ -n "$artifact_name" && "$artifact_name" != null ]] || no_evidence "run ${run_id} has no unexpired translation artifact" + mkdir -p target/reused-formal + gh run download "$run_id" --name "$artifact_name" --dir target/reused-formal || no_evidence "artifact ${artifact_name} could not be downloaded" + mapfile -t evidence < <(find target/reused-formal -type f -name aeneas-qualification.json) + [[ "${#evidence[@]}" == 1 ]] || no_evidence "artifact ${artifact_name} does not hold exactly one evidence file" + echo "AUTHS_REUSED_TRANSLATION_EVIDENCE=${evidence[0]}" >> "$GITHUB_ENV" + echo 'found=true' >> "$GITHUB_OUTPUT" + echo "Translation: protected-base run ${run_id}, artifact ${artifact_name}" >> "$GITHUB_STEP_SUMMARY" + - name: Verify and bind protected-base translation evidence + if: steps.protected-base-translation.outputs.found == 'true' + env: + AUTHS_FORMAL_PHASE_CLOSURE_SHA256: ${{ needs.ci-plan.outputs.formal_translation_digest }} + AUTHS_FORMAL_TOOLCHAIN_CLOSURE_SHA256: ${{ needs.ci-plan.outputs.formal_toolchain_digest }} + AUTHS_FORMAL_EVIDENCE_CLOSURE_SHA256: ${{ needs.ci-plan.outputs.formal_evidence_digest }} + run: cargo xtask ci formal-translation-reuse + # Two clean reproductions run unless a reuse step above located evidence: + # for a cold plan, a same-PR miss, and absent protected-base evidence. - name: Reclaim disk for cold translation - if: needs.ci-plan.outputs.formal_cold_required == 'true' && steps.prior-pr-translation.outputs.reused != 'true' + if: steps.prior-pr-translation.outputs.reused != 'true' && steps.protected-base-translation.outputs.found != 'true' shell: bash run: | set -euo pipefail @@ -406,14 +446,14 @@ jobs: sudo docker system prune --all --force sudo apt-get clean - name: Install pinned Nix with the public Aeneas Cachix substitute - if: needs.ci-plan.outputs.formal_cold_required == 'true' && steps.prior-pr-translation.outputs.reused != 'true' + if: steps.prior-pr-translation.outputs.reused != 'true' && steps.protected-base-translation.outputs.found != 'true' uses: cachix/install-nix-action@ab739621df7a23f52766f9ccc97f38da6b7af14f # v31.10.5 with: extra_nix_config: | extra-substituters = https://hacl.cachix.org extra-trusted-public-keys = hacl.cachix.org-1:FzsZ2xsByOwKwIWNPII7yMOelJNDZ12mDAj3d1eGX0c= - name: Acquire pinned Aeneas and Charon - if: needs.ci-plan.outputs.formal_cold_required == 'true' && steps.prior-pr-translation.outputs.reused != 'true' + if: steps.prior-pr-translation.outputs.reused != 'true' && steps.protected-base-translation.outputs.found != 'true' run: >- nix build --print-build-logs @@ -422,7 +462,7 @@ jobs: github:AeneasVerif/aeneas/3a8586facab25b31bdb1e1f5f45acd60d1cc5ff0#aeneas --out-link target/formal-tools - name: Reproduce translation twice - if: needs.ci-plan.outputs.formal_cold_required == 'true' && steps.prior-pr-translation.outputs.reused != 'true' + if: steps.prior-pr-translation.outputs.reused != 'true' && steps.protected-base-translation.outputs.found != 'true' env: AUTHS_AENEAS_BIN: ${{ github.workspace }}/target/formal-tools/bin/aeneas AUTHS_CHARON_BIN: ${{ github.workspace }}/target/formal-tools/bin/charon @@ -433,7 +473,7 @@ jobs: run: cargo xtask ci formal-translation-reproduce - id: formal-update name: Package a bounded translation update - if: github.event_name == 'pull_request' && needs.ci-plan.outputs.formal_cold_required == 'true' && steps.prior-pr-translation.outputs.reused != 'true' + if: github.event_name == 'pull_request' && steps.prior-pr-translation.outputs.reused != 'true' && steps.protected-base-translation.outputs.found != 'true' env: AUTHS_BASE_SHA: ${{ github.event.pull_request.base.sha }} run: | @@ -463,31 +503,6 @@ jobs: run: | echo "Generated Aeneas output drifted; the bounded updater will commit the reviewed artifact set." exit 1 - - name: Locate protected-base translation evidence - if: needs.ci-plan.outputs.formal_cold_required != 'true' - env: - GH_TOKEN: ${{ github.token }} - AUTHS_BASE_SHA: ${{ github.event.pull_request.base.sha }} - shell: bash - run: | - set -euo pipefail - run_id="$(gh api --method GET "repos/${GITHUB_REPOSITORY}/actions/runs" -f head_sha="$AUTHS_BASE_SHA" -f status=success -f per_page=50 --jq '.workflow_runs | map(select(.name == "CI" and .event == "push" and .head_branch == "main")) | first | .id')" - [[ -n "$run_id" && "$run_id" != null ]] - artifact_name="$(gh api --method GET "repos/${GITHUB_REPOSITORY}/actions/runs/${run_id}/artifacts" --jq '.artifacts | map(select(.expired == false and (.name | startswith("auths-formal-translation-")))) | first | .name')" - [[ -n "$artifact_name" && "$artifact_name" != null ]] - mkdir -p target/reused-formal - gh run download "$run_id" --name "$artifact_name" --dir target/reused-formal - mapfile -t evidence < <(find target/reused-formal -type f -name aeneas-qualification.json) - [[ "${#evidence[@]}" == 1 ]] - echo "AUTHS_REUSED_TRANSLATION_EVIDENCE=${evidence[0]}" >> "$GITHUB_ENV" - echo "Translation: protected-base run ${run_id}, artifact ${artifact_name}" >> "$GITHUB_STEP_SUMMARY" - - name: Verify and bind protected-base translation evidence - if: needs.ci-plan.outputs.formal_cold_required != 'true' - env: - AUTHS_FORMAL_PHASE_CLOSURE_SHA256: ${{ needs.ci-plan.outputs.formal_translation_digest }} - AUTHS_FORMAL_TOOLCHAIN_CLOSURE_SHA256: ${{ needs.ci-plan.outputs.formal_toolchain_digest }} - AUTHS_FORMAL_EVIDENCE_CLOSURE_SHA256: ${{ needs.ci-plan.outputs.formal_evidence_digest }} - run: cargo xtask ci formal-translation-reuse - name: Preserve reusable translation evidence if: steps.formal-update.outputs.update_required != 'true' uses: actions/upload-artifact@043fb46d1a93c77aae656e7c1c64a875d1fc6a0a # v7 @@ -510,7 +525,7 @@ jobs: with: phase: translation started-at: ${{ env.AUTHS_FORMAL_STARTED_AT }} - execution: ${{ steps.prior-pr-translation.outputs.reused == 'true' && 'reused-pr-run' || needs.ci-plan.outputs.formal_cold_required == 'true' && 'executed-cold' || 'reused-protected-base' }} + execution: ${{ steps.prior-pr-translation.outputs.reused == 'true' && 'reused-pr-run' || steps.protected-base-translation.outputs.found == 'true' && 'reused-protected-base' || steps.protected-base-translation.outputs.found == 'false' && 'executed-cold-without-base-evidence' || 'executed-cold' }} formal-kani-run: name: formal Kani diff --git a/docs/PROGRAM_BOARD.md b/docs/PROGRAM_BOARD.md index 4511dc747..543902686 100644 --- a/docs/PROGRAM_BOARD.md +++ b/docs/PROGRAM_BOARD.md @@ -194,6 +194,7 @@ gates do not shrink. | 2026-09-25 | Owner direction: the 2026-09-24 review pass is implemented as PRs in priority order, without filing public issues; a security weakness goes to a private advisory first. Decisions inside that work that the owner has not taken follow rule 8 (narrower reading, logged PROVISIONAL). | ยง3 "Review pass 2026-09-24"; `docs/audit/settled.md` | | 2026-09-25 | PROVISIONAL, taken unattended as the narrower readings for package 2.5 (kernel conformance) of the 2026-09-24 review, whose check-precedence decision the owner delegated: native's current order is codified, and only the attachment-limit line changes in Rust. (1) The canonical action is decoded, with its input, body, and detached-attachment bounds, before the proof, and a failure there carries no plan digest. The Go and TypeScript verifiers decode it the same way and return the native codes: fields read in key order, each bound checked as its field is read, the canonical encoding checked last. (2) Detached attachments are bounded by the aggregate attachment limit, as the spec and CDDL already said; native used the bundle limit, which denied attachments between the two limits and ignored a lowered attachment limit in process. (3) One check precedence, native's: decode (context, canonical action, proof), reference resolution, principal control (registry manifest and configuration first), action binding before any branch, authority branches, then plan and composition. Binding runs the carried body, each action's fields, profile, audience, challenge, evaluation time, channel, shared meaning, extensions, and observation attachments, then attachments, then the profile policy. Each branch runs root control, anchor acceptance, statuses (the anchor, then each grant's status and subject), the resource matcher, namespaces, the budget chain, the delegation walk, terminal coverage, the action's control, assurance, and observation. A statement's control failure is deferred to the branch that needs it. (4) Every grant permission's resource, not only the action's, must lie inside the anchor's namespaces, as native requires. (5) A budget algebra is resolved only where a bounded ceiling is compared, and a value in another algebra is local-policy-denied, the algebra rejecting its input; Go and TypeScript had resolved every algebra up front, including those of unrelated anchors, and returned indeterminate. (6) For a grant after the first, the observation-requirement drop check and the attenuation laws run before any handler evaluates the grant's extensions, so a malformed or over-limit child payload is `observation-requirement-dropped` under a parent with requirements and `delegation-expanded` otherwise, never the handler's code; `protocol.md` now defers to the per-extension laws instead of byte-for-byte preservation. | `core/spec/v1/verification-algorithm.md` "Stages"; `core/spec/v1/registry.md` "Attenuation laws"; `core/spec/v1/protocol.md` "Trust anchor", "Grant"; `core/spec/v1/error-codes.md`; `docs/LIMIT_COVERAGE.md` | | 2026-09-25 | PROVISIONAL, taken unattended as the narrower readings for package 2.6 (status statements) of the 2026-09-24 review, whose `purpose` decision the owner left open: (1) `purpose` is removed from principal-status statements rather than given purpose-scoped selection, which would add role semantics no spec defines. The wire loses key 3 and the later keys move down one, one direct cutover with no reader for the old shape (a ten-entry statement is `malformed-proof`); the carried-status rollback check keys on the principal alone, as selection does; the Python and WASM authoring APIs and the TypeScript engine contract drop the argument. (2) The accepted-extension rule covers every statement about a principal or grant whose status a branch evaluates, whatever its method or issuer and whether or not selection would pick it, checked after the statement's control and before selection; statements about subjects the branch does not evaluate are not checked. (3) As for actions and grants, the first extension in canonical order decides: an identifier the context does not accept is `critical-extension-unknown`, an accepted one `unsupported-critical-extension`. (4) No registered extension, `exact-marker-v1` included, has a status handler, so an accepted extension on an evaluated status statement is never evaluated and is always `unsupported-critical-extension`; a status extension needs a protocol review, an executable model, and a new manifest. | `core/spec/v1/protocol.md` "Evidence and status"; `core/spec/v1/verification-algorithm.md` "Principal status", "Grant status"; `core/spec/v1/registry.md` "Status-statement extensions"; `core/spec/v1/auths-proof.cddl` | +| 2026-09-26 | The owner delegated the choice between two fixes. Taken: when protected-base translation evidence is missing, `formal translation` runs two clean reproductions in the same job, rather than also reusing base runs where only the translation job succeeded. Six of the last eight `main` push runs were cancelled by newer merges, which the second fix cannot cover. Evidence that is found but fails binding still fails the job, and every pull-request reproduction still packages generated drift. | `docs/ci/formal-translation-evidence.md`; `.github/workflows/ci.yml` | ## 5. Not doing diff --git a/docs/ci/formal-artifact-regeneration.md b/docs/ci/formal-artifact-regeneration.md index 4d9b08292..4b030a201 100644 --- a/docs/ci/formal-artifact-regeneration.md +++ b/docs/ci/formal-artifact-regeneration.md @@ -13,6 +13,10 @@ Fork pull requests get the same downloadable artifact and diagnostic summary, bu never receive automatic writeback. A rejected artifact names the violated boundary (for example, an unexpected path, symlink, deletion, stale SHA, or size limit). +[Formal translation evidence](formal-translation-evidence.md) describes when the +translation job reproduces and when it reuses evidence, and how to recover a +pull request by dispatching `ci.yml` on its branch. + ## Architecture ```text diff --git a/docs/ci/formal-translation-evidence.md b/docs/ci/formal-translation-evidence.md new file mode 100644 index 000000000..d2281813d --- /dev/null +++ b/docs/ci/formal-translation-evidence.md @@ -0,0 +1,62 @@ +# Formal translation evidence + +## How the job chooses its evidence + +The `formal translation` job qualifies the Aeneas translation of the exact head +commit in one of three ways. + +| Path | When | Evidence | +| --- | --- | --- | +| Two clean reproductions | The plan requires a cold run: every push, schedule, and dispatch event, and every pull request that changes the translation, toolchain, or evidence closure. Also whenever no reusable evidence was located. | Aeneas and Charon run twice from source; the outputs must be byte-identical and match the committed generated files. | +| Same pull request, earlier run | A pull request with a cold plan whose earlier run's `formal translation` job succeeded with the same closure digests. | That run's result, bound to this checkout. | +| Protected base | A pull request that changes none of those closures, when a successful `CI` push run on `main` for the base commit published translation evidence. | The base run's evidence, bound to this checkout by `cargo xtask ci formal-translation-reuse`. | + +Reuse saves time; it is never required. The ci-plan summary line "reuse +protected-base evidence" states the plan. The translation job decides at run +time whether evidence exists. + +## Missing protected-base evidence + +The base commit often has no successful run. Its run may have failed in another +job, been cancelled by a newer push to `main`, still be running, or have +expired. The job then runs the two clean reproductions itself, and its summary +says why: + +```text +Translation: no protected-base evidence for base (no successful CI push run on main); executing two clean reproductions. +``` + +The phase timing records the execution as `executed-cold-without-base-evidence`. +The fallback checks nothing less than a cold plan does. A pull-request +reproduction runs in update mode: output that differs from the committed files +is packaged for the [formal artifact updater](formal-artifact-regeneration.md) +and the job fails until the regenerated files are committed. + +Evidence that is found but does not bind to this checkout fails the job. There +is no fallback for that case. It means the committed generated artifacts or the +translation source closure differ from what the base run qualified, although +the plan saw no closure change. Look for hand-edited generated files or a file +missing from the planner's closures. + +## Manual recovery + +Dispatch `ci.yml` on the pull request's branch: + +```bash +gh workflow run ci.yml --repo auths-dev/auths-proof --ref +``` + +`workflow_dispatch` is a comprehensive event in +`.github/ci/phase-ownership.toml`. The dispatched run plans every phase, runs +two clean reproductions, and qualifies the branch head. Its checks are recorded +on the same head commit as the pull-request run. The formal artifact updater +starts CI the same way after it pushes regenerated artifacts. A dispatched run +is not a pull-request event, so it never packages generated updates: drift makes +it fail. + +A missing base run no longer needs this. Use it when: + +- found base evidence failed to bind, and the head should be qualified from + source instead of from the base run; or +- a pull-request head needs a complete cold qualification without a new + commit. diff --git a/formal/assurance-manifest-v1.toml b/formal/assurance-manifest-v1.toml index 9bc34de15..06f493396 100644 --- a/formal/assurance-manifest-v1.toml +++ b/formal/assurance-manifest-v1.toml @@ -63,7 +63,7 @@ semantic_source_closure = [ "formal/qualification/aeneas/generated/model/FunsExternal.lean", "formal/qualification/aeneas/generated/model/Types.lean", ] -semantic_source_closure_sha256 = "1a9d3309c0f56c88f64aa0d60d4048d93f6ae0da6336af00d09f342294e9b249" +semantic_source_closure_sha256 = "a625715ca60dcf7c1c9f14b063fd20152a36e46b82c5a8494273c45049cea638" scope = "Rich target-V1 authority semantics over opaque identity carriers and extensional finite sets." residual_assumptions = ["Lean's kernel, the pinned toolchain, the listed foundational axioms, and the theorem premises are trusted."] toolchain_lock_sha256 = "0c45a8a08ac06e313d775e669749097bd3a0abfb8e3395c69416ba0238770d53" @@ -131,7 +131,7 @@ semantic_source_closure = [ "formal/qualification/aeneas/generated/model/FunsExternal.lean", "formal/qualification/aeneas/generated/model/Types.lean", ] -semantic_source_closure_sha256 = "1a9d3309c0f56c88f64aa0d60d4048d93f6ae0da6336af00d09f342294e9b249" +semantic_source_closure_sha256 = "a625715ca60dcf7c1c9f14b063fd20152a36e46b82c5a8494273c45049cea638" scope = "Rich target-V1 authority semantics over opaque identity carriers and extensional finite sets." residual_assumptions = ["Lean's kernel, the pinned toolchain, the listed foundational axioms, and the theorem premises are trusted."] toolchain_lock_sha256 = "0c45a8a08ac06e313d775e669749097bd3a0abfb8e3395c69416ba0238770d53" @@ -199,7 +199,7 @@ semantic_source_closure = [ "formal/qualification/aeneas/generated/model/FunsExternal.lean", "formal/qualification/aeneas/generated/model/Types.lean", ] -semantic_source_closure_sha256 = "1a9d3309c0f56c88f64aa0d60d4048d93f6ae0da6336af00d09f342294e9b249" +semantic_source_closure_sha256 = "a625715ca60dcf7c1c9f14b063fd20152a36e46b82c5a8494273c45049cea638" scope = "Rich target-V1 authority semantics over opaque identity carriers and extensional finite sets." residual_assumptions = ["Lean's kernel, the pinned toolchain, the listed foundational axioms, and the theorem premises are trusted."] toolchain_lock_sha256 = "0c45a8a08ac06e313d775e669749097bd3a0abfb8e3395c69416ba0238770d53" @@ -267,7 +267,7 @@ semantic_source_closure = [ "formal/qualification/aeneas/generated/model/FunsExternal.lean", "formal/qualification/aeneas/generated/model/Types.lean", ] -semantic_source_closure_sha256 = "1a9d3309c0f56c88f64aa0d60d4048d93f6ae0da6336af00d09f342294e9b249" +semantic_source_closure_sha256 = "a625715ca60dcf7c1c9f14b063fd20152a36e46b82c5a8494273c45049cea638" scope = "Rich target-V1 authority semantics over opaque identity carriers and extensional finite sets." residual_assumptions = ["Lean's kernel, the pinned toolchain, the listed foundational axioms, and the theorem premises are trusted."] toolchain_lock_sha256 = "0c45a8a08ac06e313d775e669749097bd3a0abfb8e3395c69416ba0238770d53" @@ -335,7 +335,7 @@ semantic_source_closure = [ "formal/qualification/aeneas/generated/model/FunsExternal.lean", "formal/qualification/aeneas/generated/model/Types.lean", ] -semantic_source_closure_sha256 = "1a9d3309c0f56c88f64aa0d60d4048d93f6ae0da6336af00d09f342294e9b249" +semantic_source_closure_sha256 = "a625715ca60dcf7c1c9f14b063fd20152a36e46b82c5a8494273c45049cea638" scope = "Rich target-V1 authority semantics over opaque identity carriers and extensional finite sets." residual_assumptions = ["Lean's kernel, the pinned toolchain, the listed foundational axioms, and the theorem premises are trusted."] toolchain_lock_sha256 = "0c45a8a08ac06e313d775e669749097bd3a0abfb8e3395c69416ba0238770d53" @@ -400,7 +400,7 @@ semantic_source_closure = [ "formal/qualification/aeneas/generated/model/FunsExternal.lean", "formal/qualification/aeneas/generated/model/Types.lean", ] -semantic_source_closure_sha256 = "1a9d3309c0f56c88f64aa0d60d4048d93f6ae0da6336af00d09f342294e9b249" +semantic_source_closure_sha256 = "a625715ca60dcf7c1c9f14b063fd20152a36e46b82c5a8494273c45049cea638" scope = "Rich target-V1 authority semantics over opaque identity carriers and extensional finite sets." residual_assumptions = ["Lean's kernel, the pinned toolchain, the listed foundational axioms, and the theorem premises are trusted."] toolchain_lock_sha256 = "0c45a8a08ac06e313d775e669749097bd3a0abfb8e3395c69416ba0238770d53" @@ -469,7 +469,7 @@ semantic_source_closure = [ "formal/qualification/aeneas/generated/model/FunsExternal.lean", "formal/qualification/aeneas/generated/model/Types.lean", ] -semantic_source_closure_sha256 = "1a9d3309c0f56c88f64aa0d60d4048d93f6ae0da6336af00d09f342294e9b249" +semantic_source_closure_sha256 = "a625715ca60dcf7c1c9f14b063fd20152a36e46b82c5a8494273c45049cea638" scope = "Rich target-V1 authority semantics over opaque identity carriers and extensional finite sets." residual_assumptions = ["Lean's kernel, the pinned toolchain, the listed foundational axioms, and the theorem premises are trusted."] toolchain_lock_sha256 = "0c45a8a08ac06e313d775e669749097bd3a0abfb8e3395c69416ba0238770d53" @@ -538,7 +538,7 @@ semantic_source_closure = [ "formal/qualification/aeneas/generated/model/FunsExternal.lean", "formal/qualification/aeneas/generated/model/Types.lean", ] -semantic_source_closure_sha256 = "1a9d3309c0f56c88f64aa0d60d4048d93f6ae0da6336af00d09f342294e9b249" +semantic_source_closure_sha256 = "a625715ca60dcf7c1c9f14b063fd20152a36e46b82c5a8494273c45049cea638" scope = "Rich target-V1 authority semantics over opaque identity carriers and extensional finite sets." residual_assumptions = ["Lean's kernel, the pinned toolchain, the listed foundational axioms, and the theorem premises are trusted."] toolchain_lock_sha256 = "0c45a8a08ac06e313d775e669749097bd3a0abfb8e3395c69416ba0238770d53" @@ -607,7 +607,7 @@ semantic_source_closure = [ "formal/qualification/aeneas/generated/model/FunsExternal.lean", "formal/qualification/aeneas/generated/model/Types.lean", ] -semantic_source_closure_sha256 = "1a9d3309c0f56c88f64aa0d60d4048d93f6ae0da6336af00d09f342294e9b249" +semantic_source_closure_sha256 = "a625715ca60dcf7c1c9f14b063fd20152a36e46b82c5a8494273c45049cea638" scope = "Rich target-V1 authority semantics over opaque identity carriers and extensional finite sets." residual_assumptions = ["Lean's kernel, the pinned toolchain, the listed foundational axioms, and the theorem premises are trusted."] toolchain_lock_sha256 = "0c45a8a08ac06e313d775e669749097bd3a0abfb8e3395c69416ba0238770d53" @@ -675,7 +675,7 @@ semantic_source_closure = [ "formal/qualification/aeneas/generated/model/FunsExternal.lean", "formal/qualification/aeneas/generated/model/Types.lean", ] -semantic_source_closure_sha256 = "1a9d3309c0f56c88f64aa0d60d4048d93f6ae0da6336af00d09f342294e9b249" +semantic_source_closure_sha256 = "a625715ca60dcf7c1c9f14b063fd20152a36e46b82c5a8494273c45049cea638" scope = "Rich target-V1 authority semantics over opaque identity carriers and extensional finite sets." residual_assumptions = ["Lean's kernel, the pinned toolchain, the listed foundational axioms, and the theorem premises are trusted."] toolchain_lock_sha256 = "0c45a8a08ac06e313d775e669749097bd3a0abfb8e3395c69416ba0238770d53" @@ -744,7 +744,7 @@ semantic_source_closure = [ "formal/qualification/aeneas/generated/model/FunsExternal.lean", "formal/qualification/aeneas/generated/model/Types.lean", ] -semantic_source_closure_sha256 = "1a9d3309c0f56c88f64aa0d60d4048d93f6ae0da6336af00d09f342294e9b249" +semantic_source_closure_sha256 = "a625715ca60dcf7c1c9f14b063fd20152a36e46b82c5a8494273c45049cea638" scope = "Rich target-V1 authority semantics over opaque identity carriers and extensional finite sets." residual_assumptions = ["Lean's kernel, the pinned toolchain, the listed foundational axioms, and the theorem premises are trusted."] toolchain_lock_sha256 = "0c45a8a08ac06e313d775e669749097bd3a0abfb8e3395c69416ba0238770d53" @@ -813,7 +813,7 @@ semantic_source_closure = [ "formal/qualification/aeneas/generated/model/FunsExternal.lean", "formal/qualification/aeneas/generated/model/Types.lean", ] -semantic_source_closure_sha256 = "1a9d3309c0f56c88f64aa0d60d4048d93f6ae0da6336af00d09f342294e9b249" +semantic_source_closure_sha256 = "a625715ca60dcf7c1c9f14b063fd20152a36e46b82c5a8494273c45049cea638" scope = "Rich target-V1 authority semantics over opaque identity carriers and extensional finite sets." residual_assumptions = ["Lean's kernel, the pinned toolchain, the listed foundational axioms, and the theorem premises are trusted."] toolchain_lock_sha256 = "0c45a8a08ac06e313d775e669749097bd3a0abfb8e3395c69416ba0238770d53" @@ -882,7 +882,7 @@ semantic_source_closure = [ "formal/qualification/aeneas/generated/model/FunsExternal.lean", "formal/qualification/aeneas/generated/model/Types.lean", ] -semantic_source_closure_sha256 = "1a9d3309c0f56c88f64aa0d60d4048d93f6ae0da6336af00d09f342294e9b249" +semantic_source_closure_sha256 = "a625715ca60dcf7c1c9f14b063fd20152a36e46b82c5a8494273c45049cea638" scope = "Rich target-V1 authority semantics over opaque identity carriers and extensional finite sets." residual_assumptions = ["Lean's kernel, the pinned toolchain, the listed foundational axioms, and the theorem premises are trusted."] toolchain_lock_sha256 = "0c45a8a08ac06e313d775e669749097bd3a0abfb8e3395c69416ba0238770d53" @@ -951,7 +951,7 @@ semantic_source_closure = [ "formal/qualification/aeneas/generated/model/FunsExternal.lean", "formal/qualification/aeneas/generated/model/Types.lean", ] -semantic_source_closure_sha256 = "1a9d3309c0f56c88f64aa0d60d4048d93f6ae0da6336af00d09f342294e9b249" +semantic_source_closure_sha256 = "a625715ca60dcf7c1c9f14b063fd20152a36e46b82c5a8494273c45049cea638" scope = "Rich target-V1 authority semantics over opaque identity carriers and extensional finite sets." residual_assumptions = ["Lean's kernel, the pinned toolchain, the listed foundational axioms, and the theorem premises are trusted."] toolchain_lock_sha256 = "0c45a8a08ac06e313d775e669749097bd3a0abfb8e3395c69416ba0238770d53" @@ -1016,7 +1016,7 @@ semantic_source_closure = [ "formal/qualification/aeneas/generated/model/FunsExternal.lean", "formal/qualification/aeneas/generated/model/Types.lean", ] -semantic_source_closure_sha256 = "1a9d3309c0f56c88f64aa0d60d4048d93f6ae0da6336af00d09f342294e9b249" +semantic_source_closure_sha256 = "a625715ca60dcf7c1c9f14b063fd20152a36e46b82c5a8494273c45049cea638" scope = "Rich target-V1 authority semantics over opaque identity carriers and extensional finite sets." residual_assumptions = ["Lean's kernel, the pinned toolchain, the listed foundational axioms, and the theorem premises are trusted."] toolchain_lock_sha256 = "0c45a8a08ac06e313d775e669749097bd3a0abfb8e3395c69416ba0238770d53" @@ -1081,7 +1081,7 @@ semantic_source_closure = [ "formal/qualification/aeneas/generated/model/FunsExternal.lean", "formal/qualification/aeneas/generated/model/Types.lean", ] -semantic_source_closure_sha256 = "1a9d3309c0f56c88f64aa0d60d4048d93f6ae0da6336af00d09f342294e9b249" +semantic_source_closure_sha256 = "a625715ca60dcf7c1c9f14b063fd20152a36e46b82c5a8494273c45049cea638" scope = "Rich target-V1 authority semantics over opaque identity carriers and extensional finite sets." residual_assumptions = ["Lean's kernel, the pinned toolchain, the listed foundational axioms, and the theorem premises are trusted."] toolchain_lock_sha256 = "0c45a8a08ac06e313d775e669749097bd3a0abfb8e3395c69416ba0238770d53" @@ -1146,7 +1146,7 @@ semantic_source_closure = [ "formal/qualification/aeneas/generated/model/FunsExternal.lean", "formal/qualification/aeneas/generated/model/Types.lean", ] -semantic_source_closure_sha256 = "1a9d3309c0f56c88f64aa0d60d4048d93f6ae0da6336af00d09f342294e9b249" +semantic_source_closure_sha256 = "a625715ca60dcf7c1c9f14b063fd20152a36e46b82c5a8494273c45049cea638" scope = "Rich target-V1 authority semantics over opaque identity carriers and extensional finite sets." residual_assumptions = ["Lean's kernel, the pinned toolchain, the listed foundational axioms, and the theorem premises are trusted."] toolchain_lock_sha256 = "0c45a8a08ac06e313d775e669749097bd3a0abfb8e3395c69416ba0238770d53" @@ -1211,7 +1211,7 @@ semantic_source_closure = [ "formal/qualification/aeneas/generated/model/FunsExternal.lean", "formal/qualification/aeneas/generated/model/Types.lean", ] -semantic_source_closure_sha256 = "1a9d3309c0f56c88f64aa0d60d4048d93f6ae0da6336af00d09f342294e9b249" +semantic_source_closure_sha256 = "a625715ca60dcf7c1c9f14b063fd20152a36e46b82c5a8494273c45049cea638" scope = "Rich target-V1 authority semantics over opaque identity carriers and extensional finite sets." residual_assumptions = ["Lean's kernel, the pinned toolchain, the listed foundational axioms, and the theorem premises are trusted."] toolchain_lock_sha256 = "0c45a8a08ac06e313d775e669749097bd3a0abfb8e3395c69416ba0238770d53" @@ -1276,7 +1276,7 @@ semantic_source_closure = [ "formal/qualification/aeneas/generated/model/FunsExternal.lean", "formal/qualification/aeneas/generated/model/Types.lean", ] -semantic_source_closure_sha256 = "1a9d3309c0f56c88f64aa0d60d4048d93f6ae0da6336af00d09f342294e9b249" +semantic_source_closure_sha256 = "a625715ca60dcf7c1c9f14b063fd20152a36e46b82c5a8494273c45049cea638" scope = "Rich target-V1 authority semantics over opaque identity carriers and extensional finite sets." residual_assumptions = ["Lean's kernel, the pinned toolchain, the listed foundational axioms, and the theorem premises are trusted."] toolchain_lock_sha256 = "0c45a8a08ac06e313d775e669749097bd3a0abfb8e3395c69416ba0238770d53" @@ -1341,7 +1341,7 @@ semantic_source_closure = [ "formal/qualification/aeneas/generated/model/FunsExternal.lean", "formal/qualification/aeneas/generated/model/Types.lean", ] -semantic_source_closure_sha256 = "1a9d3309c0f56c88f64aa0d60d4048d93f6ae0da6336af00d09f342294e9b249" +semantic_source_closure_sha256 = "a625715ca60dcf7c1c9f14b063fd20152a36e46b82c5a8494273c45049cea638" scope = "Rich target-V1 authority semantics over opaque identity carriers and extensional finite sets." residual_assumptions = ["Lean's kernel, the pinned toolchain, the listed foundational axioms, and the theorem premises are trusted."] toolchain_lock_sha256 = "0c45a8a08ac06e313d775e669749097bd3a0abfb8e3395c69416ba0238770d53" @@ -1406,7 +1406,7 @@ semantic_source_closure = [ "formal/qualification/aeneas/generated/model/FunsExternal.lean", "formal/qualification/aeneas/generated/model/Types.lean", ] -semantic_source_closure_sha256 = "1a9d3309c0f56c88f64aa0d60d4048d93f6ae0da6336af00d09f342294e9b249" +semantic_source_closure_sha256 = "a625715ca60dcf7c1c9f14b063fd20152a36e46b82c5a8494273c45049cea638" scope = "Rich target-V1 authority semantics over opaque identity carriers and extensional finite sets." residual_assumptions = ["Lean's kernel, the pinned toolchain, the listed foundational axioms, and the theorem premises are trusted."] toolchain_lock_sha256 = "0c45a8a08ac06e313d775e669749097bd3a0abfb8e3395c69416ba0238770d53" @@ -1471,7 +1471,7 @@ semantic_source_closure = [ "formal/qualification/aeneas/generated/model/FunsExternal.lean", "formal/qualification/aeneas/generated/model/Types.lean", ] -semantic_source_closure_sha256 = "1a9d3309c0f56c88f64aa0d60d4048d93f6ae0da6336af00d09f342294e9b249" +semantic_source_closure_sha256 = "a625715ca60dcf7c1c9f14b063fd20152a36e46b82c5a8494273c45049cea638" scope = "Rich target-V1 authority semantics over opaque identity carriers and extensional finite sets." residual_assumptions = ["Lean's kernel, the pinned toolchain, the listed foundational axioms, and the theorem premises are trusted."] toolchain_lock_sha256 = "0c45a8a08ac06e313d775e669749097bd3a0abfb8e3395c69416ba0238770d53" @@ -1536,7 +1536,7 @@ semantic_source_closure = [ "formal/qualification/aeneas/generated/model/FunsExternal.lean", "formal/qualification/aeneas/generated/model/Types.lean", ] -semantic_source_closure_sha256 = "1a9d3309c0f56c88f64aa0d60d4048d93f6ae0da6336af00d09f342294e9b249" +semantic_source_closure_sha256 = "a625715ca60dcf7c1c9f14b063fd20152a36e46b82c5a8494273c45049cea638" scope = "Rich target-V1 authority semantics over opaque identity carriers and extensional finite sets." residual_assumptions = ["Lean's kernel, the pinned toolchain, the listed foundational axioms, and the theorem premises are trusted."] toolchain_lock_sha256 = "0c45a8a08ac06e313d775e669749097bd3a0abfb8e3395c69416ba0238770d53" @@ -1601,7 +1601,7 @@ semantic_source_closure = [ "formal/qualification/aeneas/generated/model/FunsExternal.lean", "formal/qualification/aeneas/generated/model/Types.lean", ] -semantic_source_closure_sha256 = "1a9d3309c0f56c88f64aa0d60d4048d93f6ae0da6336af00d09f342294e9b249" +semantic_source_closure_sha256 = "a625715ca60dcf7c1c9f14b063fd20152a36e46b82c5a8494273c45049cea638" scope = "Rich target-V1 authority semantics over opaque identity carriers and extensional finite sets." residual_assumptions = ["Lean's kernel, the pinned toolchain, the listed foundational axioms, and the theorem premises are trusted."] toolchain_lock_sha256 = "0c45a8a08ac06e313d775e669749097bd3a0abfb8e3395c69416ba0238770d53" @@ -1666,7 +1666,7 @@ semantic_source_closure = [ "formal/qualification/aeneas/generated/model/FunsExternal.lean", "formal/qualification/aeneas/generated/model/Types.lean", ] -semantic_source_closure_sha256 = "1a9d3309c0f56c88f64aa0d60d4048d93f6ae0da6336af00d09f342294e9b249" +semantic_source_closure_sha256 = "a625715ca60dcf7c1c9f14b063fd20152a36e46b82c5a8494273c45049cea638" scope = "Rich target-V1 authority semantics over opaque identity carriers and extensional finite sets." residual_assumptions = ["Lean's kernel, the pinned toolchain, the listed foundational axioms, and the theorem premises are trusted."] toolchain_lock_sha256 = "0c45a8a08ac06e313d775e669749097bd3a0abfb8e3395c69416ba0238770d53" @@ -1731,7 +1731,7 @@ semantic_source_closure = [ "formal/qualification/aeneas/generated/model/FunsExternal.lean", "formal/qualification/aeneas/generated/model/Types.lean", ] -semantic_source_closure_sha256 = "1a9d3309c0f56c88f64aa0d60d4048d93f6ae0da6336af00d09f342294e9b249" +semantic_source_closure_sha256 = "a625715ca60dcf7c1c9f14b063fd20152a36e46b82c5a8494273c45049cea638" scope = "Rich target-V1 authority semantics over opaque identity carriers and extensional finite sets." residual_assumptions = ["Lean's kernel, the pinned toolchain, the listed foundational axioms, and the theorem premises are trusted."] toolchain_lock_sha256 = "0c45a8a08ac06e313d775e669749097bd3a0abfb8e3395c69416ba0238770d53" @@ -1799,7 +1799,7 @@ semantic_source_closure = [ "formal/qualification/aeneas/generated/model/FunsExternal.lean", "formal/qualification/aeneas/generated/model/Types.lean", ] -semantic_source_closure_sha256 = "1a9d3309c0f56c88f64aa0d60d4048d93f6ae0da6336af00d09f342294e9b249" +semantic_source_closure_sha256 = "a625715ca60dcf7c1c9f14b063fd20152a36e46b82c5a8494273c45049cea638" scope = "Rich target-V1 authority semantics over opaque identity carriers and extensional finite sets." residual_assumptions = ["Lean's kernel, the pinned toolchain, the listed foundational axioms, and the theorem premises are trusted."] toolchain_lock_sha256 = "0c45a8a08ac06e313d775e669749097bd3a0abfb8e3395c69416ba0238770d53" @@ -1864,7 +1864,7 @@ semantic_source_closure = [ "formal/qualification/aeneas/generated/model/FunsExternal.lean", "formal/qualification/aeneas/generated/model/Types.lean", ] -semantic_source_closure_sha256 = "1a9d3309c0f56c88f64aa0d60d4048d93f6ae0da6336af00d09f342294e9b249" +semantic_source_closure_sha256 = "a625715ca60dcf7c1c9f14b063fd20152a36e46b82c5a8494273c45049cea638" scope = "Rich target-V1 authority semantics over opaque identity carriers and extensional finite sets." residual_assumptions = ["Lean's kernel, the pinned toolchain, the listed foundational axioms, and the theorem premises are trusted."] toolchain_lock_sha256 = "0c45a8a08ac06e313d775e669749097bd3a0abfb8e3395c69416ba0238770d53" @@ -1929,7 +1929,7 @@ semantic_source_closure = [ "formal/qualification/aeneas/generated/model/FunsExternal.lean", "formal/qualification/aeneas/generated/model/Types.lean", ] -semantic_source_closure_sha256 = "1a9d3309c0f56c88f64aa0d60d4048d93f6ae0da6336af00d09f342294e9b249" +semantic_source_closure_sha256 = "a625715ca60dcf7c1c9f14b063fd20152a36e46b82c5a8494273c45049cea638" scope = "Rich target-V1 authority semantics over opaque identity carriers and extensional finite sets." residual_assumptions = ["Lean's kernel, the pinned toolchain, the listed foundational axioms, and the theorem premises are trusted."] toolchain_lock_sha256 = "0c45a8a08ac06e313d775e669749097bd3a0abfb8e3395c69416ba0238770d53" @@ -1994,7 +1994,7 @@ semantic_source_closure = [ "formal/qualification/aeneas/generated/model/FunsExternal.lean", "formal/qualification/aeneas/generated/model/Types.lean", ] -semantic_source_closure_sha256 = "1a9d3309c0f56c88f64aa0d60d4048d93f6ae0da6336af00d09f342294e9b249" +semantic_source_closure_sha256 = "a625715ca60dcf7c1c9f14b063fd20152a36e46b82c5a8494273c45049cea638" scope = "Rich target-V1 authority semantics over opaque identity carriers and extensional finite sets." residual_assumptions = ["Lean's kernel, the pinned toolchain, the listed foundational axioms, and the theorem premises are trusted."] toolchain_lock_sha256 = "0c45a8a08ac06e313d775e669749097bd3a0abfb8e3395c69416ba0238770d53" @@ -2062,7 +2062,7 @@ semantic_source_closure = [ "formal/qualification/aeneas/generated/model/FunsExternal.lean", "formal/qualification/aeneas/generated/model/Types.lean", ] -semantic_source_closure_sha256 = "1a9d3309c0f56c88f64aa0d60d4048d93f6ae0da6336af00d09f342294e9b249" +semantic_source_closure_sha256 = "a625715ca60dcf7c1c9f14b063fd20152a36e46b82c5a8494273c45049cea638" scope = "Rich target-V1 authority semantics over opaque identity carriers and extensional finite sets." residual_assumptions = ["Lean's kernel, the pinned toolchain, the listed foundational axioms, and the theorem premises are trusted."] toolchain_lock_sha256 = "0c45a8a08ac06e313d775e669749097bd3a0abfb8e3395c69416ba0238770d53" @@ -2127,7 +2127,7 @@ semantic_source_closure = [ "formal/qualification/aeneas/generated/model/FunsExternal.lean", "formal/qualification/aeneas/generated/model/Types.lean", ] -semantic_source_closure_sha256 = "1a9d3309c0f56c88f64aa0d60d4048d93f6ae0da6336af00d09f342294e9b249" +semantic_source_closure_sha256 = "a625715ca60dcf7c1c9f14b063fd20152a36e46b82c5a8494273c45049cea638" scope = "Rich target-V1 authority semantics over opaque identity carriers and extensional finite sets." residual_assumptions = ["Lean's kernel, the pinned toolchain, the listed foundational axioms, and the theorem premises are trusted."] toolchain_lock_sha256 = "0c45a8a08ac06e313d775e669749097bd3a0abfb8e3395c69416ba0238770d53" @@ -2195,7 +2195,7 @@ semantic_source_closure = [ "formal/qualification/aeneas/generated/model/FunsExternal.lean", "formal/qualification/aeneas/generated/model/Types.lean", ] -semantic_source_closure_sha256 = "1a9d3309c0f56c88f64aa0d60d4048d93f6ae0da6336af00d09f342294e9b249" +semantic_source_closure_sha256 = "a625715ca60dcf7c1c9f14b063fd20152a36e46b82c5a8494273c45049cea638" scope = "Rich target-V1 authority semantics over opaque identity carriers and extensional finite sets." residual_assumptions = ["Lean's kernel, the pinned toolchain, the listed foundational axioms, and the theorem premises are trusted."] toolchain_lock_sha256 = "0c45a8a08ac06e313d775e669749097bd3a0abfb8e3395c69416ba0238770d53" @@ -2263,7 +2263,7 @@ semantic_source_closure = [ "formal/qualification/aeneas/generated/model/FunsExternal.lean", "formal/qualification/aeneas/generated/model/Types.lean", ] -semantic_source_closure_sha256 = "1a9d3309c0f56c88f64aa0d60d4048d93f6ae0da6336af00d09f342294e9b249" +semantic_source_closure_sha256 = "a625715ca60dcf7c1c9f14b063fd20152a36e46b82c5a8494273c45049cea638" scope = "Rich target-V1 authority semantics over opaque identity carriers and extensional finite sets." residual_assumptions = ["Lean's kernel, the pinned toolchain, the listed foundational axioms, and the theorem premises are trusted."] toolchain_lock_sha256 = "0c45a8a08ac06e313d775e669749097bd3a0abfb8e3395c69416ba0238770d53" @@ -2331,7 +2331,7 @@ semantic_source_closure = [ "formal/qualification/aeneas/generated/model/FunsExternal.lean", "formal/qualification/aeneas/generated/model/Types.lean", ] -semantic_source_closure_sha256 = "1a9d3309c0f56c88f64aa0d60d4048d93f6ae0da6336af00d09f342294e9b249" +semantic_source_closure_sha256 = "a625715ca60dcf7c1c9f14b063fd20152a36e46b82c5a8494273c45049cea638" scope = "Rich target-V1 authority semantics over opaque identity carriers and extensional finite sets." residual_assumptions = ["Lean's kernel, the pinned toolchain, the listed foundational axioms, and the theorem premises are trusted."] toolchain_lock_sha256 = "0c45a8a08ac06e313d775e669749097bd3a0abfb8e3395c69416ba0238770d53" @@ -2399,7 +2399,7 @@ semantic_source_closure = [ "formal/qualification/aeneas/generated/model/FunsExternal.lean", "formal/qualification/aeneas/generated/model/Types.lean", ] -semantic_source_closure_sha256 = "1a9d3309c0f56c88f64aa0d60d4048d93f6ae0da6336af00d09f342294e9b249" +semantic_source_closure_sha256 = "a625715ca60dcf7c1c9f14b063fd20152a36e46b82c5a8494273c45049cea638" scope = "Rich target-V1 authority semantics over opaque identity carriers and extensional finite sets." residual_assumptions = ["Lean's kernel, the pinned toolchain, the listed foundational axioms, and the theorem premises are trusted."] toolchain_lock_sha256 = "0c45a8a08ac06e313d775e669749097bd3a0abfb8e3395c69416ba0238770d53" @@ -2467,7 +2467,7 @@ semantic_source_closure = [ "formal/qualification/aeneas/generated/model/FunsExternal.lean", "formal/qualification/aeneas/generated/model/Types.lean", ] -semantic_source_closure_sha256 = "1a9d3309c0f56c88f64aa0d60d4048d93f6ae0da6336af00d09f342294e9b249" +semantic_source_closure_sha256 = "a625715ca60dcf7c1c9f14b063fd20152a36e46b82c5a8494273c45049cea638" scope = "Rich target-V1 authority semantics over opaque identity carriers and extensional finite sets." residual_assumptions = ["Lean's kernel, the pinned toolchain, the listed foundational axioms, and the theorem premises are trusted."] toolchain_lock_sha256 = "0c45a8a08ac06e313d775e669749097bd3a0abfb8e3395c69416ba0238770d53" @@ -2536,7 +2536,7 @@ semantic_source_closure = [ "formal/qualification/aeneas/generated/model/FunsExternal.lean", "formal/qualification/aeneas/generated/model/Types.lean", ] -semantic_source_closure_sha256 = "1a9d3309c0f56c88f64aa0d60d4048d93f6ae0da6336af00d09f342294e9b249" +semantic_source_closure_sha256 = "a625715ca60dcf7c1c9f14b063fd20152a36e46b82c5a8494273c45049cea638" scope = "Rich target-V1 authority semantics over opaque identity carriers and extensional finite sets." residual_assumptions = ["Lean's kernel, the pinned toolchain, the listed foundational axioms, and the theorem premises are trusted."] toolchain_lock_sha256 = "0c45a8a08ac06e313d775e669749097bd3a0abfb8e3395c69416ba0238770d53" @@ -2605,7 +2605,7 @@ semantic_source_closure = [ "formal/qualification/aeneas/generated/model/FunsExternal.lean", "formal/qualification/aeneas/generated/model/Types.lean", ] -semantic_source_closure_sha256 = "1a9d3309c0f56c88f64aa0d60d4048d93f6ae0da6336af00d09f342294e9b249" +semantic_source_closure_sha256 = "a625715ca60dcf7c1c9f14b063fd20152a36e46b82c5a8494273c45049cea638" scope = "Rich target-V1 authority semantics over opaque identity carriers and extensional finite sets." residual_assumptions = ["Lean's kernel, the pinned toolchain, the listed foundational axioms, and the theorem premises are trusted."] toolchain_lock_sha256 = "0c45a8a08ac06e313d775e669749097bd3a0abfb8e3395c69416ba0238770d53" @@ -2674,7 +2674,7 @@ semantic_source_closure = [ "formal/qualification/aeneas/generated/model/FunsExternal.lean", "formal/qualification/aeneas/generated/model/Types.lean", ] -semantic_source_closure_sha256 = "1a9d3309c0f56c88f64aa0d60d4048d93f6ae0da6336af00d09f342294e9b249" +semantic_source_closure_sha256 = "a625715ca60dcf7c1c9f14b063fd20152a36e46b82c5a8494273c45049cea638" scope = "Rich target-V1 authority semantics over opaque identity carriers and extensional finite sets." residual_assumptions = ["Lean's kernel, the pinned toolchain, the listed foundational axioms, and the theorem premises are trusted."] toolchain_lock_sha256 = "0c45a8a08ac06e313d775e669749097bd3a0abfb8e3395c69416ba0238770d53" @@ -2742,7 +2742,7 @@ semantic_source_closure = [ "formal/qualification/aeneas/generated/model/FunsExternal.lean", "formal/qualification/aeneas/generated/model/Types.lean", ] -semantic_source_closure_sha256 = "1a9d3309c0f56c88f64aa0d60d4048d93f6ae0da6336af00d09f342294e9b249" +semantic_source_closure_sha256 = "a625715ca60dcf7c1c9f14b063fd20152a36e46b82c5a8494273c45049cea638" scope = "Rich target-V1 authority semantics over opaque identity carriers and extensional finite sets." residual_assumptions = ["Lean's kernel, the pinned toolchain, the listed foundational axioms, and the theorem premises are trusted."] toolchain_lock_sha256 = "0c45a8a08ac06e313d775e669749097bd3a0abfb8e3395c69416ba0238770d53" @@ -2811,7 +2811,7 @@ semantic_source_closure = [ "formal/qualification/aeneas/generated/model/FunsExternal.lean", "formal/qualification/aeneas/generated/model/Types.lean", ] -semantic_source_closure_sha256 = "1a9d3309c0f56c88f64aa0d60d4048d93f6ae0da6336af00d09f342294e9b249" +semantic_source_closure_sha256 = "a625715ca60dcf7c1c9f14b063fd20152a36e46b82c5a8494273c45049cea638" scope = "Rich target-V1 authority semantics over opaque identity carriers and extensional finite sets." residual_assumptions = ["Lean's kernel, the pinned toolchain, the listed foundational axioms, and the theorem premises are trusted."] toolchain_lock_sha256 = "0c45a8a08ac06e313d775e669749097bd3a0abfb8e3395c69416ba0238770d53" @@ -2879,7 +2879,7 @@ semantic_source_closure = [ "formal/qualification/aeneas/generated/model/FunsExternal.lean", "formal/qualification/aeneas/generated/model/Types.lean", ] -semantic_source_closure_sha256 = "1a9d3309c0f56c88f64aa0d60d4048d93f6ae0da6336af00d09f342294e9b249" +semantic_source_closure_sha256 = "a625715ca60dcf7c1c9f14b063fd20152a36e46b82c5a8494273c45049cea638" scope = "Rich target-V1 authority semantics over opaque identity carriers and extensional finite sets." residual_assumptions = ["Lean's kernel, the pinned toolchain, the listed foundational axioms, and the theorem premises are trusted."] toolchain_lock_sha256 = "0c45a8a08ac06e313d775e669749097bd3a0abfb8e3395c69416ba0238770d53" @@ -2947,7 +2947,7 @@ semantic_source_closure = [ "formal/qualification/aeneas/generated/model/FunsExternal.lean", "formal/qualification/aeneas/generated/model/Types.lean", ] -semantic_source_closure_sha256 = "1a9d3309c0f56c88f64aa0d60d4048d93f6ae0da6336af00d09f342294e9b249" +semantic_source_closure_sha256 = "a625715ca60dcf7c1c9f14b063fd20152a36e46b82c5a8494273c45049cea638" scope = "Rich target-V1 authority semantics over opaque identity carriers and extensional finite sets." residual_assumptions = ["Lean's kernel, the pinned toolchain, the listed foundational axioms, and the theorem premises are trusted."] toolchain_lock_sha256 = "0c45a8a08ac06e313d775e669749097bd3a0abfb8e3395c69416ba0238770d53" @@ -3016,7 +3016,7 @@ semantic_source_closure = [ "formal/qualification/aeneas/generated/model/FunsExternal.lean", "formal/qualification/aeneas/generated/model/Types.lean", ] -semantic_source_closure_sha256 = "1a9d3309c0f56c88f64aa0d60d4048d93f6ae0da6336af00d09f342294e9b249" +semantic_source_closure_sha256 = "a625715ca60dcf7c1c9f14b063fd20152a36e46b82c5a8494273c45049cea638" scope = "Rich target-V1 authority semantics over opaque identity carriers and extensional finite sets." residual_assumptions = ["Lean's kernel, the pinned toolchain, the listed foundational axioms, and the theorem premises are trusted."] toolchain_lock_sha256 = "0c45a8a08ac06e313d775e669749097bd3a0abfb8e3395c69416ba0238770d53" @@ -3084,7 +3084,7 @@ semantic_source_closure = [ "formal/qualification/aeneas/generated/model/FunsExternal.lean", "formal/qualification/aeneas/generated/model/Types.lean", ] -semantic_source_closure_sha256 = "1a9d3309c0f56c88f64aa0d60d4048d93f6ae0da6336af00d09f342294e9b249" +semantic_source_closure_sha256 = "a625715ca60dcf7c1c9f14b063fd20152a36e46b82c5a8494273c45049cea638" scope = "Rich target-V1 authority semantics over opaque identity carriers and extensional finite sets." residual_assumptions = ["Lean's kernel, the pinned toolchain, the listed foundational axioms, and the theorem premises are trusted."] toolchain_lock_sha256 = "0c45a8a08ac06e313d775e669749097bd3a0abfb8e3395c69416ba0238770d53" @@ -3153,7 +3153,7 @@ semantic_source_closure = [ "formal/qualification/aeneas/generated/model/FunsExternal.lean", "formal/qualification/aeneas/generated/model/Types.lean", ] -semantic_source_closure_sha256 = "1a9d3309c0f56c88f64aa0d60d4048d93f6ae0da6336af00d09f342294e9b249" +semantic_source_closure_sha256 = "a625715ca60dcf7c1c9f14b063fd20152a36e46b82c5a8494273c45049cea638" scope = "Rich target-V1 authority semantics over opaque identity carriers and extensional finite sets." residual_assumptions = ["Lean's kernel, the pinned toolchain, the listed foundational axioms, and the theorem premises are trusted."] toolchain_lock_sha256 = "0c45a8a08ac06e313d775e669749097bd3a0abfb8e3395c69416ba0238770d53" @@ -3221,7 +3221,7 @@ semantic_source_closure = [ "formal/qualification/aeneas/generated/model/FunsExternal.lean", "formal/qualification/aeneas/generated/model/Types.lean", ] -semantic_source_closure_sha256 = "1a9d3309c0f56c88f64aa0d60d4048d93f6ae0da6336af00d09f342294e9b249" +semantic_source_closure_sha256 = "a625715ca60dcf7c1c9f14b063fd20152a36e46b82c5a8494273c45049cea638" scope = "Rich target-V1 authority semantics over opaque identity carriers and extensional finite sets." residual_assumptions = ["Lean's kernel, the pinned toolchain, the listed foundational axioms, and the theorem premises are trusted."] toolchain_lock_sha256 = "0c45a8a08ac06e313d775e669749097bd3a0abfb8e3395c69416ba0238770d53" @@ -3289,7 +3289,7 @@ semantic_source_closure = [ "formal/qualification/aeneas/generated/model/FunsExternal.lean", "formal/qualification/aeneas/generated/model/Types.lean", ] -semantic_source_closure_sha256 = "1a9d3309c0f56c88f64aa0d60d4048d93f6ae0da6336af00d09f342294e9b249" +semantic_source_closure_sha256 = "a625715ca60dcf7c1c9f14b063fd20152a36e46b82c5a8494273c45049cea638" scope = "Rich target-V1 authority semantics over opaque identity carriers and extensional finite sets." residual_assumptions = ["Lean's kernel, the pinned toolchain, the listed foundational axioms, and the theorem premises are trusted."] toolchain_lock_sha256 = "0c45a8a08ac06e313d775e669749097bd3a0abfb8e3395c69416ba0238770d53" @@ -3357,7 +3357,7 @@ semantic_source_closure = [ "formal/qualification/aeneas/generated/model/FunsExternal.lean", "formal/qualification/aeneas/generated/model/Types.lean", ] -semantic_source_closure_sha256 = "1a9d3309c0f56c88f64aa0d60d4048d93f6ae0da6336af00d09f342294e9b249" +semantic_source_closure_sha256 = "a625715ca60dcf7c1c9f14b063fd20152a36e46b82c5a8494273c45049cea638" scope = "Rich target-V1 authority semantics over opaque identity carriers and extensional finite sets." residual_assumptions = ["Lean's kernel, the pinned toolchain, the listed foundational axioms, and the theorem premises are trusted."] toolchain_lock_sha256 = "0c45a8a08ac06e313d775e669749097bd3a0abfb8e3395c69416ba0238770d53" @@ -3425,7 +3425,7 @@ semantic_source_closure = [ "formal/qualification/aeneas/generated/model/FunsExternal.lean", "formal/qualification/aeneas/generated/model/Types.lean", ] -semantic_source_closure_sha256 = "1a9d3309c0f56c88f64aa0d60d4048d93f6ae0da6336af00d09f342294e9b249" +semantic_source_closure_sha256 = "a625715ca60dcf7c1c9f14b063fd20152a36e46b82c5a8494273c45049cea638" scope = "Rich target-V1 authority semantics over opaque identity carriers and extensional finite sets." residual_assumptions = ["Lean's kernel, the pinned toolchain, the listed foundational axioms, and the theorem premises are trusted."] toolchain_lock_sha256 = "0c45a8a08ac06e313d775e669749097bd3a0abfb8e3395c69416ba0238770d53" @@ -3493,7 +3493,7 @@ semantic_source_closure = [ "formal/qualification/aeneas/generated/model/FunsExternal.lean", "formal/qualification/aeneas/generated/model/Types.lean", ] -semantic_source_closure_sha256 = "1a9d3309c0f56c88f64aa0d60d4048d93f6ae0da6336af00d09f342294e9b249" +semantic_source_closure_sha256 = "a625715ca60dcf7c1c9f14b063fd20152a36e46b82c5a8494273c45049cea638" scope = "Rich target-V1 authority semantics over opaque identity carriers and extensional finite sets." residual_assumptions = ["Lean's kernel, the pinned toolchain, the listed foundational axioms, and the theorem premises are trusted."] toolchain_lock_sha256 = "0c45a8a08ac06e313d775e669749097bd3a0abfb8e3395c69416ba0238770d53" @@ -3561,7 +3561,7 @@ semantic_source_closure = [ "formal/qualification/aeneas/generated/model/FunsExternal.lean", "formal/qualification/aeneas/generated/model/Types.lean", ] -semantic_source_closure_sha256 = "1a9d3309c0f56c88f64aa0d60d4048d93f6ae0da6336af00d09f342294e9b249" +semantic_source_closure_sha256 = "a625715ca60dcf7c1c9f14b063fd20152a36e46b82c5a8494273c45049cea638" scope = "Rich target-V1 authority semantics over opaque identity carriers and extensional finite sets." residual_assumptions = ["Lean's kernel, the pinned toolchain, the listed foundational axioms, and the theorem premises are trusted."] toolchain_lock_sha256 = "0c45a8a08ac06e313d775e669749097bd3a0abfb8e3395c69416ba0238770d53" @@ -3629,7 +3629,7 @@ semantic_source_closure = [ "formal/qualification/aeneas/generated/model/FunsExternal.lean", "formal/qualification/aeneas/generated/model/Types.lean", ] -semantic_source_closure_sha256 = "1a9d3309c0f56c88f64aa0d60d4048d93f6ae0da6336af00d09f342294e9b249" +semantic_source_closure_sha256 = "a625715ca60dcf7c1c9f14b063fd20152a36e46b82c5a8494273c45049cea638" scope = "Rich target-V1 authority semantics over opaque identity carriers and extensional finite sets." residual_assumptions = ["Lean's kernel, the pinned toolchain, the listed foundational axioms, and the theorem premises are trusted."] toolchain_lock_sha256 = "0c45a8a08ac06e313d775e669749097bd3a0abfb8e3395c69416ba0238770d53" @@ -3697,7 +3697,7 @@ semantic_source_closure = [ "formal/qualification/aeneas/generated/model/FunsExternal.lean", "formal/qualification/aeneas/generated/model/Types.lean", ] -semantic_source_closure_sha256 = "1a9d3309c0f56c88f64aa0d60d4048d93f6ae0da6336af00d09f342294e9b249" +semantic_source_closure_sha256 = "a625715ca60dcf7c1c9f14b063fd20152a36e46b82c5a8494273c45049cea638" scope = "Rich target-V1 authority semantics over opaque identity carriers and extensional finite sets." residual_assumptions = ["Lean's kernel, the pinned toolchain, the listed foundational axioms, and the theorem premises are trusted."] toolchain_lock_sha256 = "0c45a8a08ac06e313d775e669749097bd3a0abfb8e3395c69416ba0238770d53" @@ -3765,7 +3765,7 @@ semantic_source_closure = [ "formal/qualification/aeneas/generated/model/FunsExternal.lean", "formal/qualification/aeneas/generated/model/Types.lean", ] -semantic_source_closure_sha256 = "1a9d3309c0f56c88f64aa0d60d4048d93f6ae0da6336af00d09f342294e9b249" +semantic_source_closure_sha256 = "a625715ca60dcf7c1c9f14b063fd20152a36e46b82c5a8494273c45049cea638" scope = "Rich target-V1 authority semantics over opaque identity carriers and extensional finite sets." residual_assumptions = ["Lean's kernel, the pinned toolchain, the listed foundational axioms, and the theorem premises are trusted."] toolchain_lock_sha256 = "0c45a8a08ac06e313d775e669749097bd3a0abfb8e3395c69416ba0238770d53" @@ -3833,7 +3833,7 @@ semantic_source_closure = [ "formal/qualification/aeneas/generated/model/FunsExternal.lean", "formal/qualification/aeneas/generated/model/Types.lean", ] -semantic_source_closure_sha256 = "1a9d3309c0f56c88f64aa0d60d4048d93f6ae0da6336af00d09f342294e9b249" +semantic_source_closure_sha256 = "a625715ca60dcf7c1c9f14b063fd20152a36e46b82c5a8494273c45049cea638" scope = "Rich target-V1 authority semantics over opaque identity carriers and extensional finite sets." residual_assumptions = ["Lean's kernel, the pinned toolchain, the listed foundational axioms, and the theorem premises are trusted."] toolchain_lock_sha256 = "0c45a8a08ac06e313d775e669749097bd3a0abfb8e3395c69416ba0238770d53" @@ -3902,7 +3902,7 @@ semantic_source_closure = [ "formal/qualification/aeneas/generated/model/FunsExternal.lean", "formal/qualification/aeneas/generated/model/Types.lean", ] -semantic_source_closure_sha256 = "1a9d3309c0f56c88f64aa0d60d4048d93f6ae0da6336af00d09f342294e9b249" +semantic_source_closure_sha256 = "a625715ca60dcf7c1c9f14b063fd20152a36e46b82c5a8494273c45049cea638" scope = "Rich target-V1 authority semantics over opaque identity carriers and extensional finite sets." residual_assumptions = ["Lean's kernel, the pinned toolchain, the listed foundational axioms, and the theorem premises are trusted."] toolchain_lock_sha256 = "0c45a8a08ac06e313d775e669749097bd3a0abfb8e3395c69416ba0238770d53" @@ -3971,7 +3971,7 @@ semantic_source_closure = [ "formal/qualification/aeneas/generated/model/FunsExternal.lean", "formal/qualification/aeneas/generated/model/Types.lean", ] -semantic_source_closure_sha256 = "1a9d3309c0f56c88f64aa0d60d4048d93f6ae0da6336af00d09f342294e9b249" +semantic_source_closure_sha256 = "a625715ca60dcf7c1c9f14b063fd20152a36e46b82c5a8494273c45049cea638" scope = "Rich target-V1 authority semantics over opaque identity carriers and extensional finite sets." residual_assumptions = ["Lean's kernel, the pinned toolchain, the listed foundational axioms, and the theorem premises are trusted."] toolchain_lock_sha256 = "0c45a8a08ac06e313d775e669749097bd3a0abfb8e3395c69416ba0238770d53" @@ -4040,7 +4040,7 @@ semantic_source_closure = [ "formal/qualification/aeneas/generated/model/FunsExternal.lean", "formal/qualification/aeneas/generated/model/Types.lean", ] -semantic_source_closure_sha256 = "1a9d3309c0f56c88f64aa0d60d4048d93f6ae0da6336af00d09f342294e9b249" +semantic_source_closure_sha256 = "a625715ca60dcf7c1c9f14b063fd20152a36e46b82c5a8494273c45049cea638" scope = "Rich target-V1 authority semantics over opaque identity carriers and extensional finite sets." residual_assumptions = ["Lean's kernel, the pinned toolchain, the listed foundational axioms, and the theorem premises are trusted."] toolchain_lock_sha256 = "0c45a8a08ac06e313d775e669749097bd3a0abfb8e3395c69416ba0238770d53" @@ -4109,7 +4109,7 @@ semantic_source_closure = [ "formal/qualification/aeneas/generated/model/FunsExternal.lean", "formal/qualification/aeneas/generated/model/Types.lean", ] -semantic_source_closure_sha256 = "1a9d3309c0f56c88f64aa0d60d4048d93f6ae0da6336af00d09f342294e9b249" +semantic_source_closure_sha256 = "a625715ca60dcf7c1c9f14b063fd20152a36e46b82c5a8494273c45049cea638" scope = "Rich target-V1 authority semantics over opaque identity carriers and extensional finite sets." residual_assumptions = ["Lean's kernel, the pinned toolchain, the listed foundational axioms, and the theorem premises are trusted."] toolchain_lock_sha256 = "0c45a8a08ac06e313d775e669749097bd3a0abfb8e3395c69416ba0238770d53" @@ -4178,7 +4178,7 @@ semantic_source_closure = [ "formal/qualification/aeneas/generated/model/FunsExternal.lean", "formal/qualification/aeneas/generated/model/Types.lean", ] -semantic_source_closure_sha256 = "1a9d3309c0f56c88f64aa0d60d4048d93f6ae0da6336af00d09f342294e9b249" +semantic_source_closure_sha256 = "a625715ca60dcf7c1c9f14b063fd20152a36e46b82c5a8494273c45049cea638" scope = "Rich target-V1 authority semantics over opaque identity carriers and extensional finite sets." residual_assumptions = ["Lean's kernel, the pinned toolchain, the listed foundational axioms, and the theorem premises are trusted."] toolchain_lock_sha256 = "0c45a8a08ac06e313d775e669749097bd3a0abfb8e3395c69416ba0238770d53" @@ -4246,7 +4246,7 @@ semantic_source_closure = [ "formal/qualification/aeneas/generated/model/FunsExternal.lean", "formal/qualification/aeneas/generated/model/Types.lean", ] -semantic_source_closure_sha256 = "1a9d3309c0f56c88f64aa0d60d4048d93f6ae0da6336af00d09f342294e9b249" +semantic_source_closure_sha256 = "a625715ca60dcf7c1c9f14b063fd20152a36e46b82c5a8494273c45049cea638" scope = "Rich target-V1 authority semantics over opaque identity carriers and extensional finite sets." residual_assumptions = ["Lean's kernel, the pinned toolchain, the listed foundational axioms, and the theorem premises are trusted."] toolchain_lock_sha256 = "0c45a8a08ac06e313d775e669749097bd3a0abfb8e3395c69416ba0238770d53" @@ -4314,7 +4314,7 @@ semantic_source_closure = [ "formal/qualification/aeneas/generated/model/FunsExternal.lean", "formal/qualification/aeneas/generated/model/Types.lean", ] -semantic_source_closure_sha256 = "1a9d3309c0f56c88f64aa0d60d4048d93f6ae0da6336af00d09f342294e9b249" +semantic_source_closure_sha256 = "a625715ca60dcf7c1c9f14b063fd20152a36e46b82c5a8494273c45049cea638" scope = "Rich target-V1 authority semantics over opaque identity carriers and extensional finite sets." residual_assumptions = ["Lean's kernel, the pinned toolchain, the listed foundational axioms, and the theorem premises are trusted."] toolchain_lock_sha256 = "0c45a8a08ac06e313d775e669749097bd3a0abfb8e3395c69416ba0238770d53" @@ -4383,7 +4383,7 @@ semantic_source_closure = [ "formal/qualification/aeneas/generated/model/FunsExternal.lean", "formal/qualification/aeneas/generated/model/Types.lean", ] -semantic_source_closure_sha256 = "1a9d3309c0f56c88f64aa0d60d4048d93f6ae0da6336af00d09f342294e9b249" +semantic_source_closure_sha256 = "a625715ca60dcf7c1c9f14b063fd20152a36e46b82c5a8494273c45049cea638" scope = "Rich target-V1 authority semantics over opaque identity carriers and extensional finite sets." residual_assumptions = ["Lean's kernel, the pinned toolchain, the listed foundational axioms, and the theorem premises are trusted."] toolchain_lock_sha256 = "0c45a8a08ac06e313d775e669749097bd3a0abfb8e3395c69416ba0238770d53" @@ -4452,7 +4452,7 @@ semantic_source_closure = [ "formal/qualification/aeneas/generated/model/FunsExternal.lean", "formal/qualification/aeneas/generated/model/Types.lean", ] -semantic_source_closure_sha256 = "1a9d3309c0f56c88f64aa0d60d4048d93f6ae0da6336af00d09f342294e9b249" +semantic_source_closure_sha256 = "a625715ca60dcf7c1c9f14b063fd20152a36e46b82c5a8494273c45049cea638" scope = "Rich target-V1 authority semantics over opaque identity carriers and extensional finite sets." residual_assumptions = ["Lean's kernel, the pinned toolchain, the listed foundational axioms, and the theorem premises are trusted."] toolchain_lock_sha256 = "0c45a8a08ac06e313d775e669749097bd3a0abfb8e3395c69416ba0238770d53" @@ -4521,7 +4521,7 @@ semantic_source_closure = [ "formal/qualification/aeneas/generated/model/FunsExternal.lean", "formal/qualification/aeneas/generated/model/Types.lean", ] -semantic_source_closure_sha256 = "1a9d3309c0f56c88f64aa0d60d4048d93f6ae0da6336af00d09f342294e9b249" +semantic_source_closure_sha256 = "a625715ca60dcf7c1c9f14b063fd20152a36e46b82c5a8494273c45049cea638" scope = "Rich target-V1 authority semantics over opaque identity carriers and extensional finite sets." residual_assumptions = ["Lean's kernel, the pinned toolchain, the listed foundational axioms, and the theorem premises are trusted."] toolchain_lock_sha256 = "0c45a8a08ac06e313d775e669749097bd3a0abfb8e3395c69416ba0238770d53" @@ -4590,7 +4590,7 @@ semantic_source_closure = [ "formal/qualification/aeneas/generated/model/FunsExternal.lean", "formal/qualification/aeneas/generated/model/Types.lean", ] -semantic_source_closure_sha256 = "1a9d3309c0f56c88f64aa0d60d4048d93f6ae0da6336af00d09f342294e9b249" +semantic_source_closure_sha256 = "a625715ca60dcf7c1c9f14b063fd20152a36e46b82c5a8494273c45049cea638" scope = "Rich target-V1 authority semantics over opaque identity carriers and extensional finite sets." residual_assumptions = ["Lean's kernel, the pinned toolchain, the listed foundational axioms, and the theorem premises are trusted."] toolchain_lock_sha256 = "0c45a8a08ac06e313d775e669749097bd3a0abfb8e3395c69416ba0238770d53" @@ -4659,7 +4659,7 @@ semantic_source_closure = [ "formal/qualification/aeneas/generated/model/FunsExternal.lean", "formal/qualification/aeneas/generated/model/Types.lean", ] -semantic_source_closure_sha256 = "1a9d3309c0f56c88f64aa0d60d4048d93f6ae0da6336af00d09f342294e9b249" +semantic_source_closure_sha256 = "a625715ca60dcf7c1c9f14b063fd20152a36e46b82c5a8494273c45049cea638" scope = "Rich target-V1 authority semantics over opaque identity carriers and extensional finite sets." residual_assumptions = ["Lean's kernel, the pinned toolchain, the listed foundational axioms, and the theorem premises are trusted."] toolchain_lock_sha256 = "0c45a8a08ac06e313d775e669749097bd3a0abfb8e3395c69416ba0238770d53" @@ -4728,7 +4728,7 @@ semantic_source_closure = [ "formal/qualification/aeneas/generated/model/FunsExternal.lean", "formal/qualification/aeneas/generated/model/Types.lean", ] -semantic_source_closure_sha256 = "1a9d3309c0f56c88f64aa0d60d4048d93f6ae0da6336af00d09f342294e9b249" +semantic_source_closure_sha256 = "a625715ca60dcf7c1c9f14b063fd20152a36e46b82c5a8494273c45049cea638" scope = "Rich target-V1 authority semantics over opaque identity carriers and extensional finite sets." residual_assumptions = ["Lean's kernel, the pinned toolchain, the listed foundational axioms, and the theorem premises are trusted."] toolchain_lock_sha256 = "0c45a8a08ac06e313d775e669749097bd3a0abfb8e3395c69416ba0238770d53" @@ -4797,7 +4797,7 @@ semantic_source_closure = [ "formal/qualification/aeneas/generated/model/FunsExternal.lean", "formal/qualification/aeneas/generated/model/Types.lean", ] -semantic_source_closure_sha256 = "1a9d3309c0f56c88f64aa0d60d4048d93f6ae0da6336af00d09f342294e9b249" +semantic_source_closure_sha256 = "a625715ca60dcf7c1c9f14b063fd20152a36e46b82c5a8494273c45049cea638" scope = "Rich target-V1 authority semantics over opaque identity carriers and extensional finite sets." residual_assumptions = ["Lean's kernel, the pinned toolchain, the listed foundational axioms, and the theorem premises are trusted."] toolchain_lock_sha256 = "0c45a8a08ac06e313d775e669749097bd3a0abfb8e3395c69416ba0238770d53" @@ -4866,7 +4866,7 @@ semantic_source_closure = [ "formal/qualification/aeneas/generated/model/FunsExternal.lean", "formal/qualification/aeneas/generated/model/Types.lean", ] -semantic_source_closure_sha256 = "1a9d3309c0f56c88f64aa0d60d4048d93f6ae0da6336af00d09f342294e9b249" +semantic_source_closure_sha256 = "a625715ca60dcf7c1c9f14b063fd20152a36e46b82c5a8494273c45049cea638" scope = "Rich target-V1 authority semantics over opaque identity carriers and extensional finite sets." residual_assumptions = ["Lean's kernel, the pinned toolchain, the listed foundational axioms, and the theorem premises are trusted."] toolchain_lock_sha256 = "0c45a8a08ac06e313d775e669749097bd3a0abfb8e3395c69416ba0238770d53" @@ -4935,7 +4935,7 @@ semantic_source_closure = [ "formal/qualification/aeneas/generated/model/FunsExternal.lean", "formal/qualification/aeneas/generated/model/Types.lean", ] -semantic_source_closure_sha256 = "1a9d3309c0f56c88f64aa0d60d4048d93f6ae0da6336af00d09f342294e9b249" +semantic_source_closure_sha256 = "a625715ca60dcf7c1c9f14b063fd20152a36e46b82c5a8494273c45049cea638" scope = "Rich target-V1 authority semantics over opaque identity carriers and extensional finite sets." residual_assumptions = ["Lean's kernel, the pinned toolchain, the listed foundational axioms, and the theorem premises are trusted."] toolchain_lock_sha256 = "0c45a8a08ac06e313d775e669749097bd3a0abfb8e3395c69416ba0238770d53" @@ -5003,7 +5003,7 @@ semantic_source_closure = [ "formal/qualification/aeneas/generated/model/FunsExternal.lean", "formal/qualification/aeneas/generated/model/Types.lean", ] -semantic_source_closure_sha256 = "1a9d3309c0f56c88f64aa0d60d4048d93f6ae0da6336af00d09f342294e9b249" +semantic_source_closure_sha256 = "a625715ca60dcf7c1c9f14b063fd20152a36e46b82c5a8494273c45049cea638" scope = "Rich target-V1 authority semantics over opaque identity carriers and extensional finite sets." residual_assumptions = ["Lean's kernel, the pinned toolchain, the listed foundational axioms, and the theorem premises are trusted."] toolchain_lock_sha256 = "0c45a8a08ac06e313d775e669749097bd3a0abfb8e3395c69416ba0238770d53" @@ -5071,7 +5071,7 @@ semantic_source_closure = [ "formal/qualification/aeneas/generated/model/FunsExternal.lean", "formal/qualification/aeneas/generated/model/Types.lean", ] -semantic_source_closure_sha256 = "1a9d3309c0f56c88f64aa0d60d4048d93f6ae0da6336af00d09f342294e9b249" +semantic_source_closure_sha256 = "a625715ca60dcf7c1c9f14b063fd20152a36e46b82c5a8494273c45049cea638" scope = "Rich target-V1 authority semantics over opaque identity carriers and extensional finite sets." residual_assumptions = ["Lean's kernel, the pinned toolchain, the listed foundational axioms, and the theorem premises are trusted."] toolchain_lock_sha256 = "0c45a8a08ac06e313d775e669749097bd3a0abfb8e3395c69416ba0238770d53" @@ -5139,7 +5139,7 @@ semantic_source_closure = [ "formal/qualification/aeneas/generated/model/FunsExternal.lean", "formal/qualification/aeneas/generated/model/Types.lean", ] -semantic_source_closure_sha256 = "1a9d3309c0f56c88f64aa0d60d4048d93f6ae0da6336af00d09f342294e9b249" +semantic_source_closure_sha256 = "a625715ca60dcf7c1c9f14b063fd20152a36e46b82c5a8494273c45049cea638" scope = "Rich target-V1 authority semantics over opaque identity carriers and extensional finite sets." residual_assumptions = ["Lean's kernel, the pinned toolchain, the listed foundational axioms, and the theorem premises are trusted."] toolchain_lock_sha256 = "0c45a8a08ac06e313d775e669749097bd3a0abfb8e3395c69416ba0238770d53" @@ -5207,7 +5207,7 @@ semantic_source_closure = [ "formal/qualification/aeneas/generated/model/FunsExternal.lean", "formal/qualification/aeneas/generated/model/Types.lean", ] -semantic_source_closure_sha256 = "1a9d3309c0f56c88f64aa0d60d4048d93f6ae0da6336af00d09f342294e9b249" +semantic_source_closure_sha256 = "a625715ca60dcf7c1c9f14b063fd20152a36e46b82c5a8494273c45049cea638" scope = "Rich target-V1 authority semantics over opaque identity carriers and extensional finite sets." residual_assumptions = ["Lean's kernel, the pinned toolchain, the listed foundational axioms, and the theorem premises are trusted."] toolchain_lock_sha256 = "0c45a8a08ac06e313d775e669749097bd3a0abfb8e3395c69416ba0238770d53" @@ -5275,7 +5275,7 @@ semantic_source_closure = [ "formal/qualification/aeneas/generated/model/FunsExternal.lean", "formal/qualification/aeneas/generated/model/Types.lean", ] -semantic_source_closure_sha256 = "1a9d3309c0f56c88f64aa0d60d4048d93f6ae0da6336af00d09f342294e9b249" +semantic_source_closure_sha256 = "a625715ca60dcf7c1c9f14b063fd20152a36e46b82c5a8494273c45049cea638" scope = "Rich target-V1 authority semantics over opaque identity carriers and extensional finite sets." residual_assumptions = ["Lean's kernel, the pinned toolchain, the listed foundational axioms, and the theorem premises are trusted."] toolchain_lock_sha256 = "0c45a8a08ac06e313d775e669749097bd3a0abfb8e3395c69416ba0238770d53" @@ -5344,7 +5344,7 @@ semantic_source_closure = [ "formal/qualification/aeneas/generated/model/FunsExternal.lean", "formal/qualification/aeneas/generated/model/Types.lean", ] -semantic_source_closure_sha256 = "1a9d3309c0f56c88f64aa0d60d4048d93f6ae0da6336af00d09f342294e9b249" +semantic_source_closure_sha256 = "a625715ca60dcf7c1c9f14b063fd20152a36e46b82c5a8494273c45049cea638" scope = "Rich target-V1 authority semantics over opaque identity carriers and extensional finite sets." residual_assumptions = ["Lean's kernel, the pinned toolchain, the listed foundational axioms, and the theorem premises are trusted."] toolchain_lock_sha256 = "0c45a8a08ac06e313d775e669749097bd3a0abfb8e3395c69416ba0238770d53" @@ -5413,7 +5413,7 @@ semantic_source_closure = [ "formal/qualification/aeneas/generated/model/FunsExternal.lean", "formal/qualification/aeneas/generated/model/Types.lean", ] -semantic_source_closure_sha256 = "1a9d3309c0f56c88f64aa0d60d4048d93f6ae0da6336af00d09f342294e9b249" +semantic_source_closure_sha256 = "a625715ca60dcf7c1c9f14b063fd20152a36e46b82c5a8494273c45049cea638" scope = "Rich target-V1 authority semantics over opaque identity carriers and extensional finite sets." residual_assumptions = ["Lean's kernel, the pinned toolchain, the listed foundational axioms, and the theorem premises are trusted."] toolchain_lock_sha256 = "0c45a8a08ac06e313d775e669749097bd3a0abfb8e3395c69416ba0238770d53" @@ -5482,7 +5482,7 @@ semantic_source_closure = [ "formal/qualification/aeneas/generated/model/FunsExternal.lean", "formal/qualification/aeneas/generated/model/Types.lean", ] -semantic_source_closure_sha256 = "1a9d3309c0f56c88f64aa0d60d4048d93f6ae0da6336af00d09f342294e9b249" +semantic_source_closure_sha256 = "a625715ca60dcf7c1c9f14b063fd20152a36e46b82c5a8494273c45049cea638" scope = "Rich target-V1 authority semantics over opaque identity carriers and extensional finite sets." residual_assumptions = ["Lean's kernel, the pinned toolchain, the listed foundational axioms, and the theorem premises are trusted."] toolchain_lock_sha256 = "0c45a8a08ac06e313d775e669749097bd3a0abfb8e3395c69416ba0238770d53" @@ -5551,7 +5551,7 @@ semantic_source_closure = [ "formal/qualification/aeneas/generated/model/FunsExternal.lean", "formal/qualification/aeneas/generated/model/Types.lean", ] -semantic_source_closure_sha256 = "1a9d3309c0f56c88f64aa0d60d4048d93f6ae0da6336af00d09f342294e9b249" +semantic_source_closure_sha256 = "a625715ca60dcf7c1c9f14b063fd20152a36e46b82c5a8494273c45049cea638" scope = "Rich target-V1 authority semantics over opaque identity carriers and extensional finite sets." residual_assumptions = ["Lean's kernel, the pinned toolchain, the listed foundational axioms, and the theorem premises are trusted."] toolchain_lock_sha256 = "0c45a8a08ac06e313d775e669749097bd3a0abfb8e3395c69416ba0238770d53" @@ -5620,7 +5620,7 @@ semantic_source_closure = [ "formal/qualification/aeneas/generated/model/FunsExternal.lean", "formal/qualification/aeneas/generated/model/Types.lean", ] -semantic_source_closure_sha256 = "1a9d3309c0f56c88f64aa0d60d4048d93f6ae0da6336af00d09f342294e9b249" +semantic_source_closure_sha256 = "a625715ca60dcf7c1c9f14b063fd20152a36e46b82c5a8494273c45049cea638" scope = "Rich target-V1 authority semantics over opaque identity carriers and extensional finite sets." residual_assumptions = ["Lean's kernel, the pinned toolchain, the listed foundational axioms, and the theorem premises are trusted."] toolchain_lock_sha256 = "0c45a8a08ac06e313d775e669749097bd3a0abfb8e3395c69416ba0238770d53" @@ -5689,7 +5689,7 @@ semantic_source_closure = [ "formal/qualification/aeneas/generated/model/FunsExternal.lean", "formal/qualification/aeneas/generated/model/Types.lean", ] -semantic_source_closure_sha256 = "1a9d3309c0f56c88f64aa0d60d4048d93f6ae0da6336af00d09f342294e9b249" +semantic_source_closure_sha256 = "a625715ca60dcf7c1c9f14b063fd20152a36e46b82c5a8494273c45049cea638" scope = "Rich target-V1 authority semantics over opaque identity carriers and extensional finite sets." residual_assumptions = ["Lean's kernel, the pinned toolchain, the listed foundational axioms, and the theorem premises are trusted."] toolchain_lock_sha256 = "0c45a8a08ac06e313d775e669749097bd3a0abfb8e3395c69416ba0238770d53" @@ -5757,7 +5757,7 @@ semantic_source_closure = [ "formal/qualification/aeneas/generated/model/FunsExternal.lean", "formal/qualification/aeneas/generated/model/Types.lean", ] -semantic_source_closure_sha256 = "1a9d3309c0f56c88f64aa0d60d4048d93f6ae0da6336af00d09f342294e9b249" +semantic_source_closure_sha256 = "a625715ca60dcf7c1c9f14b063fd20152a36e46b82c5a8494273c45049cea638" scope = "Rich target-V1 authority semantics over opaque identity carriers and extensional finite sets." residual_assumptions = ["Lean's kernel, the pinned toolchain, the listed foundational axioms, and the theorem premises are trusted."] toolchain_lock_sha256 = "0c45a8a08ac06e313d775e669749097bd3a0abfb8e3395c69416ba0238770d53" @@ -5825,7 +5825,7 @@ semantic_source_closure = [ "formal/qualification/aeneas/generated/model/FunsExternal.lean", "formal/qualification/aeneas/generated/model/Types.lean", ] -semantic_source_closure_sha256 = "1a9d3309c0f56c88f64aa0d60d4048d93f6ae0da6336af00d09f342294e9b249" +semantic_source_closure_sha256 = "a625715ca60dcf7c1c9f14b063fd20152a36e46b82c5a8494273c45049cea638" scope = "Rich target-V1 authority semantics over opaque identity carriers and extensional finite sets." residual_assumptions = ["Lean's kernel, the pinned toolchain, the listed foundational axioms, and the theorem premises are trusted."] toolchain_lock_sha256 = "0c45a8a08ac06e313d775e669749097bd3a0abfb8e3395c69416ba0238770d53" @@ -5893,7 +5893,7 @@ semantic_source_closure = [ "formal/qualification/aeneas/generated/model/FunsExternal.lean", "formal/qualification/aeneas/generated/model/Types.lean", ] -semantic_source_closure_sha256 = "1a9d3309c0f56c88f64aa0d60d4048d93f6ae0da6336af00d09f342294e9b249" +semantic_source_closure_sha256 = "a625715ca60dcf7c1c9f14b063fd20152a36e46b82c5a8494273c45049cea638" scope = "Rich target-V1 authority semantics over opaque identity carriers and extensional finite sets." residual_assumptions = ["Lean's kernel, the pinned toolchain, the listed foundational axioms, and the theorem premises are trusted."] toolchain_lock_sha256 = "0c45a8a08ac06e313d775e669749097bd3a0abfb8e3395c69416ba0238770d53" @@ -5962,7 +5962,7 @@ semantic_source_closure = [ "formal/qualification/aeneas/generated/model/FunsExternal.lean", "formal/qualification/aeneas/generated/model/Types.lean", ] -semantic_source_closure_sha256 = "1a9d3309c0f56c88f64aa0d60d4048d93f6ae0da6336af00d09f342294e9b249" +semantic_source_closure_sha256 = "a625715ca60dcf7c1c9f14b063fd20152a36e46b82c5a8494273c45049cea638" scope = "Rich target-V1 authority semantics over opaque identity carriers and extensional finite sets." residual_assumptions = ["Lean's kernel, the pinned toolchain, the listed foundational axioms, and the theorem premises are trusted."] toolchain_lock_sha256 = "0c45a8a08ac06e313d775e669749097bd3a0abfb8e3395c69416ba0238770d53" @@ -6030,7 +6030,7 @@ semantic_source_closure = [ "formal/qualification/aeneas/generated/model/FunsExternal.lean", "formal/qualification/aeneas/generated/model/Types.lean", ] -semantic_source_closure_sha256 = "1a9d3309c0f56c88f64aa0d60d4048d93f6ae0da6336af00d09f342294e9b249" +semantic_source_closure_sha256 = "a625715ca60dcf7c1c9f14b063fd20152a36e46b82c5a8494273c45049cea638" scope = "Rich target-V1 authority semantics over opaque identity carriers and extensional finite sets." residual_assumptions = ["Lean's kernel, the pinned toolchain, the listed foundational axioms, and the theorem premises are trusted."] toolchain_lock_sha256 = "0c45a8a08ac06e313d775e669749097bd3a0abfb8e3395c69416ba0238770d53" @@ -6099,7 +6099,7 @@ semantic_source_closure = [ "formal/qualification/aeneas/generated/model/FunsExternal.lean", "formal/qualification/aeneas/generated/model/Types.lean", ] -semantic_source_closure_sha256 = "1a9d3309c0f56c88f64aa0d60d4048d93f6ae0da6336af00d09f342294e9b249" +semantic_source_closure_sha256 = "a625715ca60dcf7c1c9f14b063fd20152a36e46b82c5a8494273c45049cea638" scope = "Rich target-V1 authority semantics over opaque identity carriers and extensional finite sets." residual_assumptions = ["Lean's kernel, the pinned toolchain, the listed foundational axioms, and the theorem premises are trusted."] toolchain_lock_sha256 = "0c45a8a08ac06e313d775e669749097bd3a0abfb8e3395c69416ba0238770d53" @@ -6168,7 +6168,7 @@ semantic_source_closure = [ "formal/qualification/aeneas/generated/model/FunsExternal.lean", "formal/qualification/aeneas/generated/model/Types.lean", ] -semantic_source_closure_sha256 = "1a9d3309c0f56c88f64aa0d60d4048d93f6ae0da6336af00d09f342294e9b249" +semantic_source_closure_sha256 = "a625715ca60dcf7c1c9f14b063fd20152a36e46b82c5a8494273c45049cea638" scope = "Rich target-V1 authority semantics over opaque identity carriers and extensional finite sets." residual_assumptions = ["Lean's kernel, the pinned toolchain, the listed foundational axioms, and the theorem premises are trusted."] toolchain_lock_sha256 = "0c45a8a08ac06e313d775e669749097bd3a0abfb8e3395c69416ba0238770d53" @@ -6237,7 +6237,7 @@ semantic_source_closure = [ "formal/qualification/aeneas/generated/model/FunsExternal.lean", "formal/qualification/aeneas/generated/model/Types.lean", ] -semantic_source_closure_sha256 = "1a9d3309c0f56c88f64aa0d60d4048d93f6ae0da6336af00d09f342294e9b249" +semantic_source_closure_sha256 = "a625715ca60dcf7c1c9f14b063fd20152a36e46b82c5a8494273c45049cea638" scope = "Rich target-V1 authority semantics over opaque identity carriers and extensional finite sets." residual_assumptions = ["Lean's kernel, the pinned toolchain, the listed foundational axioms, and the theorem premises are trusted."] toolchain_lock_sha256 = "0c45a8a08ac06e313d775e669749097bd3a0abfb8e3395c69416ba0238770d53" @@ -6306,7 +6306,7 @@ semantic_source_closure = [ "formal/qualification/aeneas/generated/model/FunsExternal.lean", "formal/qualification/aeneas/generated/model/Types.lean", ] -semantic_source_closure_sha256 = "1a9d3309c0f56c88f64aa0d60d4048d93f6ae0da6336af00d09f342294e9b249" +semantic_source_closure_sha256 = "a625715ca60dcf7c1c9f14b063fd20152a36e46b82c5a8494273c45049cea638" scope = "Rich target-V1 authority semantics over opaque identity carriers and extensional finite sets." residual_assumptions = ["Lean's kernel, the pinned toolchain, the listed foundational axioms, and the theorem premises are trusted."] toolchain_lock_sha256 = "0c45a8a08ac06e313d775e669749097bd3a0abfb8e3395c69416ba0238770d53" @@ -6375,7 +6375,7 @@ semantic_source_closure = [ "formal/qualification/aeneas/generated/model/FunsExternal.lean", "formal/qualification/aeneas/generated/model/Types.lean", ] -semantic_source_closure_sha256 = "1a9d3309c0f56c88f64aa0d60d4048d93f6ae0da6336af00d09f342294e9b249" +semantic_source_closure_sha256 = "a625715ca60dcf7c1c9f14b063fd20152a36e46b82c5a8494273c45049cea638" scope = "Rich target-V1 authority semantics over opaque identity carriers and extensional finite sets." residual_assumptions = ["Lean's kernel, the pinned toolchain, the listed foundational axioms, and the theorem premises are trusted."] toolchain_lock_sha256 = "0c45a8a08ac06e313d775e669749097bd3a0abfb8e3395c69416ba0238770d53" @@ -6443,7 +6443,7 @@ semantic_source_closure = [ "formal/qualification/aeneas/generated/model/FunsExternal.lean", "formal/qualification/aeneas/generated/model/Types.lean", ] -semantic_source_closure_sha256 = "1a9d3309c0f56c88f64aa0d60d4048d93f6ae0da6336af00d09f342294e9b249" +semantic_source_closure_sha256 = "a625715ca60dcf7c1c9f14b063fd20152a36e46b82c5a8494273c45049cea638" scope = "Rich target-V1 authority semantics over opaque identity carriers and extensional finite sets." residual_assumptions = ["Lean's kernel, the pinned toolchain, the listed foundational axioms, and the theorem premises are trusted."] toolchain_lock_sha256 = "0c45a8a08ac06e313d775e669749097bd3a0abfb8e3395c69416ba0238770d53" @@ -6512,7 +6512,7 @@ semantic_source_closure = [ "formal/qualification/aeneas/generated/model/FunsExternal.lean", "formal/qualification/aeneas/generated/model/Types.lean", ] -semantic_source_closure_sha256 = "1a9d3309c0f56c88f64aa0d60d4048d93f6ae0da6336af00d09f342294e9b249" +semantic_source_closure_sha256 = "a625715ca60dcf7c1c9f14b063fd20152a36e46b82c5a8494273c45049cea638" scope = "Rich target-V1 authority semantics over opaque identity carriers and extensional finite sets." residual_assumptions = ["Lean's kernel, the pinned toolchain, the listed foundational axioms, and the theorem premises are trusted."] toolchain_lock_sha256 = "0c45a8a08ac06e313d775e669749097bd3a0abfb8e3395c69416ba0238770d53" @@ -6581,7 +6581,7 @@ semantic_source_closure = [ "formal/qualification/aeneas/generated/model/FunsExternal.lean", "formal/qualification/aeneas/generated/model/Types.lean", ] -semantic_source_closure_sha256 = "1a9d3309c0f56c88f64aa0d60d4048d93f6ae0da6336af00d09f342294e9b249" +semantic_source_closure_sha256 = "a625715ca60dcf7c1c9f14b063fd20152a36e46b82c5a8494273c45049cea638" scope = "Rich target-V1 authority semantics over opaque identity carriers and extensional finite sets." residual_assumptions = ["Lean's kernel, the pinned toolchain, the listed foundational axioms, and the theorem premises are trusted."] toolchain_lock_sha256 = "0c45a8a08ac06e313d775e669749097bd3a0abfb8e3395c69416ba0238770d53" @@ -6650,7 +6650,7 @@ semantic_source_closure = [ "formal/qualification/aeneas/generated/model/FunsExternal.lean", "formal/qualification/aeneas/generated/model/Types.lean", ] -semantic_source_closure_sha256 = "1a9d3309c0f56c88f64aa0d60d4048d93f6ae0da6336af00d09f342294e9b249" +semantic_source_closure_sha256 = "a625715ca60dcf7c1c9f14b063fd20152a36e46b82c5a8494273c45049cea638" scope = "Rich target-V1 authority semantics over opaque identity carriers and extensional finite sets." residual_assumptions = ["Lean's kernel, the pinned toolchain, the listed foundational axioms, and the theorem premises are trusted."] toolchain_lock_sha256 = "0c45a8a08ac06e313d775e669749097bd3a0abfb8e3395c69416ba0238770d53" @@ -6719,7 +6719,7 @@ semantic_source_closure = [ "formal/qualification/aeneas/generated/model/FunsExternal.lean", "formal/qualification/aeneas/generated/model/Types.lean", ] -semantic_source_closure_sha256 = "1a9d3309c0f56c88f64aa0d60d4048d93f6ae0da6336af00d09f342294e9b249" +semantic_source_closure_sha256 = "a625715ca60dcf7c1c9f14b063fd20152a36e46b82c5a8494273c45049cea638" scope = "Rich target-V1 authority semantics over opaque identity carriers and extensional finite sets." residual_assumptions = ["Lean's kernel, the pinned toolchain, the listed foundational axioms, and the theorem premises are trusted."] toolchain_lock_sha256 = "0c45a8a08ac06e313d775e669749097bd3a0abfb8e3395c69416ba0238770d53" @@ -6788,7 +6788,7 @@ semantic_source_closure = [ "formal/qualification/aeneas/generated/model/FunsExternal.lean", "formal/qualification/aeneas/generated/model/Types.lean", ] -semantic_source_closure_sha256 = "1a9d3309c0f56c88f64aa0d60d4048d93f6ae0da6336af00d09f342294e9b249" +semantic_source_closure_sha256 = "a625715ca60dcf7c1c9f14b063fd20152a36e46b82c5a8494273c45049cea638" scope = "Rich target-V1 authority semantics over opaque identity carriers and extensional finite sets." residual_assumptions = ["Lean's kernel, the pinned toolchain, the listed foundational axioms, and the theorem premises are trusted."] toolchain_lock_sha256 = "0c45a8a08ac06e313d775e669749097bd3a0abfb8e3395c69416ba0238770d53" @@ -6853,7 +6853,7 @@ semantic_source_closure = [ "formal/qualification/aeneas/generated/model/FunsExternal.lean", "formal/qualification/aeneas/generated/model/Types.lean", ] -semantic_source_closure_sha256 = "1a9d3309c0f56c88f64aa0d60d4048d93f6ae0da6336af00d09f342294e9b249" +semantic_source_closure_sha256 = "a625715ca60dcf7c1c9f14b063fd20152a36e46b82c5a8494273c45049cea638" scope = "Rich target-V1 authority semantics over opaque identity carriers and extensional finite sets." residual_assumptions = ["Lean's kernel, the pinned toolchain, the listed foundational axioms, and the theorem premises are trusted."] toolchain_lock_sha256 = "0c45a8a08ac06e313d775e669749097bd3a0abfb8e3395c69416ba0238770d53" @@ -6922,7 +6922,7 @@ semantic_source_closure = [ "formal/qualification/aeneas/generated/model/FunsExternal.lean", "formal/qualification/aeneas/generated/model/Types.lean", ] -semantic_source_closure_sha256 = "1a9d3309c0f56c88f64aa0d60d4048d93f6ae0da6336af00d09f342294e9b249" +semantic_source_closure_sha256 = "a625715ca60dcf7c1c9f14b063fd20152a36e46b82c5a8494273c45049cea638" scope = "Rich target-V1 authority semantics over opaque identity carriers and extensional finite sets." residual_assumptions = ["Lean's kernel, the pinned toolchain, the listed foundational axioms, and the theorem premises are trusted."] toolchain_lock_sha256 = "0c45a8a08ac06e313d775e669749097bd3a0abfb8e3395c69416ba0238770d53" @@ -6991,7 +6991,7 @@ semantic_source_closure = [ "formal/qualification/aeneas/generated/model/FunsExternal.lean", "formal/qualification/aeneas/generated/model/Types.lean", ] -semantic_source_closure_sha256 = "1a9d3309c0f56c88f64aa0d60d4048d93f6ae0da6336af00d09f342294e9b249" +semantic_source_closure_sha256 = "a625715ca60dcf7c1c9f14b063fd20152a36e46b82c5a8494273c45049cea638" scope = "Rich target-V1 authority semantics over opaque identity carriers and extensional finite sets." residual_assumptions = ["Lean's kernel, the pinned toolchain, the listed foundational axioms, and the theorem premises are trusted."] toolchain_lock_sha256 = "0c45a8a08ac06e313d775e669749097bd3a0abfb8e3395c69416ba0238770d53" @@ -7060,7 +7060,7 @@ semantic_source_closure = [ "formal/qualification/aeneas/generated/model/FunsExternal.lean", "formal/qualification/aeneas/generated/model/Types.lean", ] -semantic_source_closure_sha256 = "1a9d3309c0f56c88f64aa0d60d4048d93f6ae0da6336af00d09f342294e9b249" +semantic_source_closure_sha256 = "a625715ca60dcf7c1c9f14b063fd20152a36e46b82c5a8494273c45049cea638" scope = "Rich target-V1 authority semantics over opaque identity carriers and extensional finite sets." residual_assumptions = ["Lean's kernel, the pinned toolchain, the listed foundational axioms, and the theorem premises are trusted."] toolchain_lock_sha256 = "0c45a8a08ac06e313d775e669749097bd3a0abfb8e3395c69416ba0238770d53" @@ -7147,7 +7147,7 @@ semantic_source_closure = [ "formal/qualification/aeneas/generated/model/FunsExternal.lean", "formal/qualification/aeneas/generated/model/Types.lean", ] -semantic_source_closure_sha256 = "1a9d3309c0f56c88f64aa0d60d4048d93f6ae0da6336af00d09f342294e9b249" +semantic_source_closure_sha256 = "a625715ca60dcf7c1c9f14b063fd20152a36e46b82c5a8494273c45049cea638" scope = "The exact translated pre-signing scope evaluator over validated bounded views, including all ten scope/depth dimensions and ordered diagnostics, for every set of critical-extension laws." residual_assumptions = [ "Lean's kernel, the pinned Rust/Charon/Aeneas/Lean toolchain, the reviewed transparent external bridges, the listed foundational axioms, and the theorem's explicit representation-validity premises are trusted.", @@ -7184,7 +7184,7 @@ sha256 = "2bb401ffca0136622cd79bb14a5a38852061649a06cc46100503870c22d300c7" [[claims.evidence]] kind = "source-closure" artifact = "formal/qualification/aeneas/source-closure.json" -sha256 = "047b34bfe6deab4196c24256f55987245376abc6ddf57a4de8df1212c73bfec9" +sha256 = "c9eeba1225594d6dba4da1f0fc803480c0384b9c39c27b5ad1257012dd9fe9d0" [[claims]] claim_id = "AP-FORMAL-RICH-055" @@ -7255,7 +7255,7 @@ semantic_source_closure = [ "formal/qualification/aeneas/generated/model/FunsExternal.lean", "formal/qualification/aeneas/generated/model/Types.lean", ] -semantic_source_closure_sha256 = "1a9d3309c0f56c88f64aa0d60d4048d93f6ae0da6336af00d09f342294e9b249" +semantic_source_closure_sha256 = "a625715ca60dcf7c1c9f14b063fd20152a36e46b82c5a8494273c45049cea638" scope = "The crate-private raw translated evaluator over validated authority/action views. The public EffectiveAuthority::authorizes boundary resolves budget expressibility from AcceptedRegistries and the exact action profile before calling it." residual_assumptions = [ "Lean's kernel, the pinned Rust/Charon/Aeneas/Lean toolchain, the reviewed transparent external bridges, the listed foundational axioms, and the theorem's explicit representation-validity premises are trusted.", @@ -7291,7 +7291,7 @@ sha256 = "2bb401ffca0136622cd79bb14a5a38852061649a06cc46100503870c22d300c7" [[claims.evidence]] kind = "source-closure" artifact = "formal/qualification/aeneas/source-closure.json" -sha256 = "047b34bfe6deab4196c24256f55987245376abc6ddf57a4de8df1212c73bfec9" +sha256 = "c9eeba1225594d6dba4da1f0fc803480c0384b9c39c27b5ad1257012dd9fe9d0" [[claims]] claim_id = "AP-FORMAL-RICH-056" @@ -7375,7 +7375,7 @@ semantic_source_closure = [ "formal/qualification/aeneas/generated/model/FunsExternal.lean", "formal/qualification/aeneas/generated/model/Types.lean", ] -semantic_source_closure_sha256 = "1a9d3309c0f56c88f64aa0d60d4048d93f6ae0da6336af00d09f342294e9b249" +semantic_source_closure_sha256 = "a625715ca60dcf7c1c9f14b063fd20152a36e46b82c5a8494273c45049cea638" scope = "The crate-private raw evaluator over validated parent/grant views, including root linkage, strict depth, every attenuation dimension, and the unique accepted transition, for every set of critical-extension laws." residual_assumptions = [ "Lean's kernel, the pinned Rust/Charon/Aeneas/Lean toolchain, the reviewed transparent external bridges, the listed foundational axioms, and the theorem's explicit representation-validity premises are trusted.", @@ -7412,7 +7412,7 @@ sha256 = "2bb401ffca0136622cd79bb14a5a38852061649a06cc46100503870c22d300c7" [[claims.evidence]] kind = "source-closure" artifact = "formal/qualification/aeneas/source-closure.json" -sha256 = "047b34bfe6deab4196c24256f55987245376abc6ddf57a4de8df1212c73bfec9" +sha256 = "c9eeba1225594d6dba4da1f0fc803480c0384b9c39c27b5ad1257012dd9fe9d0" [[claims]] claim_id = "AP-FORMAL-RICH-104" @@ -7468,7 +7468,7 @@ semantic_source_closure = [ "formal/qualification/aeneas/generated/model/FunsExternal.lean", "formal/qualification/aeneas/generated/model/Types.lean", ] -semantic_source_closure_sha256 = "1a9d3309c0f56c88f64aa0d60d4048d93f6ae0da6336af00d09f342294e9b249" +semantic_source_closure_sha256 = "a625715ca60dcf7c1c9f14b063fd20152a36e46b82c5a8494273c45049cea638" scope = "Rich target-V1 authority semantics over opaque identity carriers and extensional finite sets." residual_assumptions = ["Lean's kernel, the pinned toolchain, the listed foundational axioms, and the theorem premises are trusted."] toolchain_lock_sha256 = "0c45a8a08ac06e313d775e669749097bd3a0abfb8e3395c69416ba0238770d53" @@ -7537,7 +7537,7 @@ semantic_source_closure = [ "formal/qualification/aeneas/generated/model/FunsExternal.lean", "formal/qualification/aeneas/generated/model/Types.lean", ] -semantic_source_closure_sha256 = "1a9d3309c0f56c88f64aa0d60d4048d93f6ae0da6336af00d09f342294e9b249" +semantic_source_closure_sha256 = "a625715ca60dcf7c1c9f14b063fd20152a36e46b82c5a8494273c45049cea638" scope = "Rich target-V1 authority semantics over opaque identity carriers and extensional finite sets." residual_assumptions = ["Lean's kernel, the pinned toolchain, the listed foundational axioms, and the theorem premises are trusted."] toolchain_lock_sha256 = "0c45a8a08ac06e313d775e669749097bd3a0abfb8e3395c69416ba0238770d53" @@ -7606,7 +7606,7 @@ semantic_source_closure = [ "formal/qualification/aeneas/generated/model/FunsExternal.lean", "formal/qualification/aeneas/generated/model/Types.lean", ] -semantic_source_closure_sha256 = "1a9d3309c0f56c88f64aa0d60d4048d93f6ae0da6336af00d09f342294e9b249" +semantic_source_closure_sha256 = "a625715ca60dcf7c1c9f14b063fd20152a36e46b82c5a8494273c45049cea638" scope = "Rich target-V1 authority semantics over opaque identity carriers and extensional finite sets." residual_assumptions = ["Lean's kernel, the pinned toolchain, the listed foundational axioms, and the theorem premises are trusted."] toolchain_lock_sha256 = "0c45a8a08ac06e313d775e669749097bd3a0abfb8e3395c69416ba0238770d53" @@ -7675,7 +7675,7 @@ semantic_source_closure = [ "formal/qualification/aeneas/generated/model/FunsExternal.lean", "formal/qualification/aeneas/generated/model/Types.lean", ] -semantic_source_closure_sha256 = "1a9d3309c0f56c88f64aa0d60d4048d93f6ae0da6336af00d09f342294e9b249" +semantic_source_closure_sha256 = "a625715ca60dcf7c1c9f14b063fd20152a36e46b82c5a8494273c45049cea638" scope = "Rich target-V1 authority semantics over opaque identity carriers and extensional finite sets." residual_assumptions = ["Lean's kernel, the pinned toolchain, the listed foundational axioms, and the theorem premises are trusted."] toolchain_lock_sha256 = "0c45a8a08ac06e313d775e669749097bd3a0abfb8e3395c69416ba0238770d53" @@ -7744,7 +7744,7 @@ semantic_source_closure = [ "formal/qualification/aeneas/generated/model/FunsExternal.lean", "formal/qualification/aeneas/generated/model/Types.lean", ] -semantic_source_closure_sha256 = "1a9d3309c0f56c88f64aa0d60d4048d93f6ae0da6336af00d09f342294e9b249" +semantic_source_closure_sha256 = "a625715ca60dcf7c1c9f14b063fd20152a36e46b82c5a8494273c45049cea638" scope = "Pure V1 bounded product-policy commitments, checked arithmetic, configuration gating, and eligibility." residual_assumptions = ["Lean's kernel, the pinned toolchain, the listed foundational axioms, and the theorem premises are trusted."] toolchain_lock_sha256 = "0c45a8a08ac06e313d775e669749097bd3a0abfb8e3395c69416ba0238770d53" @@ -7809,7 +7809,7 @@ semantic_source_closure = [ "formal/qualification/aeneas/generated/model/FunsExternal.lean", "formal/qualification/aeneas/generated/model/Types.lean", ] -semantic_source_closure_sha256 = "1a9d3309c0f56c88f64aa0d60d4048d93f6ae0da6336af00d09f342294e9b249" +semantic_source_closure_sha256 = "a625715ca60dcf7c1c9f14b063fd20152a36e46b82c5a8494273c45049cea638" scope = "Pure V1 bounded product-policy commitments, checked arithmetic, configuration gating, and eligibility." residual_assumptions = ["Lean's kernel, the pinned toolchain, the listed foundational axioms, and the theorem premises are trusted."] toolchain_lock_sha256 = "0c45a8a08ac06e313d775e669749097bd3a0abfb8e3395c69416ba0238770d53" @@ -7874,7 +7874,7 @@ semantic_source_closure = [ "formal/qualification/aeneas/generated/model/FunsExternal.lean", "formal/qualification/aeneas/generated/model/Types.lean", ] -semantic_source_closure_sha256 = "1a9d3309c0f56c88f64aa0d60d4048d93f6ae0da6336af00d09f342294e9b249" +semantic_source_closure_sha256 = "a625715ca60dcf7c1c9f14b063fd20152a36e46b82c5a8494273c45049cea638" scope = "Pure V1 bounded product-policy commitments, checked arithmetic, configuration gating, and eligibility." residual_assumptions = ["Lean's kernel, the pinned toolchain, the listed foundational axioms, and the theorem premises are trusted."] toolchain_lock_sha256 = "0c45a8a08ac06e313d775e669749097bd3a0abfb8e3395c69416ba0238770d53" @@ -7939,7 +7939,7 @@ semantic_source_closure = [ "formal/qualification/aeneas/generated/model/FunsExternal.lean", "formal/qualification/aeneas/generated/model/Types.lean", ] -semantic_source_closure_sha256 = "1a9d3309c0f56c88f64aa0d60d4048d93f6ae0da6336af00d09f342294e9b249" +semantic_source_closure_sha256 = "a625715ca60dcf7c1c9f14b063fd20152a36e46b82c5a8494273c45049cea638" scope = "Pure V1 bounded product-policy commitments, checked arithmetic, configuration gating, and eligibility." residual_assumptions = ["Lean's kernel, the pinned toolchain, the listed foundational axioms, and the theorem premises are trusted."] toolchain_lock_sha256 = "0c45a8a08ac06e313d775e669749097bd3a0abfb8e3395c69416ba0238770d53" @@ -8004,7 +8004,7 @@ semantic_source_closure = [ "formal/qualification/aeneas/generated/model/FunsExternal.lean", "formal/qualification/aeneas/generated/model/Types.lean", ] -semantic_source_closure_sha256 = "1a9d3309c0f56c88f64aa0d60d4048d93f6ae0da6336af00d09f342294e9b249" +semantic_source_closure_sha256 = "a625715ca60dcf7c1c9f14b063fd20152a36e46b82c5a8494273c45049cea638" scope = "Pure V1 bounded product-policy commitments, checked arithmetic, configuration gating, and eligibility." residual_assumptions = ["Lean's kernel, the pinned toolchain, the listed foundational axioms, and the theorem premises are trusted."] toolchain_lock_sha256 = "0c45a8a08ac06e313d775e669749097bd3a0abfb8e3395c69416ba0238770d53" @@ -8069,7 +8069,7 @@ semantic_source_closure = [ "formal/qualification/aeneas/generated/model/FunsExternal.lean", "formal/qualification/aeneas/generated/model/Types.lean", ] -semantic_source_closure_sha256 = "1a9d3309c0f56c88f64aa0d60d4048d93f6ae0da6336af00d09f342294e9b249" +semantic_source_closure_sha256 = "a625715ca60dcf7c1c9f14b063fd20152a36e46b82c5a8494273c45049cea638" scope = "Pure V1 bounded product-policy commitments, checked arithmetic, configuration gating, and eligibility." residual_assumptions = ["Lean's kernel, the pinned toolchain, the listed foundational axioms, and the theorem premises are trusted."] toolchain_lock_sha256 = "0c45a8a08ac06e313d775e669749097bd3a0abfb8e3395c69416ba0238770d53" @@ -8134,7 +8134,7 @@ semantic_source_closure = [ "formal/qualification/aeneas/generated/model/FunsExternal.lean", "formal/qualification/aeneas/generated/model/Types.lean", ] -semantic_source_closure_sha256 = "1a9d3309c0f56c88f64aa0d60d4048d93f6ae0da6336af00d09f342294e9b249" +semantic_source_closure_sha256 = "a625715ca60dcf7c1c9f14b063fd20152a36e46b82c5a8494273c45049cea638" scope = "Pure V1 bounded product-policy commitments, checked arithmetic, configuration gating, and eligibility." residual_assumptions = ["Lean's kernel, the pinned toolchain, the listed foundational axioms, and the theorem premises are trusted."] toolchain_lock_sha256 = "0c45a8a08ac06e313d775e669749097bd3a0abfb8e3395c69416ba0238770d53" @@ -8199,7 +8199,7 @@ semantic_source_closure = [ "formal/qualification/aeneas/generated/model/FunsExternal.lean", "formal/qualification/aeneas/generated/model/Types.lean", ] -semantic_source_closure_sha256 = "1a9d3309c0f56c88f64aa0d60d4048d93f6ae0da6336af00d09f342294e9b249" +semantic_source_closure_sha256 = "a625715ca60dcf7c1c9f14b063fd20152a36e46b82c5a8494273c45049cea638" scope = "Pure V1 bounded product-policy commitments, checked arithmetic, configuration gating, and eligibility." residual_assumptions = ["Lean's kernel, the pinned toolchain, the listed foundational axioms, and the theorem premises are trusted."] toolchain_lock_sha256 = "0c45a8a08ac06e313d775e669749097bd3a0abfb8e3395c69416ba0238770d53" @@ -8267,7 +8267,7 @@ semantic_source_closure = [ "formal/qualification/aeneas/generated/model/FunsExternal.lean", "formal/qualification/aeneas/generated/model/Types.lean", ] -semantic_source_closure_sha256 = "1a9d3309c0f56c88f64aa0d60d4048d93f6ae0da6336af00d09f342294e9b249" +semantic_source_closure_sha256 = "a625715ca60dcf7c1c9f14b063fd20152a36e46b82c5a8494273c45049cea638" scope = "Pure V1 bounded product-policy commitments, checked arithmetic, configuration gating, and eligibility." residual_assumptions = ["Lean's kernel, the pinned toolchain, the listed foundational axioms, and the theorem premises are trusted."] toolchain_lock_sha256 = "0c45a8a08ac06e313d775e669749097bd3a0abfb8e3395c69416ba0238770d53" @@ -8332,7 +8332,7 @@ semantic_source_closure = [ "formal/qualification/aeneas/generated/model/FunsExternal.lean", "formal/qualification/aeneas/generated/model/Types.lean", ] -semantic_source_closure_sha256 = "1a9d3309c0f56c88f64aa0d60d4048d93f6ae0da6336af00d09f342294e9b249" +semantic_source_closure_sha256 = "a625715ca60dcf7c1c9f14b063fd20152a36e46b82c5a8494273c45049cea638" scope = "Pure V1 bounded product-policy commitments, checked arithmetic, configuration gating, and eligibility." residual_assumptions = ["Lean's kernel, the pinned toolchain, the listed foundational axioms, and the theorem premises are trusted."] toolchain_lock_sha256 = "0c45a8a08ac06e313d775e669749097bd3a0abfb8e3395c69416ba0238770d53" @@ -8401,7 +8401,7 @@ semantic_source_closure = [ "formal/qualification/aeneas/generated/model/FunsExternal.lean", "formal/qualification/aeneas/generated/model/Types.lean", ] -semantic_source_closure_sha256 = "1a9d3309c0f56c88f64aa0d60d4048d93f6ae0da6336af00d09f342294e9b249" +semantic_source_closure_sha256 = "a625715ca60dcf7c1c9f14b063fd20152a36e46b82c5a8494273c45049cea638" scope = "Pure V1 bounded product-policy commitments, checked arithmetic, configuration gating, and eligibility." residual_assumptions = ["Lean's kernel, the pinned toolchain, the listed foundational axioms, and the theorem premises are trusted."] toolchain_lock_sha256 = "0c45a8a08ac06e313d775e669749097bd3a0abfb8e3395c69416ba0238770d53" @@ -8470,7 +8470,7 @@ semantic_source_closure = [ "formal/qualification/aeneas/generated/model/FunsExternal.lean", "formal/qualification/aeneas/generated/model/Types.lean", ] -semantic_source_closure_sha256 = "1a9d3309c0f56c88f64aa0d60d4048d93f6ae0da6336af00d09f342294e9b249" +semantic_source_closure_sha256 = "a625715ca60dcf7c1c9f14b063fd20152a36e46b82c5a8494273c45049cea638" scope = "Pure V1 bounded product-policy commitments, checked arithmetic, configuration gating, and eligibility." residual_assumptions = ["Lean's kernel, the pinned toolchain, the listed foundational axioms, and the theorem premises are trusted."] toolchain_lock_sha256 = "0c45a8a08ac06e313d775e669749097bd3a0abfb8e3395c69416ba0238770d53" @@ -8539,7 +8539,7 @@ semantic_source_closure = [ "formal/qualification/aeneas/generated/model/FunsExternal.lean", "formal/qualification/aeneas/generated/model/Types.lean", ] -semantic_source_closure_sha256 = "1a9d3309c0f56c88f64aa0d60d4048d93f6ae0da6336af00d09f342294e9b249" +semantic_source_closure_sha256 = "a625715ca60dcf7c1c9f14b063fd20152a36e46b82c5a8494273c45049cea638" scope = "Pure V1 bounded product-policy commitments, checked arithmetic, configuration gating, and eligibility." residual_assumptions = ["Lean's kernel, the pinned toolchain, the listed foundational axioms, and the theorem premises are trusted."] toolchain_lock_sha256 = "0c45a8a08ac06e313d775e669749097bd3a0abfb8e3395c69416ba0238770d53" @@ -8608,7 +8608,7 @@ semantic_source_closure = [ "formal/qualification/aeneas/generated/model/FunsExternal.lean", "formal/qualification/aeneas/generated/model/Types.lean", ] -semantic_source_closure_sha256 = "1a9d3309c0f56c88f64aa0d60d4048d93f6ae0da6336af00d09f342294e9b249" +semantic_source_closure_sha256 = "a625715ca60dcf7c1c9f14b063fd20152a36e46b82c5a8494273c45049cea638" scope = "The Aeneas-translated argument-ceiling window-count leaves of auths-bounded-policy, under the pinned translation." residual_assumptions = ["Lean's kernel, the pinned toolchain, the listed foundational axioms, and the theorem premises are trusted."] toolchain_lock_sha256 = "0c45a8a08ac06e313d775e669749097bd3a0abfb8e3395c69416ba0238770d53" @@ -8676,7 +8676,7 @@ semantic_source_closure = [ "formal/qualification/aeneas/generated/model/FunsExternal.lean", "formal/qualification/aeneas/generated/model/Types.lean", ] -semantic_source_closure_sha256 = "1a9d3309c0f56c88f64aa0d60d4048d93f6ae0da6336af00d09f342294e9b249" +semantic_source_closure_sha256 = "a625715ca60dcf7c1c9f14b063fd20152a36e46b82c5a8494273c45049cea638" scope = "The Aeneas-translated argument-ceiling window-count leaves of auths-bounded-policy, under the pinned translation." residual_assumptions = ["Lean's kernel, the pinned toolchain, the listed foundational axioms, and the theorem premises are trusted."] toolchain_lock_sha256 = "0c45a8a08ac06e313d775e669749097bd3a0abfb8e3395c69416ba0238770d53" @@ -8744,7 +8744,7 @@ semantic_source_closure = [ "formal/qualification/aeneas/generated/model/FunsExternal.lean", "formal/qualification/aeneas/generated/model/Types.lean", ] -semantic_source_closure_sha256 = "1a9d3309c0f56c88f64aa0d60d4048d93f6ae0da6336af00d09f342294e9b249" +semantic_source_closure_sha256 = "a625715ca60dcf7c1c9f14b063fd20152a36e46b82c5a8494273c45049cea638" scope = "The gateway's registered argument-ceiling window-count evaluator: fixed-context evaluation over verified unsigned arguments and per-window counts, semantic tightening, and the registered tightening decider." residual_assumptions = ["Lean's kernel, the pinned toolchain, the listed foundational axioms, and the theorem premises are trusted."] toolchain_lock_sha256 = "0c45a8a08ac06e313d775e669749097bd3a0abfb8e3395c69416ba0238770d53" @@ -8809,7 +8809,7 @@ semantic_source_closure = [ "formal/qualification/aeneas/generated/model/FunsExternal.lean", "formal/qualification/aeneas/generated/model/Types.lean", ] -semantic_source_closure_sha256 = "1a9d3309c0f56c88f64aa0d60d4048d93f6ae0da6336af00d09f342294e9b249" +semantic_source_closure_sha256 = "a625715ca60dcf7c1c9f14b063fd20152a36e46b82c5a8494273c45049cea638" scope = "The gateway's registered argument-ceiling window-count evaluator: fixed-context evaluation over verified unsigned arguments and per-window counts, semantic tightening, and the registered tightening decider." residual_assumptions = ["Lean's kernel, the pinned toolchain, the listed foundational axioms, and the theorem premises are trusted."] toolchain_lock_sha256 = "0c45a8a08ac06e313d775e669749097bd3a0abfb8e3395c69416ba0238770d53" @@ -8874,7 +8874,7 @@ semantic_source_closure = [ "formal/qualification/aeneas/generated/model/FunsExternal.lean", "formal/qualification/aeneas/generated/model/Types.lean", ] -semantic_source_closure_sha256 = "1a9d3309c0f56c88f64aa0d60d4048d93f6ae0da6336af00d09f342294e9b249" +semantic_source_closure_sha256 = "a625715ca60dcf7c1c9f14b063fd20152a36e46b82c5a8494273c45049cea638" scope = "The gateway's registered argument-ceiling window-count evaluator: fixed-context evaluation over verified unsigned arguments and per-window counts, semantic tightening, and the registered tightening decider." residual_assumptions = ["Lean's kernel, the pinned toolchain, the listed foundational axioms, and the theorem premises are trusted."] toolchain_lock_sha256 = "0c45a8a08ac06e313d775e669749097bd3a0abfb8e3395c69416ba0238770d53" @@ -8943,7 +8943,7 @@ semantic_source_closure = [ "formal/qualification/aeneas/generated/model/FunsExternal.lean", "formal/qualification/aeneas/generated/model/Types.lean", ] -semantic_source_closure_sha256 = "1a9d3309c0f56c88f64aa0d60d4048d93f6ae0da6336af00d09f342294e9b249" +semantic_source_closure_sha256 = "a625715ca60dcf7c1c9f14b063fd20152a36e46b82c5a8494273c45049cea638" scope = "The gateway's registered argument-ceiling window-count evaluator: fixed-context evaluation over verified unsigned arguments and per-window counts, semantic tightening, and the registered tightening decider." residual_assumptions = ["Lean's kernel, the pinned toolchain, the listed foundational axioms, and the theorem premises are trusted."] toolchain_lock_sha256 = "0c45a8a08ac06e313d775e669749097bd3a0abfb8e3395c69416ba0238770d53" @@ -9012,7 +9012,7 @@ semantic_source_closure = [ "formal/qualification/aeneas/generated/model/FunsExternal.lean", "formal/qualification/aeneas/generated/model/Types.lean", ] -semantic_source_closure_sha256 = "1a9d3309c0f56c88f64aa0d60d4048d93f6ae0da6336af00d09f342294e9b249" +semantic_source_closure_sha256 = "a625715ca60dcf7c1c9f14b063fd20152a36e46b82c5a8494273c45049cea638" scope = "The gateway's registered argument-ceiling window-count evaluator: fixed-context evaluation over verified unsigned arguments and per-window counts, semantic tightening, and the registered tightening decider." residual_assumptions = ["Lean's kernel, the pinned toolchain, the listed foundational axioms, and the theorem premises are trusted."] toolchain_lock_sha256 = "0c45a8a08ac06e313d775e669749097bd3a0abfb8e3395c69416ba0238770d53" @@ -9081,7 +9081,7 @@ semantic_source_closure = [ "formal/qualification/aeneas/generated/model/FunsExternal.lean", "formal/qualification/aeneas/generated/model/Types.lean", ] -semantic_source_closure_sha256 = "1a9d3309c0f56c88f64aa0d60d4048d93f6ae0da6336af00d09f342294e9b249" +semantic_source_closure_sha256 = "a625715ca60dcf7c1c9f14b063fd20152a36e46b82c5a8494273c45049cea638" scope = "The gateway's registered argument-ceiling window-count evaluator: fixed-context evaluation over verified unsigned arguments and per-window counts, semantic tightening, and the registered tightening decider." residual_assumptions = ["Lean's kernel, the pinned toolchain, the listed foundational axioms, and the theorem premises are trusted."] toolchain_lock_sha256 = "0c45a8a08ac06e313d775e669749097bd3a0abfb8e3395c69416ba0238770d53" @@ -9150,7 +9150,7 @@ semantic_source_closure = [ "formal/qualification/aeneas/generated/model/FunsExternal.lean", "formal/qualification/aeneas/generated/model/Types.lean", ] -semantic_source_closure_sha256 = "1a9d3309c0f56c88f64aa0d60d4048d93f6ae0da6336af00d09f342294e9b249" +semantic_source_closure_sha256 = "a625715ca60dcf7c1c9f14b063fd20152a36e46b82c5a8494273c45049cea638" scope = "The gateway's registered argument-ceiling window-count evaluator: fixed-context evaluation over verified unsigned arguments and per-window counts, semantic tightening, and the registered tightening decider." residual_assumptions = ["Lean's kernel, the pinned toolchain, the listed foundational axioms, and the theorem premises are trusted."] toolchain_lock_sha256 = "0c45a8a08ac06e313d775e669749097bd3a0abfb8e3395c69416ba0238770d53" @@ -9215,7 +9215,7 @@ semantic_source_closure = [ "formal/qualification/aeneas/generated/model/FunsExternal.lean", "formal/qualification/aeneas/generated/model/Types.lean", ] -semantic_source_closure_sha256 = "1a9d3309c0f56c88f64aa0d60d4048d93f6ae0da6336af00d09f342294e9b249" +semantic_source_closure_sha256 = "a625715ca60dcf7c1c9f14b063fd20152a36e46b82c5a8494273c45049cea638" scope = "The gateway's registered argument-ceiling window-count evaluator: fixed-context evaluation over verified unsigned arguments and per-window counts, semantic tightening, and the registered tightening decider." residual_assumptions = ["Lean's kernel, the pinned toolchain, the listed foundational axioms, and the theorem premises are trusted."] toolchain_lock_sha256 = "0c45a8a08ac06e313d775e669749097bd3a0abfb8e3395c69416ba0238770d53" @@ -9280,7 +9280,7 @@ semantic_source_closure = [ "formal/qualification/aeneas/generated/model/FunsExternal.lean", "formal/qualification/aeneas/generated/model/Types.lean", ] -semantic_source_closure_sha256 = "1a9d3309c0f56c88f64aa0d60d4048d93f6ae0da6336af00d09f342294e9b249" +semantic_source_closure_sha256 = "a625715ca60dcf7c1c9f14b063fd20152a36e46b82c5a8494273c45049cea638" scope = "Product-layer premise of the bounded-policy-commitment-v1 extension. The kernel checks only that a delegated commitment links the digest of its parent's extension bytes; narrowing is discharged here by the registered evaluator's tightening decider, which the gateway runs on every linked pair before eligibility. This is not a kernel theorem." residual_assumptions = [ "Lean's kernel, the pinned toolchain, the listed foundational axioms, and the theorem premises are trusted.", @@ -9352,7 +9352,7 @@ semantic_source_closure = [ "formal/qualification/aeneas/generated/model/FunsExternal.lean", "formal/qualification/aeneas/generated/model/Types.lean", ] -semantic_source_closure_sha256 = "1a9d3309c0f56c88f64aa0d60d4048d93f6ae0da6336af00d09f342294e9b249" +semantic_source_closure_sha256 = "a625715ca60dcf7c1c9f14b063fd20152a36e46b82c5a8494273c45049cea638" scope = "Product-layer premise of the bounded-policy-commitment-v1 extension. The kernel checks only that a delegated commitment links the digest of its parent's extension bytes; narrowing is discharged here by the registered evaluator's tightening decider, which the gateway runs on every linked pair before eligibility. This is not a kernel theorem." residual_assumptions = [ "Lean's kernel, the pinned toolchain, the listed foundational axioms, and the theorem premises are trusted.", @@ -9420,7 +9420,7 @@ semantic_source_closure = [ "formal/qualification/aeneas/generated/model/FunsExternal.lean", "formal/qualification/aeneas/generated/model/Types.lean", ] -semantic_source_closure_sha256 = "1a9d3309c0f56c88f64aa0d60d4048d93f6ae0da6336af00d09f342294e9b249" +semantic_source_closure_sha256 = "a625715ca60dcf7c1c9f14b063fd20152a36e46b82c5a8494273c45049cea638" scope = "The gateway's registered argument-ceiling window-count evaluator: fixed-context evaluation over verified unsigned arguments and per-window counts, semantic tightening, and the registered tightening decider." residual_assumptions = ["Lean's kernel, the pinned toolchain, the listed foundational axioms, and the theorem premises are trusted."] toolchain_lock_sha256 = "0c45a8a08ac06e313d775e669749097bd3a0abfb8e3395c69416ba0238770d53" @@ -9489,7 +9489,7 @@ semantic_source_closure = [ "formal/qualification/aeneas/generated/model/FunsExternal.lean", "formal/qualification/aeneas/generated/model/Types.lean", ] -semantic_source_closure_sha256 = "1a9d3309c0f56c88f64aa0d60d4048d93f6ae0da6336af00d09f342294e9b249" +semantic_source_closure_sha256 = "a625715ca60dcf7c1c9f14b063fd20152a36e46b82c5a8494273c45049cea638" scope = "Pure V1 lifecycle transitions, capacity conservation, replay, configuration gates, credential ordering, provider entry, and reconciliation." residual_assumptions = ["Lean's kernel, the pinned toolchain, the listed foundational axioms, and the theorem premises are trusted."] toolchain_lock_sha256 = "0c45a8a08ac06e313d775e669749097bd3a0abfb8e3395c69416ba0238770d53" @@ -9558,7 +9558,7 @@ semantic_source_closure = [ "formal/qualification/aeneas/generated/model/FunsExternal.lean", "formal/qualification/aeneas/generated/model/Types.lean", ] -semantic_source_closure_sha256 = "1a9d3309c0f56c88f64aa0d60d4048d93f6ae0da6336af00d09f342294e9b249" +semantic_source_closure_sha256 = "a625715ca60dcf7c1c9f14b063fd20152a36e46b82c5a8494273c45049cea638" scope = "Pure V1 lifecycle transitions, capacity conservation, replay, configuration gates, credential ordering, provider entry, and reconciliation." residual_assumptions = ["Lean's kernel, the pinned toolchain, the listed foundational axioms, and the theorem premises are trusted."] toolchain_lock_sha256 = "0c45a8a08ac06e313d775e669749097bd3a0abfb8e3395c69416ba0238770d53" @@ -9626,7 +9626,7 @@ semantic_source_closure = [ "formal/qualification/aeneas/generated/model/FunsExternal.lean", "formal/qualification/aeneas/generated/model/Types.lean", ] -semantic_source_closure_sha256 = "1a9d3309c0f56c88f64aa0d60d4048d93f6ae0da6336af00d09f342294e9b249" +semantic_source_closure_sha256 = "a625715ca60dcf7c1c9f14b063fd20152a36e46b82c5a8494273c45049cea638" scope = "Pure V1 lifecycle transitions, capacity conservation, replay, configuration gates, credential ordering, provider entry, and reconciliation." residual_assumptions = ["Lean's kernel, the pinned toolchain, the listed foundational axioms, and the theorem premises are trusted."] toolchain_lock_sha256 = "0c45a8a08ac06e313d775e669749097bd3a0abfb8e3395c69416ba0238770d53" @@ -9694,7 +9694,7 @@ semantic_source_closure = [ "formal/qualification/aeneas/generated/model/FunsExternal.lean", "formal/qualification/aeneas/generated/model/Types.lean", ] -semantic_source_closure_sha256 = "1a9d3309c0f56c88f64aa0d60d4048d93f6ae0da6336af00d09f342294e9b249" +semantic_source_closure_sha256 = "a625715ca60dcf7c1c9f14b063fd20152a36e46b82c5a8494273c45049cea638" scope = "Pure V1 lifecycle transitions, capacity conservation, replay, configuration gates, credential ordering, provider entry, and reconciliation." residual_assumptions = ["Lean's kernel, the pinned toolchain, the listed foundational axioms, and the theorem premises are trusted."] toolchain_lock_sha256 = "0c45a8a08ac06e313d775e669749097bd3a0abfb8e3395c69416ba0238770d53" @@ -9762,7 +9762,7 @@ semantic_source_closure = [ "formal/qualification/aeneas/generated/model/FunsExternal.lean", "formal/qualification/aeneas/generated/model/Types.lean", ] -semantic_source_closure_sha256 = "1a9d3309c0f56c88f64aa0d60d4048d93f6ae0da6336af00d09f342294e9b249" +semantic_source_closure_sha256 = "a625715ca60dcf7c1c9f14b063fd20152a36e46b82c5a8494273c45049cea638" scope = "Pure V1 lifecycle transitions, capacity conservation, replay, configuration gates, credential ordering, provider entry, and reconciliation." residual_assumptions = ["Lean's kernel, the pinned toolchain, the listed foundational axioms, and the theorem premises are trusted."] toolchain_lock_sha256 = "0c45a8a08ac06e313d775e669749097bd3a0abfb8e3395c69416ba0238770d53" @@ -9831,7 +9831,7 @@ semantic_source_closure = [ "formal/qualification/aeneas/generated/model/FunsExternal.lean", "formal/qualification/aeneas/generated/model/Types.lean", ] -semantic_source_closure_sha256 = "1a9d3309c0f56c88f64aa0d60d4048d93f6ae0da6336af00d09f342294e9b249" +semantic_source_closure_sha256 = "a625715ca60dcf7c1c9f14b063fd20152a36e46b82c5a8494273c45049cea638" scope = "Pure V1 lifecycle transitions, capacity conservation, replay, configuration gates, credential ordering, provider entry, and reconciliation." residual_assumptions = ["Lean's kernel, the pinned toolchain, the listed foundational axioms, and the theorem premises are trusted."] toolchain_lock_sha256 = "0c45a8a08ac06e313d775e669749097bd3a0abfb8e3395c69416ba0238770d53" @@ -9900,7 +9900,7 @@ semantic_source_closure = [ "formal/qualification/aeneas/generated/model/FunsExternal.lean", "formal/qualification/aeneas/generated/model/Types.lean", ] -semantic_source_closure_sha256 = "1a9d3309c0f56c88f64aa0d60d4048d93f6ae0da6336af00d09f342294e9b249" +semantic_source_closure_sha256 = "a625715ca60dcf7c1c9f14b063fd20152a36e46b82c5a8494273c45049cea638" scope = "Pure V1 lifecycle transitions, capacity conservation, replay, configuration gates, credential ordering, provider entry, and reconciliation." residual_assumptions = ["Lean's kernel, the pinned toolchain, the listed foundational axioms, and the theorem premises are trusted."] toolchain_lock_sha256 = "0c45a8a08ac06e313d775e669749097bd3a0abfb8e3395c69416ba0238770d53" @@ -9965,7 +9965,7 @@ semantic_source_closure = [ "formal/qualification/aeneas/generated/model/FunsExternal.lean", "formal/qualification/aeneas/generated/model/Types.lean", ] -semantic_source_closure_sha256 = "1a9d3309c0f56c88f64aa0d60d4048d93f6ae0da6336af00d09f342294e9b249" +semantic_source_closure_sha256 = "a625715ca60dcf7c1c9f14b063fd20152a36e46b82c5a8494273c45049cea638" scope = "Pure V1 lifecycle transitions, capacity conservation, replay, configuration gates, credential ordering, provider entry, and reconciliation." residual_assumptions = ["Lean's kernel, the pinned toolchain, the listed foundational axioms, and the theorem premises are trusted."] toolchain_lock_sha256 = "0c45a8a08ac06e313d775e669749097bd3a0abfb8e3395c69416ba0238770d53" @@ -10030,7 +10030,7 @@ semantic_source_closure = [ "formal/qualification/aeneas/generated/model/FunsExternal.lean", "formal/qualification/aeneas/generated/model/Types.lean", ] -semantic_source_closure_sha256 = "1a9d3309c0f56c88f64aa0d60d4048d93f6ae0da6336af00d09f342294e9b249" +semantic_source_closure_sha256 = "a625715ca60dcf7c1c9f14b063fd20152a36e46b82c5a8494273c45049cea638" scope = "Pure V1 lifecycle transitions, capacity conservation, replay, configuration gates, credential ordering, provider entry, and reconciliation." residual_assumptions = ["Lean's kernel, the pinned toolchain, the listed foundational axioms, and the theorem premises are trusted."] toolchain_lock_sha256 = "0c45a8a08ac06e313d775e669749097bd3a0abfb8e3395c69416ba0238770d53" @@ -10095,7 +10095,7 @@ semantic_source_closure = [ "formal/qualification/aeneas/generated/model/FunsExternal.lean", "formal/qualification/aeneas/generated/model/Types.lean", ] -semantic_source_closure_sha256 = "1a9d3309c0f56c88f64aa0d60d4048d93f6ae0da6336af00d09f342294e9b249" +semantic_source_closure_sha256 = "a625715ca60dcf7c1c9f14b063fd20152a36e46b82c5a8494273c45049cea638" scope = "Pure V1 lifecycle transitions, capacity conservation, replay, configuration gates, credential ordering, provider entry, and reconciliation." residual_assumptions = ["Lean's kernel, the pinned toolchain, the listed foundational axioms, and the theorem premises are trusted."] toolchain_lock_sha256 = "0c45a8a08ac06e313d775e669749097bd3a0abfb8e3395c69416ba0238770d53" @@ -10160,7 +10160,7 @@ semantic_source_closure = [ "formal/qualification/aeneas/generated/model/FunsExternal.lean", "formal/qualification/aeneas/generated/model/Types.lean", ] -semantic_source_closure_sha256 = "1a9d3309c0f56c88f64aa0d60d4048d93f6ae0da6336af00d09f342294e9b249" +semantic_source_closure_sha256 = "a625715ca60dcf7c1c9f14b063fd20152a36e46b82c5a8494273c45049cea638" scope = "Pure V1 lifecycle transitions, capacity conservation, replay, configuration gates, credential ordering, provider entry, and reconciliation." residual_assumptions = ["Lean's kernel, the pinned toolchain, the listed foundational axioms, and the theorem premises are trusted."] toolchain_lock_sha256 = "0c45a8a08ac06e313d775e669749097bd3a0abfb8e3395c69416ba0238770d53" @@ -10225,7 +10225,7 @@ semantic_source_closure = [ "formal/qualification/aeneas/generated/model/FunsExternal.lean", "formal/qualification/aeneas/generated/model/Types.lean", ] -semantic_source_closure_sha256 = "1a9d3309c0f56c88f64aa0d60d4048d93f6ae0da6336af00d09f342294e9b249" +semantic_source_closure_sha256 = "a625715ca60dcf7c1c9f14b063fd20152a36e46b82c5a8494273c45049cea638" scope = "Pure V1 lifecycle transitions, capacity conservation, replay, configuration gates, credential ordering, provider entry, and reconciliation." residual_assumptions = ["Lean's kernel, the pinned toolchain, the listed foundational axioms, and the theorem premises are trusted."] toolchain_lock_sha256 = "0c45a8a08ac06e313d775e669749097bd3a0abfb8e3395c69416ba0238770d53" @@ -10290,7 +10290,7 @@ semantic_source_closure = [ "formal/qualification/aeneas/generated/model/FunsExternal.lean", "formal/qualification/aeneas/generated/model/Types.lean", ] -semantic_source_closure_sha256 = "1a9d3309c0f56c88f64aa0d60d4048d93f6ae0da6336af00d09f342294e9b249" +semantic_source_closure_sha256 = "a625715ca60dcf7c1c9f14b063fd20152a36e46b82c5a8494273c45049cea638" scope = "Pure V1 lifecycle transitions, capacity conservation, replay, configuration gates, credential ordering, provider entry, and reconciliation." residual_assumptions = ["Lean's kernel, the pinned toolchain, the listed foundational axioms, and the theorem premises are trusted."] toolchain_lock_sha256 = "0c45a8a08ac06e313d775e669749097bd3a0abfb8e3395c69416ba0238770d53" @@ -10355,7 +10355,7 @@ semantic_source_closure = [ "formal/qualification/aeneas/generated/model/FunsExternal.lean", "formal/qualification/aeneas/generated/model/Types.lean", ] -semantic_source_closure_sha256 = "1a9d3309c0f56c88f64aa0d60d4048d93f6ae0da6336af00d09f342294e9b249" +semantic_source_closure_sha256 = "a625715ca60dcf7c1c9f14b063fd20152a36e46b82c5a8494273c45049cea638" scope = "Pure V1 lifecycle transitions, capacity conservation, replay, configuration gates, credential ordering, provider entry, and reconciliation." residual_assumptions = ["Lean's kernel, the pinned toolchain, the listed foundational axioms, and the theorem premises are trusted."] toolchain_lock_sha256 = "0c45a8a08ac06e313d775e669749097bd3a0abfb8e3395c69416ba0238770d53" @@ -10420,7 +10420,7 @@ semantic_source_closure = [ "formal/qualification/aeneas/generated/model/FunsExternal.lean", "formal/qualification/aeneas/generated/model/Types.lean", ] -semantic_source_closure_sha256 = "1a9d3309c0f56c88f64aa0d60d4048d93f6ae0da6336af00d09f342294e9b249" +semantic_source_closure_sha256 = "a625715ca60dcf7c1c9f14b063fd20152a36e46b82c5a8494273c45049cea638" scope = "Pure V1 lifecycle transitions, capacity conservation, replay, configuration gates, credential ordering, provider entry, and reconciliation." residual_assumptions = ["Lean's kernel, the pinned toolchain, the listed foundational axioms, and the theorem premises are trusted."] toolchain_lock_sha256 = "0c45a8a08ac06e313d775e669749097bd3a0abfb8e3395c69416ba0238770d53" @@ -10485,7 +10485,7 @@ semantic_source_closure = [ "formal/qualification/aeneas/generated/model/FunsExternal.lean", "formal/qualification/aeneas/generated/model/Types.lean", ] -semantic_source_closure_sha256 = "1a9d3309c0f56c88f64aa0d60d4048d93f6ae0da6336af00d09f342294e9b249" +semantic_source_closure_sha256 = "a625715ca60dcf7c1c9f14b063fd20152a36e46b82c5a8494273c45049cea638" scope = "Pure V1 lifecycle transitions, capacity conservation, replay, configuration gates, credential ordering, provider entry, and reconciliation." residual_assumptions = ["Lean's kernel, the pinned toolchain, the listed foundational axioms, and the theorem premises are trusted."] toolchain_lock_sha256 = "0c45a8a08ac06e313d775e669749097bd3a0abfb8e3395c69416ba0238770d53" @@ -10550,7 +10550,7 @@ semantic_source_closure = [ "formal/qualification/aeneas/generated/model/FunsExternal.lean", "formal/qualification/aeneas/generated/model/Types.lean", ] -semantic_source_closure_sha256 = "1a9d3309c0f56c88f64aa0d60d4048d93f6ae0da6336af00d09f342294e9b249" +semantic_source_closure_sha256 = "a625715ca60dcf7c1c9f14b063fd20152a36e46b82c5a8494273c45049cea638" scope = "Pure V1 lifecycle transitions, capacity conservation, replay, configuration gates, credential ordering, provider entry, and reconciliation." residual_assumptions = ["Lean's kernel, the pinned toolchain, the listed foundational axioms, and the theorem premises are trusted."] toolchain_lock_sha256 = "0c45a8a08ac06e313d775e669749097bd3a0abfb8e3395c69416ba0238770d53" @@ -10615,7 +10615,7 @@ semantic_source_closure = [ "formal/qualification/aeneas/generated/model/FunsExternal.lean", "formal/qualification/aeneas/generated/model/Types.lean", ] -semantic_source_closure_sha256 = "1a9d3309c0f56c88f64aa0d60d4048d93f6ae0da6336af00d09f342294e9b249" +semantic_source_closure_sha256 = "a625715ca60dcf7c1c9f14b063fd20152a36e46b82c5a8494273c45049cea638" scope = "The pinned Charon/Aeneas translation of `auths_lifecycle::model::LifecycleState::is_terminal` is extensionally equivalent to the corresponding rich Lean V1 lifecycle semantics." residual_assumptions = ["Lean's kernel, the pinned Rust/Charon/Aeneas/Lean toolchain, the qualified translation boundary, the listed foundational axioms, and the theorem premises are trusted."] toolchain_lock_sha256 = "0c45a8a08ac06e313d775e669749097bd3a0abfb8e3395c69416ba0238770d53" @@ -10680,7 +10680,7 @@ semantic_source_closure = [ "formal/qualification/aeneas/generated/model/FunsExternal.lean", "formal/qualification/aeneas/generated/model/Types.lean", ] -semantic_source_closure_sha256 = "1a9d3309c0f56c88f64aa0d60d4048d93f6ae0da6336af00d09f342294e9b249" +semantic_source_closure_sha256 = "a625715ca60dcf7c1c9f14b063fd20152a36e46b82c5a8494273c45049cea638" scope = "The pinned Charon/Aeneas translation of `auths_lifecycle::kernel::transition_code` is extensionally equivalent to the corresponding rich Lean V1 lifecycle semantics." residual_assumptions = ["Lean's kernel, the pinned Rust/Charon/Aeneas/Lean toolchain, the qualified translation boundary, the listed foundational axioms, and the theorem premises are trusted."] toolchain_lock_sha256 = "0c45a8a08ac06e313d775e669749097bd3a0abfb8e3395c69416ba0238770d53" @@ -10748,7 +10748,7 @@ semantic_source_closure = [ "formal/qualification/aeneas/generated/model/FunsExternal.lean", "formal/qualification/aeneas/generated/model/Types.lean", ] -semantic_source_closure_sha256 = "1a9d3309c0f56c88f64aa0d60d4048d93f6ae0da6336af00d09f342294e9b249" +semantic_source_closure_sha256 = "a625715ca60dcf7c1c9f14b063fd20152a36e46b82c5a8494273c45049cea638" scope = "The pinned Charon/Aeneas translation of `auths_lifecycle::kernel::exclusive_capacity_available` is extensionally equivalent to the corresponding rich Lean V1 lifecycle semantics." residual_assumptions = ["Lean's kernel, the pinned Rust/Charon/Aeneas/Lean toolchain, the qualified translation boundary, the listed foundational axioms, and the theorem premises are trusted."] toolchain_lock_sha256 = "0c45a8a08ac06e313d775e669749097bd3a0abfb8e3395c69416ba0238770d53" @@ -10813,7 +10813,7 @@ semantic_source_closure = [ "formal/qualification/aeneas/generated/model/FunsExternal.lean", "formal/qualification/aeneas/generated/model/Types.lean", ] -semantic_source_closure_sha256 = "1a9d3309c0f56c88f64aa0d60d4048d93f6ae0da6336af00d09f342294e9b249" +semantic_source_closure_sha256 = "a625715ca60dcf7c1c9f14b063fd20152a36e46b82c5a8494273c45049cea638" scope = "The pinned Charon/Aeneas translation of `auths_lifecycle::kernel::additive_capacity_available` is extensionally equivalent to the corresponding rich Lean V1 lifecycle semantics." residual_assumptions = ["Lean's kernel, the pinned Rust/Charon/Aeneas/Lean toolchain, the qualified translation boundary, the listed foundational axioms, and the theorem premises are trusted."] toolchain_lock_sha256 = "0c45a8a08ac06e313d775e669749097bd3a0abfb8e3395c69416ba0238770d53" @@ -10882,7 +10882,7 @@ semantic_source_closure = [ "formal/qualification/aeneas/generated/model/FunsExternal.lean", "formal/qualification/aeneas/generated/model/Types.lean", ] -semantic_source_closure_sha256 = "1a9d3309c0f56c88f64aa0d60d4048d93f6ae0da6336af00d09f342294e9b249" +semantic_source_closure_sha256 = "a625715ca60dcf7c1c9f14b063fd20152a36e46b82c5a8494273c45049cea638" scope = "The pinned Charon/Aeneas translation of `auths_lifecycle::kernel::replay_code` is extensionally equivalent to the corresponding rich Lean V1 lifecycle semantics." residual_assumptions = ["Lean's kernel, the pinned Rust/Charon/Aeneas/Lean toolchain, the qualified translation boundary, the listed foundational axioms, and the theorem premises are trusted."] toolchain_lock_sha256 = "0c45a8a08ac06e313d775e669749097bd3a0abfb8e3395c69416ba0238770d53" @@ -10947,7 +10947,7 @@ semantic_source_closure = [ "formal/qualification/aeneas/generated/model/FunsExternal.lean", "formal/qualification/aeneas/generated/model/Types.lean", ] -semantic_source_closure_sha256 = "1a9d3309c0f56c88f64aa0d60d4048d93f6ae0da6336af00d09f342294e9b249" +semantic_source_closure_sha256 = "a625715ca60dcf7c1c9f14b063fd20152a36e46b82c5a8494273c45049cea638" scope = "The closed three-valued binary all operator." residual_assumptions = ["Lean's kernel, the pinned toolchain, and the listed foundational axioms are trusted."] toolchain_lock_sha256 = "0c45a8a08ac06e313d775e669749097bd3a0abfb8e3395c69416ba0238770d53" @@ -11012,7 +11012,7 @@ semantic_source_closure = [ "formal/qualification/aeneas/generated/model/FunsExternal.lean", "formal/qualification/aeneas/generated/model/Types.lean", ] -semantic_source_closure_sha256 = "1a9d3309c0f56c88f64aa0d60d4048d93f6ae0da6336af00d09f342294e9b249" +semantic_source_closure_sha256 = "a625715ca60dcf7c1c9f14b063fd20152a36e46b82c5a8494273c45049cea638" scope = "The closed three-valued binary all operator." residual_assumptions = ["Lean's kernel, the pinned toolchain, and the listed foundational axioms are trusted."] toolchain_lock_sha256 = "0c45a8a08ac06e313d775e669749097bd3a0abfb8e3395c69416ba0238770d53" @@ -11077,7 +11077,7 @@ semantic_source_closure = [ "formal/qualification/aeneas/generated/model/FunsExternal.lean", "formal/qualification/aeneas/generated/model/Types.lean", ] -semantic_source_closure_sha256 = "1a9d3309c0f56c88f64aa0d60d4048d93f6ae0da6336af00d09f342294e9b249" +semantic_source_closure_sha256 = "a625715ca60dcf7c1c9f14b063fd20152a36e46b82c5a8494273c45049cea638" scope = "The closed three-valued binary all operator." residual_assumptions = ["Lean's kernel, the pinned toolchain, and the listed foundational axioms are trusted."] toolchain_lock_sha256 = "0c45a8a08ac06e313d775e669749097bd3a0abfb8e3395c69416ba0238770d53" @@ -11142,7 +11142,7 @@ semantic_source_closure = [ "formal/qualification/aeneas/generated/model/FunsExternal.lean", "formal/qualification/aeneas/generated/model/Types.lean", ] -semantic_source_closure_sha256 = "1a9d3309c0f56c88f64aa0d60d4048d93f6ae0da6336af00d09f342294e9b249" +semantic_source_closure_sha256 = "a625715ca60dcf7c1c9f14b063fd20152a36e46b82c5a8494273c45049cea638" scope = "The closed three-valued binary any operator." residual_assumptions = ["Lean's kernel, the pinned toolchain, and the listed foundational axioms are trusted."] toolchain_lock_sha256 = "0c45a8a08ac06e313d775e669749097bd3a0abfb8e3395c69416ba0238770d53" @@ -11207,7 +11207,7 @@ semantic_source_closure = [ "formal/qualification/aeneas/generated/model/FunsExternal.lean", "formal/qualification/aeneas/generated/model/Types.lean", ] -semantic_source_closure_sha256 = "1a9d3309c0f56c88f64aa0d60d4048d93f6ae0da6336af00d09f342294e9b249" +semantic_source_closure_sha256 = "a625715ca60dcf7c1c9f14b063fd20152a36e46b82c5a8494273c45049cea638" scope = "The closed three-valued binary any operator." residual_assumptions = ["Lean's kernel, the pinned toolchain, and the listed foundational axioms are trusted."] toolchain_lock_sha256 = "0c45a8a08ac06e313d775e669749097bd3a0abfb8e3395c69416ba0238770d53" @@ -11272,7 +11272,7 @@ semantic_source_closure = [ "formal/qualification/aeneas/generated/model/FunsExternal.lean", "formal/qualification/aeneas/generated/model/Types.lean", ] -semantic_source_closure_sha256 = "1a9d3309c0f56c88f64aa0d60d4048d93f6ae0da6336af00d09f342294e9b249" +semantic_source_closure_sha256 = "a625715ca60dcf7c1c9f14b063fd20152a36e46b82c5a8494273c45049cea638" scope = "The closed three-valued binary any operator." residual_assumptions = ["Lean's kernel, the pinned toolchain, and the listed foundational axioms are trusted."] toolchain_lock_sha256 = "0c45a8a08ac06e313d775e669749097bd3a0abfb8e3395c69416ba0238770d53" @@ -11337,7 +11337,7 @@ semantic_source_closure = [ "formal/qualification/aeneas/generated/model/FunsExternal.lean", "formal/qualification/aeneas/generated/model/Types.lean", ] -semantic_source_closure_sha256 = "1a9d3309c0f56c88f64aa0d60d4048d93f6ae0da6336af00d09f342294e9b249" +semantic_source_closure_sha256 = "a625715ca60dcf7c1c9f14b063fd20152a36e46b82c5a8494273c45049cea638" scope = "The generated two-input threshold abstraction." residual_assumptions = ["Lean's kernel, the pinned toolchain, generator correctness, and the Rust vector harness are trusted."] toolchain_lock_sha256 = "0c45a8a08ac06e313d775e669749097bd3a0abfb8e3395c69416ba0238770d53" @@ -11407,7 +11407,7 @@ semantic_source_closure = [ "formal/qualification/aeneas/generated/model/FunsExternal.lean", "formal/qualification/aeneas/generated/model/Types.lean", ] -semantic_source_closure_sha256 = "1a9d3309c0f56c88f64aa0d60d4048d93f6ae0da6336af00d09f342294e9b249" +semantic_source_closure_sha256 = "a625715ca60dcf7c1c9f14b063fd20152a36e46b82c5a8494273c45049cea638" scope = "The generated two-input threshold abstraction." residual_assumptions = ["Lean's kernel, the pinned toolchain, generator correctness, and the Rust vector harness are trusted."] toolchain_lock_sha256 = "0c45a8a08ac06e313d775e669749097bd3a0abfb8e3395c69416ba0238770d53" @@ -11477,7 +11477,7 @@ semantic_source_closure = [ "formal/qualification/aeneas/generated/model/FunsExternal.lean", "formal/qualification/aeneas/generated/model/Types.lean", ] -semantic_source_closure_sha256 = "1a9d3309c0f56c88f64aa0d60d4048d93f6ae0da6336af00d09f342294e9b249" +semantic_source_closure_sha256 = "a625715ca60dcf7c1c9f14b063fd20152a36e46b82c5a8494273c45049cea638" scope = "Exactly the two-input threshold helper and the declared three-valued truth order." residual_assumptions = ["Lean's kernel, the pinned toolchain, listed foundational axioms, generator correctness, and the Rust vector harness are trusted."] toolchain_lock_sha256 = "0c45a8a08ac06e313d775e669749097bd3a0abfb8e3395c69416ba0238770d53" @@ -11550,7 +11550,7 @@ semantic_source_closure = [ "formal/qualification/aeneas/generated/model/FunsExternal.lean", "formal/qualification/aeneas/generated/model/Types.lean", ] -semantic_source_closure_sha256 = "1a9d3309c0f56c88f64aa0d60d4048d93f6ae0da6336af00d09f342294e9b249" +semantic_source_closure_sha256 = "a625715ca60dcf7c1c9f14b063fd20152a36e46b82c5a8494273c45049cea638" scope = "A two-value swap only; arbitrary authorization-plan permutations are not claimed." residual_assumptions = ["Lean's kernel, the pinned toolchain, and the listed foundational axioms are trusted."] toolchain_lock_sha256 = "0c45a8a08ac06e313d775e669749097bd3a0abfb8e3395c69416ba0238770d53" @@ -11615,7 +11615,7 @@ semantic_source_closure = [ "formal/qualification/aeneas/generated/model/FunsExternal.lean", "formal/qualification/aeneas/generated/model/Types.lean", ] -semantic_source_closure_sha256 = "1a9d3309c0f56c88f64aa0d60d4048d93f6ae0da6336af00d09f342294e9b249" +semantic_source_closure_sha256 = "a625715ca60dcf7c1c9f14b063fd20152a36e46b82c5a8494273c45049cea638" scope = "The two-value canonicalCode helper; arbitrary plan diagnostic permutations are not claimed." residual_assumptions = ["Lean's kernel, the pinned toolchain, and the listed foundational axioms are trusted."] toolchain_lock_sha256 = "0c45a8a08ac06e313d775e669749097bd3a0abfb8e3395c69416ba0238770d53" @@ -11680,7 +11680,7 @@ semantic_source_closure = [ "formal/qualification/aeneas/generated/model/FunsExternal.lean", "formal/qualification/aeneas/generated/model/Types.lean", ] -semantic_source_closure_sha256 = "1a9d3309c0f56c88f64aa0d60d4048d93f6ae0da6336af00d09f342294e9b249" +semantic_source_closure_sha256 = "a625715ca60dcf7c1c9f14b063fd20152a36e46b82c5a8494273c45049cea638" scope = "A definitional model equality; it does not prove that the shipping evaluator visits leaves once." residual_assumptions = ["Lean's kernel, the pinned toolchain, and the listed foundational axioms are trusted."] toolchain_lock_sha256 = "0c45a8a08ac06e313d775e669749097bd3a0abfb8e3395c69416ba0238770d53" @@ -11748,7 +11748,7 @@ semantic_source_closure = [ "formal/qualification/aeneas/generated/model/FunsExternal.lean", "formal/qualification/aeneas/generated/model/Types.lean", ] -semantic_source_closure_sha256 = "1a9d3309c0f56c88f64aa0d60d4048d93f6ae0da6336af00d09f342294e9b249" +semantic_source_closure_sha256 = "a625715ca60dcf7c1c9f14b063fd20152a36e46b82c5a8494273c45049cea638" scope = "A definitional model equality; no asymptotic or shipping evaluator cost bound is claimed." residual_assumptions = ["Lean's kernel, the pinned toolchain, and the listed foundational axioms are trusted."] toolchain_lock_sha256 = "0c45a8a08ac06e313d775e669749097bd3a0abfb8e3395c69416ba0238770d53" @@ -11816,7 +11816,7 @@ semantic_source_closure = [ "formal/qualification/aeneas/generated/model/FunsExternal.lean", "formal/qualification/aeneas/generated/model/Types.lean", ] -semantic_source_closure_sha256 = "1a9d3309c0f56c88f64aa0d60d4048d93f6ae0da6336af00d09f342294e9b249" +semantic_source_closure_sha256 = "a625715ca60dcf7c1c9f14b063fd20152a36e46b82c5a8494273c45049cea638" scope = "The generated count classifier and its exhaustive target-V1 bounded Rust vectors." residual_assumptions = ["Lean's kernel, the pinned toolchain, generator correctness, and the Rust vector harness are trusted."] toolchain_lock_sha256 = "0c45a8a08ac06e313d775e669749097bd3a0abfb8e3395c69416ba0238770d53" @@ -11886,7 +11886,7 @@ semantic_source_closure = [ "formal/qualification/aeneas/generated/model/FunsExternal.lean", "formal/qualification/aeneas/generated/model/Types.lean", ] -semantic_source_closure_sha256 = "1a9d3309c0f56c88f64aa0d60d4048d93f6ae0da6336af00d09f342294e9b249" +semantic_source_closure_sha256 = "a625715ca60dcf7c1c9f14b063fd20152a36e46b82c5a8494273c45049cea638" scope = "The generated count classifier and its exhaustive target-V1 bounded Rust vectors." residual_assumptions = ["Lean's kernel, the pinned toolchain, listed foundational axioms, generator correctness, and the Rust vector harness are trusted."] toolchain_lock_sha256 = "0c45a8a08ac06e313d775e669749097bd3a0abfb8e3395c69416ba0238770d53" @@ -11959,7 +11959,7 @@ semantic_source_closure = [ "formal/qualification/aeneas/generated/model/FunsExternal.lean", "formal/qualification/aeneas/generated/model/Types.lean", ] -semantic_source_closure_sha256 = "1a9d3309c0f56c88f64aa0d60d4048d93f6ae0da6336af00d09f342294e9b249" +semantic_source_closure_sha256 = "a625715ca60dcf7c1c9f14b063fd20152a36e46b82c5a8494273c45049cea638" scope = "The generated count classifier and its exhaustive target-V1 bounded Rust vectors." residual_assumptions = ["Lean's kernel, the pinned toolchain, listed foundational axioms, generator correctness, and the Rust vector harness are trusted."] toolchain_lock_sha256 = "0c45a8a08ac06e313d775e669749097bd3a0abfb8e3395c69416ba0238770d53" @@ -12033,7 +12033,7 @@ semantic_source_closure = [ "formal/qualification/aeneas/generated/model/FunsExternal.lean", "formal/qualification/aeneas/generated/model/Types.lean", ] -semantic_source_closure_sha256 = "1a9d3309c0f56c88f64aa0d60d4048d93f6ae0da6336af00d09f342294e9b249" +semantic_source_closure_sha256 = "a625715ca60dcf7c1c9f14b063fd20152a36e46b82c5a8494273c45049cea638" scope = "Abstract evidence-conditioned authority: closed conjunctive observation conditions, freshness, observer and subject binding, over already verified observations and an abstract subject namespace matcher." residual_assumptions = ["Lean's kernel, the pinned toolchain, the listed foundational axioms, and the theorem premises are trusted."] toolchain_lock_sha256 = "0c45a8a08ac06e313d775e669749097bd3a0abfb8e3395c69416ba0238770d53" @@ -12101,7 +12101,7 @@ semantic_source_closure = [ "formal/qualification/aeneas/generated/model/FunsExternal.lean", "formal/qualification/aeneas/generated/model/Types.lean", ] -semantic_source_closure_sha256 = "1a9d3309c0f56c88f64aa0d60d4048d93f6ae0da6336af00d09f342294e9b249" +semantic_source_closure_sha256 = "a625715ca60dcf7c1c9f14b063fd20152a36e46b82c5a8494273c45049cea638" scope = "Abstract evidence-conditioned authority: closed conjunctive observation conditions, freshness, observer and subject binding, over already verified observations and an abstract subject namespace matcher." residual_assumptions = ["Lean's kernel, the pinned toolchain, the listed foundational axioms, and the theorem premises are trusted."] toolchain_lock_sha256 = "0c45a8a08ac06e313d775e669749097bd3a0abfb8e3395c69416ba0238770d53" @@ -12169,7 +12169,7 @@ semantic_source_closure = [ "formal/qualification/aeneas/generated/model/FunsExternal.lean", "formal/qualification/aeneas/generated/model/Types.lean", ] -semantic_source_closure_sha256 = "1a9d3309c0f56c88f64aa0d60d4048d93f6ae0da6336af00d09f342294e9b249" +semantic_source_closure_sha256 = "a625715ca60dcf7c1c9f14b063fd20152a36e46b82c5a8494273c45049cea638" scope = "Abstract evidence-conditioned authority: closed conjunctive observation conditions, freshness, observer and subject binding, over already verified observations and an abstract subject namespace matcher." residual_assumptions = ["Lean's kernel, the pinned toolchain, the listed foundational axioms, and the theorem premises are trusted."] toolchain_lock_sha256 = "0c45a8a08ac06e313d775e669749097bd3a0abfb8e3395c69416ba0238770d53" @@ -12237,7 +12237,7 @@ semantic_source_closure = [ "formal/qualification/aeneas/generated/model/FunsExternal.lean", "formal/qualification/aeneas/generated/model/Types.lean", ] -semantic_source_closure_sha256 = "1a9d3309c0f56c88f64aa0d60d4048d93f6ae0da6336af00d09f342294e9b249" +semantic_source_closure_sha256 = "a625715ca60dcf7c1c9f14b063fd20152a36e46b82c5a8494273c45049cea638" scope = "Abstract evidence-conditioned authority: closed conjunctive observation conditions, freshness, observer and subject binding, over already verified observations and an abstract subject namespace matcher." residual_assumptions = ["Lean's kernel, the pinned toolchain, the listed foundational axioms, and the theorem premises are trusted."] toolchain_lock_sha256 = "0c45a8a08ac06e313d775e669749097bd3a0abfb8e3395c69416ba0238770d53" @@ -12305,7 +12305,7 @@ semantic_source_closure = [ "formal/qualification/aeneas/generated/model/FunsExternal.lean", "formal/qualification/aeneas/generated/model/Types.lean", ] -semantic_source_closure_sha256 = "1a9d3309c0f56c88f64aa0d60d4048d93f6ae0da6336af00d09f342294e9b249" +semantic_source_closure_sha256 = "a625715ca60dcf7c1c9f14b063fd20152a36e46b82c5a8494273c45049cea638" scope = "Abstract evidence-conditioned authority: closed conjunctive observation conditions, freshness, observer and subject binding, over already verified observations and an abstract subject namespace matcher." residual_assumptions = ["Lean's kernel, the pinned toolchain, the listed foundational axioms, and the theorem premises are trusted."] toolchain_lock_sha256 = "0c45a8a08ac06e313d775e669749097bd3a0abfb8e3395c69416ba0238770d53" @@ -12370,7 +12370,7 @@ semantic_source_closure = [ "formal/qualification/aeneas/generated/model/FunsExternal.lean", "formal/qualification/aeneas/generated/model/Types.lean", ] -semantic_source_closure_sha256 = "1a9d3309c0f56c88f64aa0d60d4048d93f6ae0da6336af00d09f342294e9b249" +semantic_source_closure_sha256 = "a625715ca60dcf7c1c9f14b063fd20152a36e46b82c5a8494273c45049cea638" scope = "Abstract evidence-conditioned authority: closed conjunctive observation conditions, freshness, observer and subject binding, over already verified observations and an abstract subject namespace matcher." residual_assumptions = ["Lean's kernel, the pinned toolchain, the listed foundational axioms, and the theorem premises are trusted."] toolchain_lock_sha256 = "0c45a8a08ac06e313d775e669749097bd3a0abfb8e3395c69416ba0238770d53" @@ -12439,7 +12439,7 @@ semantic_source_closure = [ "formal/qualification/aeneas/generated/model/FunsExternal.lean", "formal/qualification/aeneas/generated/model/Types.lean", ] -semantic_source_closure_sha256 = "1a9d3309c0f56c88f64aa0d60d4048d93f6ae0da6336af00d09f342294e9b249" +semantic_source_closure_sha256 = "a625715ca60dcf7c1c9f14b063fd20152a36e46b82c5a8494273c45049cea638" scope = "Abstract evidence-conditioned authority: closed conjunctive observation conditions, freshness, observer and subject binding, over already verified observations and an abstract subject namespace matcher." residual_assumptions = ["Lean's kernel, the pinned toolchain, the listed foundational axioms, and the theorem premises are trusted."] toolchain_lock_sha256 = "0c45a8a08ac06e313d775e669749097bd3a0abfb8e3395c69416ba0238770d53" @@ -12508,7 +12508,7 @@ semantic_source_closure = [ "formal/qualification/aeneas/generated/model/FunsExternal.lean", "formal/qualification/aeneas/generated/model/Types.lean", ] -semantic_source_closure_sha256 = "1a9d3309c0f56c88f64aa0d60d4048d93f6ae0da6336af00d09f342294e9b249" +semantic_source_closure_sha256 = "a625715ca60dcf7c1c9f14b063fd20152a36e46b82c5a8494273c45049cea638" scope = "Abstract evidence-conditioned authority: closed conjunctive observation conditions, freshness, observer and subject binding, over already verified observations and an abstract subject namespace matcher." residual_assumptions = ["Lean's kernel, the pinned toolchain, the listed foundational axioms, and the theorem premises are trusted."] toolchain_lock_sha256 = "0c45a8a08ac06e313d775e669749097bd3a0abfb8e3395c69416ba0238770d53" @@ -12576,7 +12576,7 @@ semantic_source_closure = [ "formal/qualification/aeneas/generated/model/FunsExternal.lean", "formal/qualification/aeneas/generated/model/Types.lean", ] -semantic_source_closure_sha256 = "1a9d3309c0f56c88f64aa0d60d4048d93f6ae0da6336af00d09f342294e9b249" +semantic_source_closure_sha256 = "a625715ca60dcf7c1c9f14b063fd20152a36e46b82c5a8494273c45049cea638" scope = "Abstract evidence-conditioned authority: closed conjunctive observation conditions, freshness, observer and subject binding, over already verified observations and an abstract subject namespace matcher." residual_assumptions = ["Lean's kernel, the pinned toolchain, the listed foundational axioms, and the theorem premises are trusted."] toolchain_lock_sha256 = "0c45a8a08ac06e313d775e669749097bd3a0abfb8e3395c69416ba0238770d53" @@ -12644,7 +12644,7 @@ semantic_source_closure = [ "formal/qualification/aeneas/generated/model/FunsExternal.lean", "formal/qualification/aeneas/generated/model/Types.lean", ] -semantic_source_closure_sha256 = "1a9d3309c0f56c88f64aa0d60d4048d93f6ae0da6336af00d09f342294e9b249" +semantic_source_closure_sha256 = "a625715ca60dcf7c1c9f14b063fd20152a36e46b82c5a8494273c45049cea638" scope = "Abstract evidence-conditioned authority: closed conjunctive observation conditions, freshness, observer and subject binding, over already verified observations and an abstract subject namespace matcher." residual_assumptions = ["Lean's kernel, the pinned toolchain, the listed foundational axioms, and the theorem premises are trusted."] toolchain_lock_sha256 = "0c45a8a08ac06e313d775e669749097bd3a0abfb8e3395c69416ba0238770d53" @@ -12712,7 +12712,7 @@ semantic_source_closure = [ "formal/qualification/aeneas/generated/model/FunsExternal.lean", "formal/qualification/aeneas/generated/model/Types.lean", ] -semantic_source_closure_sha256 = "1a9d3309c0f56c88f64aa0d60d4048d93f6ae0da6336af00d09f342294e9b249" +semantic_source_closure_sha256 = "a625715ca60dcf7c1c9f14b063fd20152a36e46b82c5a8494273c45049cea638" scope = "Abstract evidence-conditioned authority: closed conjunctive observation conditions, freshness, observer and subject binding, over already verified observations and an abstract subject namespace matcher." residual_assumptions = ["Lean's kernel, the pinned toolchain, the listed foundational axioms, and the theorem premises are trusted."] toolchain_lock_sha256 = "0c45a8a08ac06e313d775e669749097bd3a0abfb8e3395c69416ba0238770d53" @@ -12781,7 +12781,7 @@ semantic_source_closure = [ "formal/qualification/aeneas/generated/model/FunsExternal.lean", "formal/qualification/aeneas/generated/model/Types.lean", ] -semantic_source_closure_sha256 = "1a9d3309c0f56c88f64aa0d60d4048d93f6ae0da6336af00d09f342294e9b249" +semantic_source_closure_sha256 = "a625715ca60dcf7c1c9f14b063fd20152a36e46b82c5a8494273c45049cea638" scope = "Abstract evidence-conditioned authority: closed conjunctive observation conditions, freshness, observer and subject binding, over already verified observations and an abstract subject namespace matcher." residual_assumptions = ["Lean's kernel, the pinned toolchain, the listed foundational axioms, and the theorem premises are trusted."] toolchain_lock_sha256 = "0c45a8a08ac06e313d775e669749097bd3a0abfb8e3395c69416ba0238770d53" @@ -12850,7 +12850,7 @@ semantic_source_closure = [ "formal/qualification/aeneas/generated/model/FunsExternal.lean", "formal/qualification/aeneas/generated/model/Types.lean", ] -semantic_source_closure_sha256 = "1a9d3309c0f56c88f64aa0d60d4048d93f6ae0da6336af00d09f342294e9b249" +semantic_source_closure_sha256 = "a625715ca60dcf7c1c9f14b063fd20152a36e46b82c5a8494273c45049cea638" scope = "Abstract evidence-conditioned authority: closed conjunctive observation conditions, freshness, observer and subject binding, over already verified observations and an abstract subject namespace matcher." residual_assumptions = ["Lean's kernel, the pinned toolchain, the listed foundational axioms, and the theorem premises are trusted."] toolchain_lock_sha256 = "0c45a8a08ac06e313d775e669749097bd3a0abfb8e3395c69416ba0238770d53" @@ -12919,7 +12919,7 @@ semantic_source_closure = [ "formal/qualification/aeneas/generated/model/FunsExternal.lean", "formal/qualification/aeneas/generated/model/Types.lean", ] -semantic_source_closure_sha256 = "1a9d3309c0f56c88f64aa0d60d4048d93f6ae0da6336af00d09f342294e9b249" +semantic_source_closure_sha256 = "a625715ca60dcf7c1c9f14b063fd20152a36e46b82c5a8494273c45049cea638" scope = "Abstract evidence-conditioned authority: closed conjunctive observation conditions, freshness, observer and subject binding, over already verified observations and an abstract subject namespace matcher." residual_assumptions = ["Lean's kernel, the pinned toolchain, the listed foundational axioms, and the theorem premises are trusted."] toolchain_lock_sha256 = "0c45a8a08ac06e313d775e669749097bd3a0abfb8e3395c69416ba0238770d53" @@ -12987,7 +12987,7 @@ semantic_source_closure = [ "formal/qualification/aeneas/generated/model/FunsExternal.lean", "formal/qualification/aeneas/generated/model/Types.lean", ] -semantic_source_closure_sha256 = "1a9d3309c0f56c88f64aa0d60d4048d93f6ae0da6336af00d09f342294e9b249" +semantic_source_closure_sha256 = "a625715ca60dcf7c1c9f14b063fd20152a36e46b82c5a8494273c45049cea638" scope = "Abstract evidence-conditioned authority: closed conjunctive observation conditions, freshness, observer and subject binding, over already verified observations and an abstract subject namespace matcher." residual_assumptions = ["Lean's kernel, the pinned toolchain, the listed foundational axioms, and the theorem premises are trusted."] toolchain_lock_sha256 = "0c45a8a08ac06e313d775e669749097bd3a0abfb8e3395c69416ba0238770d53" @@ -13052,7 +13052,7 @@ semantic_source_closure = [ "formal/qualification/aeneas/generated/model/FunsExternal.lean", "formal/qualification/aeneas/generated/model/Types.lean", ] -semantic_source_closure_sha256 = "1a9d3309c0f56c88f64aa0d60d4048d93f6ae0da6336af00d09f342294e9b249" +semantic_source_closure_sha256 = "a625715ca60dcf7c1c9f14b063fd20152a36e46b82c5a8494273c45049cea638" scope = "Abstract evidence-conditioned authority: closed conjunctive observation conditions, freshness, observer and subject binding, over already verified observations and an abstract subject namespace matcher." residual_assumptions = ["Lean's kernel, the pinned toolchain, the listed foundational axioms, and the theorem premises are trusted."] toolchain_lock_sha256 = "0c45a8a08ac06e313d775e669749097bd3a0abfb8e3395c69416ba0238770d53" @@ -13120,7 +13120,7 @@ semantic_source_closure = [ "formal/qualification/aeneas/generated/model/FunsExternal.lean", "formal/qualification/aeneas/generated/model/Types.lean", ] -semantic_source_closure_sha256 = "1a9d3309c0f56c88f64aa0d60d4048d93f6ae0da6336af00d09f342294e9b249" +semantic_source_closure_sha256 = "a625715ca60dcf7c1c9f14b063fd20152a36e46b82c5a8494273c45049cea638" scope = "Abstract evidence-conditioned authority: closed conjunctive observation conditions, freshness, observer and subject binding, over already verified observations and an abstract subject namespace matcher." residual_assumptions = ["Lean's kernel, the pinned toolchain, the listed foundational axioms, and the theorem premises are trusted."] toolchain_lock_sha256 = "0c45a8a08ac06e313d775e669749097bd3a0abfb8e3395c69416ba0238770d53" @@ -13189,7 +13189,7 @@ semantic_source_closure = [ "formal/qualification/aeneas/generated/model/FunsExternal.lean", "formal/qualification/aeneas/generated/model/Types.lean", ] -semantic_source_closure_sha256 = "1a9d3309c0f56c88f64aa0d60d4048d93f6ae0da6336af00d09f342294e9b249" +semantic_source_closure_sha256 = "a625715ca60dcf7c1c9f14b063fd20152a36e46b82c5a8494273c45049cea638" scope = "Critical-extension attenuation laws over decoded payloads: each registered handler law is a preorder that narrows the worlds its payload admits." residual_assumptions = ["Lean's kernel, the pinned toolchain, the listed foundational axioms, and the theorem premises are trusted."] toolchain_lock_sha256 = "0c45a8a08ac06e313d775e669749097bd3a0abfb8e3395c69416ba0238770d53" @@ -13258,7 +13258,7 @@ semantic_source_closure = [ "formal/qualification/aeneas/generated/model/FunsExternal.lean", "formal/qualification/aeneas/generated/model/Types.lean", ] -semantic_source_closure_sha256 = "1a9d3309c0f56c88f64aa0d60d4048d93f6ae0da6336af00d09f342294e9b249" +semantic_source_closure_sha256 = "a625715ca60dcf7c1c9f14b063fd20152a36e46b82c5a8494273c45049cea638" scope = "Critical-extension attenuation laws over decoded payloads: each registered handler law is a preorder that narrows the worlds its payload admits." residual_assumptions = ["Lean's kernel, the pinned toolchain, the listed foundational axioms, and the theorem premises are trusted."] toolchain_lock_sha256 = "0c45a8a08ac06e313d775e669749097bd3a0abfb8e3395c69416ba0238770d53" @@ -13323,7 +13323,7 @@ semantic_source_closure = [ "formal/qualification/aeneas/generated/model/FunsExternal.lean", "formal/qualification/aeneas/generated/model/Types.lean", ] -semantic_source_closure_sha256 = "1a9d3309c0f56c88f64aa0d60d4048d93f6ae0da6336af00d09f342294e9b249" +semantic_source_closure_sha256 = "a625715ca60dcf7c1c9f14b063fd20152a36e46b82c5a8494273c45049cea638" scope = "Critical-extension attenuation laws over decoded payloads: each registered handler law is a preorder that narrows the worlds its payload admits." residual_assumptions = ["Lean's kernel, the pinned toolchain, the listed foundational axioms, and the theorem premises are trusted."] toolchain_lock_sha256 = "0c45a8a08ac06e313d775e669749097bd3a0abfb8e3395c69416ba0238770d53" @@ -13388,7 +13388,7 @@ semantic_source_closure = [ "formal/qualification/aeneas/generated/model/FunsExternal.lean", "formal/qualification/aeneas/generated/model/Types.lean", ] -semantic_source_closure_sha256 = "1a9d3309c0f56c88f64aa0d60d4048d93f6ae0da6336af00d09f342294e9b249" +semantic_source_closure_sha256 = "a625715ca60dcf7c1c9f14b063fd20152a36e46b82c5a8494273c45049cea638" scope = "Critical-extension attenuation laws over decoded payloads: each registered handler law is a preorder that narrows the worlds its payload admits." residual_assumptions = ["Lean's kernel, the pinned toolchain, the listed foundational axioms, and the theorem premises are trusted."] toolchain_lock_sha256 = "0c45a8a08ac06e313d775e669749097bd3a0abfb8e3395c69416ba0238770d53" @@ -13453,7 +13453,7 @@ semantic_source_closure = [ "formal/qualification/aeneas/generated/model/FunsExternal.lean", "formal/qualification/aeneas/generated/model/Types.lean", ] -semantic_source_closure_sha256 = "1a9d3309c0f56c88f64aa0d60d4048d93f6ae0da6336af00d09f342294e9b249" +semantic_source_closure_sha256 = "a625715ca60dcf7c1c9f14b063fd20152a36e46b82c5a8494273c45049cea638" scope = "Rich target-V1 authority semantics over opaque identity carriers and extensional finite sets." residual_assumptions = ["Lean's kernel, the pinned toolchain, the listed foundational axioms, and the theorem premises are trusted."] toolchain_lock_sha256 = "0c45a8a08ac06e313d775e669749097bd3a0abfb8e3395c69416ba0238770d53" @@ -13518,7 +13518,7 @@ semantic_source_closure = [ "formal/qualification/aeneas/generated/model/FunsExternal.lean", "formal/qualification/aeneas/generated/model/Types.lean", ] -semantic_source_closure_sha256 = "1a9d3309c0f56c88f64aa0d60d4048d93f6ae0da6336af00d09f342294e9b249" +semantic_source_closure_sha256 = "a625715ca60dcf7c1c9f14b063fd20152a36e46b82c5a8494273c45049cea638" scope = "UTF-8 byte comparison of two fact names, bridged to String equality by UTF-8 injectivity." residual_assumptions = [ "Lean's kernel, the pinned Rust/Charon/Aeneas/Lean toolchain, the reviewed transparent external bridges, the listed foundational axioms, and the theorem's explicit representation-validity premises (every compared text fits the u32 UTF-8 byte bound) are trusted.", @@ -13539,12 +13539,12 @@ sha256 = "0bb2cdcf0806b77a207ed0196f697249d394c3036758ddcf9545c63eb3f7afc7" [[claims.evidence]] kind = "mechanical-translation" artifact = "formal/qualification/aeneas/generated/model/Funs.lean" -sha256 = "3836a626ec93077801d41fbf8e11e3086fc5b416af668c488710ab0717c66c92" +sha256 = "aa3f5bf6211f243c8cf937f08bddda0bc5f6219d935bd9a67c9214bb1799f598" [[claims.evidence]] kind = "source-closure" artifact = "formal/qualification/aeneas/source-closure.json" -sha256 = "047b34bfe6deab4196c24256f55987245376abc6ddf57a4de8df1212c73bfec9" +sha256 = "c9eeba1225594d6dba4da1f0fc803480c0384b9c39c27b5ad1257012dd9fe9d0" [[claims]] claim_id = "AP-FORMAL-RICH-189" @@ -13600,7 +13600,7 @@ semantic_source_closure = [ "formal/qualification/aeneas/generated/model/FunsExternal.lean", "formal/qualification/aeneas/generated/model/Types.lean", ] -semantic_source_closure_sha256 = "1a9d3309c0f56c88f64aa0d60d4048d93f6ae0da6336af00d09f342294e9b249" +semantic_source_closure_sha256 = "a625715ca60dcf7c1c9f14b063fd20152a36e46b82c5a8494273c45049cea638" scope = "The guarded u64 age subtraction, maximum age, and anchor validity window, for every u64 input." residual_assumptions = [ "Lean's kernel, the pinned Rust/Charon/Aeneas/Lean toolchain, the reviewed transparent external bridges, the listed foundational axioms, and the theorem's explicit representation-validity premises (every compared text fits the u32 UTF-8 byte bound) are trusted.", @@ -13621,12 +13621,12 @@ sha256 = "0bb2cdcf0806b77a207ed0196f697249d394c3036758ddcf9545c63eb3f7afc7" [[claims.evidence]] kind = "mechanical-translation" artifact = "formal/qualification/aeneas/generated/model/Funs.lean" -sha256 = "3836a626ec93077801d41fbf8e11e3086fc5b416af668c488710ab0717c66c92" +sha256 = "aa3f5bf6211f243c8cf937f08bddda0bc5f6219d935bd9a67c9214bb1799f598" [[claims.evidence]] kind = "source-closure" artifact = "formal/qualification/aeneas/source-closure.json" -sha256 = "047b34bfe6deab4196c24256f55987245376abc6ddf57a4de8df1212c73bfec9" +sha256 = "c9eeba1225594d6dba4da1f0fc803480c0384b9c39c27b5ad1257012dd9fe9d0" [[claims]] claim_id = "AP-FORMAL-RICH-190" @@ -13682,7 +13682,7 @@ semantic_source_closure = [ "formal/qualification/aeneas/generated/model/FunsExternal.lean", "formal/qualification/aeneas/generated/model/Types.lean", ] -semantic_source_closure_sha256 = "1a9d3309c0f56c88f64aa0d60d4048d93f6ae0da6336af00d09f342294e9b249" +semantic_source_closure_sha256 = "a625715ca60dcf7c1c9f14b063fd20152a36e46b82c5a8494273c45049cea638" scope = "UTF-8 byte comparison of the expected and observed resource, bridged to String equality." residual_assumptions = [ "Lean's kernel, the pinned Rust/Charon/Aeneas/Lean toolchain, the reviewed transparent external bridges, the listed foundational axioms, and the theorem's explicit representation-validity premises (every compared text fits the u32 UTF-8 byte bound) are trusted.", @@ -13703,12 +13703,12 @@ sha256 = "0bb2cdcf0806b77a207ed0196f697249d394c3036758ddcf9545c63eb3f7afc7" [[claims.evidence]] kind = "mechanical-translation" artifact = "formal/qualification/aeneas/generated/model/Funs.lean" -sha256 = "3836a626ec93077801d41fbf8e11e3086fc5b416af668c488710ab0717c66c92" +sha256 = "aa3f5bf6211f243c8cf937f08bddda0bc5f6219d935bd9a67c9214bb1799f598" [[claims.evidence]] kind = "source-closure" artifact = "formal/qualification/aeneas/source-closure.json" -sha256 = "047b34bfe6deab4196c24256f55987245376abc6ddf57a4de8df1212c73bfec9" +sha256 = "c9eeba1225594d6dba4da1f0fc803480c0384b9c39c27b5ad1257012dd9fe9d0" [[claims]] claim_id = "AP-FORMAL-RICH-191" @@ -13764,7 +13764,7 @@ semantic_source_closure = [ "formal/qualification/aeneas/generated/model/FunsExternal.lean", "formal/qualification/aeneas/generated/model/Types.lean", ] -semantic_source_closure_sha256 = "1a9d3309c0f56c88f64aa0d60d4048d93f6ae0da6336af00d09f342294e9b249" +semantic_source_closure_sha256 = "a625715ca60dcf7c1c9f14b063fd20152a36e46b82c5a8494273c45049cea638" scope = "Unsigned, byte-string, and text fact values, including every cross-type pair." residual_assumptions = [ "Lean's kernel, the pinned Rust/Charon/Aeneas/Lean toolchain, the reviewed transparent external bridges, the listed foundational axioms, and the theorem's explicit representation-validity premises (every compared text fits the u32 UTF-8 byte bound) are trusted.", @@ -13785,12 +13785,12 @@ sha256 = "0bb2cdcf0806b77a207ed0196f697249d394c3036758ddcf9545c63eb3f7afc7" [[claims.evidence]] kind = "mechanical-translation" artifact = "formal/qualification/aeneas/generated/model/Funs.lean" -sha256 = "3836a626ec93077801d41fbf8e11e3086fc5b416af668c488710ab0717c66c92" +sha256 = "aa3f5bf6211f243c8cf937f08bddda0bc5f6219d935bd9a67c9214bb1799f598" [[claims.evidence]] kind = "source-closure" artifact = "formal/qualification/aeneas/source-closure.json" -sha256 = "047b34bfe6deab4196c24256f55987245376abc6ddf57a4de8df1212c73bfec9" +sha256 = "c9eeba1225594d6dba4da1f0fc803480c0384b9c39c27b5ad1257012dd9fe9d0" [[claims]] claim_id = "AP-FORMAL-RICH-192" @@ -13846,7 +13846,7 @@ semantic_source_closure = [ "formal/qualification/aeneas/generated/model/FunsExternal.lean", "formal/qualification/aeneas/generated/model/Types.lean", ] -semantic_source_closure_sha256 = "1a9d3309c0f56c88f64aa0d60d4048d93f6ae0da6336af00d09f342294e9b249" +semantic_source_closure_sha256 = "a625715ca60dcf7c1c9f14b063fd20152a36e46b82c5a8494273c45049cea638" scope = "The inclusive u64 range test on an observed unsigned value." residual_assumptions = [ "Lean's kernel, the pinned Rust/Charon/Aeneas/Lean toolchain, the reviewed transparent external bridges, the listed foundational axioms, and the theorem's explicit representation-validity premises (every compared text fits the u32 UTF-8 byte bound) are trusted.", @@ -13866,12 +13866,12 @@ sha256 = "0bb2cdcf0806b77a207ed0196f697249d394c3036758ddcf9545c63eb3f7afc7" [[claims.evidence]] kind = "mechanical-translation" artifact = "formal/qualification/aeneas/generated/model/Funs.lean" -sha256 = "3836a626ec93077801d41fbf8e11e3086fc5b416af668c488710ab0717c66c92" +sha256 = "aa3f5bf6211f243c8cf937f08bddda0bc5f6219d935bd9a67c9214bb1799f598" [[claims.evidence]] kind = "source-closure" artifact = "formal/qualification/aeneas/source-closure.json" -sha256 = "047b34bfe6deab4196c24256f55987245376abc6ddf57a4de8df1212c73bfec9" +sha256 = "c9eeba1225594d6dba4da1f0fc803480c0384b9c39c27b5ad1257012dd9fe9d0" [[claims]] claim_id = "AP-FORMAL-RICH-193" @@ -13930,7 +13930,7 @@ semantic_source_closure = [ "formal/qualification/aeneas/generated/model/FunsExternal.lean", "formal/qualification/aeneas/generated/model/Types.lean", ] -semantic_source_closure_sha256 = "1a9d3309c0f56c88f64aa0d60d4048d93f6ae0da6336af00d09f342294e9b249" +semantic_source_closure_sha256 = "a625715ca60dcf7c1c9f14b063fd20152a36e46b82c5a8494273c45049cea638" scope = "The terminating scan of a finite literal list for an observed fact value." residual_assumptions = [ "Lean's kernel, the pinned Rust/Charon/Aeneas/Lean toolchain, the reviewed transparent external bridges, the listed foundational axioms, and the theorem's explicit representation-validity premises (every compared text fits the u32 UTF-8 byte bound) are trusted.", @@ -13951,12 +13951,12 @@ sha256 = "0bb2cdcf0806b77a207ed0196f697249d394c3036758ddcf9545c63eb3f7afc7" [[claims.evidence]] kind = "mechanical-translation" artifact = "formal/qualification/aeneas/generated/model/Funs.lean" -sha256 = "3836a626ec93077801d41fbf8e11e3086fc5b416af668c488710ab0717c66c92" +sha256 = "aa3f5bf6211f243c8cf937f08bddda0bc5f6219d935bd9a67c9214bb1799f598" [[claims.evidence]] kind = "source-closure" artifact = "formal/qualification/aeneas/source-closure.json" -sha256 = "047b34bfe6deab4196c24256f55987245376abc6ddf57a4de8df1212c73bfec9" +sha256 = "c9eeba1225594d6dba4da1f0fc803480c0384b9c39c27b5ad1257012dd9fe9d0" [[claims]] claim_id = "AP-FORMAL-RICH-194" @@ -14015,7 +14015,7 @@ semantic_source_closure = [ "formal/qualification/aeneas/generated/model/FunsExternal.lean", "formal/qualification/aeneas/generated/model/Types.lean", ] -semantic_source_closure_sha256 = "1a9d3309c0f56c88f64aa0d60d4048d93f6ae0da6336af00d09f342294e9b249" +semantic_source_closure_sha256 = "a625715ca60dcf7c1c9f14b063fd20152a36e46b82c5a8494273c45049cea638" scope = "The terminating first-match scan of an observation's facts by name." residual_assumptions = [ "Lean's kernel, the pinned Rust/Charon/Aeneas/Lean toolchain, the reviewed transparent external bridges, the listed foundational axioms, and the theorem's explicit representation-validity premises (every compared text fits the u32 UTF-8 byte bound) are trusted.", @@ -14036,12 +14036,12 @@ sha256 = "0bb2cdcf0806b77a207ed0196f697249d394c3036758ddcf9545c63eb3f7afc7" [[claims.evidence]] kind = "mechanical-translation" artifact = "formal/qualification/aeneas/generated/model/Funs.lean" -sha256 = "3836a626ec93077801d41fbf8e11e3086fc5b416af668c488710ab0717c66c92" +sha256 = "aa3f5bf6211f243c8cf937f08bddda0bc5f6219d935bd9a67c9214bb1799f598" [[claims.evidence]] kind = "source-closure" artifact = "formal/qualification/aeneas/source-closure.json" -sha256 = "047b34bfe6deab4196c24256f55987245376abc6ddf57a4de8df1212c73bfec9" +sha256 = "c9eeba1225594d6dba4da1f0fc803480c0384b9c39c27b5ad1257012dd9fe9d0" [[claims]] claim_id = "AP-FORMAL-RICH-195" @@ -14102,7 +14102,7 @@ semantic_source_closure = [ "formal/qualification/aeneas/generated/model/FunsExternal.lean", "formal/qualification/aeneas/generated/model/Types.lean", ] -semantic_source_closure_sha256 = "1a9d3309c0f56c88f64aa0d60d4048d93f6ae0da6336af00d09f342294e9b249" +semantic_source_closure_sha256 = "a625715ca60dcf7c1c9f14b063fd20152a36e46b82c5a8494273c45049cea638" scope = "All four condition atoms against a present or absent observed value and a present or absent action value." residual_assumptions = [ "Lean's kernel, the pinned Rust/Charon/Aeneas/Lean toolchain, the reviewed transparent external bridges, the listed foundational axioms, and the theorem's explicit representation-validity premises (every compared text fits the u32 UTF-8 byte bound) are trusted.", @@ -14123,12 +14123,12 @@ sha256 = "0bb2cdcf0806b77a207ed0196f697249d394c3036758ddcf9545c63eb3f7afc7" [[claims.evidence]] kind = "mechanical-translation" artifact = "formal/qualification/aeneas/generated/model/Funs.lean" -sha256 = "3836a626ec93077801d41fbf8e11e3086fc5b416af668c488710ab0717c66c92" +sha256 = "aa3f5bf6211f243c8cf937f08bddda0bc5f6219d935bd9a67c9214bb1799f598" [[claims.evidence]] kind = "source-closure" artifact = "formal/qualification/aeneas/source-closure.json" -sha256 = "047b34bfe6deab4196c24256f55987245376abc6ddf57a4de8df1212c73bfec9" +sha256 = "c9eeba1225594d6dba4da1f0fc803480c0384b9c39c27b5ad1257012dd9fe9d0" [[claims]] claim_id = "AP-FORMAL-RICH-196" @@ -14192,7 +14192,7 @@ semantic_source_closure = [ "formal/qualification/aeneas/generated/model/FunsExternal.lean", "formal/qualification/aeneas/generated/model/Types.lean", ] -semantic_source_closure_sha256 = "1a9d3309c0f56c88f64aa0d60d4048d93f6ae0da6336af00d09f342294e9b249" +semantic_source_closure_sha256 = "a625715ca60dcf7c1c9f14b063fd20152a36e46b82c5a8494273c45049cea638" scope = "One named condition over an observation's facts with its supplied action value." residual_assumptions = [ "Lean's kernel, the pinned Rust/Charon/Aeneas/Lean toolchain, the reviewed transparent external bridges, the listed foundational axioms, and the theorem's explicit representation-validity premises (every compared text fits the u32 UTF-8 byte bound) are trusted.", @@ -14213,12 +14213,12 @@ sha256 = "0bb2cdcf0806b77a207ed0196f697249d394c3036758ddcf9545c63eb3f7afc7" [[claims.evidence]] kind = "mechanical-translation" artifact = "formal/qualification/aeneas/generated/model/Funs.lean" -sha256 = "3836a626ec93077801d41fbf8e11e3086fc5b416af668c488710ab0717c66c92" +sha256 = "aa3f5bf6211f243c8cf937f08bddda0bc5f6219d935bd9a67c9214bb1799f598" [[claims.evidence]] kind = "source-closure" artifact = "formal/qualification/aeneas/source-closure.json" -sha256 = "047b34bfe6deab4196c24256f55987245376abc6ddf57a4de8df1212c73bfec9" +sha256 = "c9eeba1225594d6dba4da1f0fc803480c0384b9c39c27b5ad1257012dd9fe9d0" [[claims]] claim_id = "AP-FORMAL-RICH-197" @@ -14283,7 +14283,7 @@ semantic_source_closure = [ "formal/qualification/aeneas/generated/model/FunsExternal.lean", "formal/qualification/aeneas/generated/model/Types.lean", ] -semantic_source_closure_sha256 = "1a9d3309c0f56c88f64aa0d60d4048d93f6ae0da6336af00d09f342294e9b249" +semantic_source_closure_sha256 = "a625715ca60dcf7c1c9f14b063fd20152a36e46b82c5a8494273c45049cea638" scope = "The terminating conjunction loop over a condition slice and a parallel action-value slice." residual_assumptions = [ "Lean's kernel, the pinned Rust/Charon/Aeneas/Lean toolchain, the reviewed transparent external bridges, the listed foundational axioms, and the theorem's explicit representation-validity premises (every compared text fits the u32 UTF-8 byte bound) are trusted.", @@ -14304,12 +14304,12 @@ sha256 = "0bb2cdcf0806b77a207ed0196f697249d394c3036758ddcf9545c63eb3f7afc7" [[claims.evidence]] kind = "mechanical-translation" artifact = "formal/qualification/aeneas/generated/model/Funs.lean" -sha256 = "3836a626ec93077801d41fbf8e11e3086fc5b416af668c488710ab0717c66c92" +sha256 = "aa3f5bf6211f243c8cf937f08bddda0bc5f6219d935bd9a67c9214bb1799f598" [[claims.evidence]] kind = "source-closure" artifact = "formal/qualification/aeneas/source-closure.json" -sha256 = "047b34bfe6deab4196c24256f55987245376abc6ddf57a4de8df1212c73bfec9" +sha256 = "c9eeba1225594d6dba4da1f0fc803480c0384b9c39c27b5ad1257012dd9fe9d0" [[claims]] claim_id = "AP-FORMAL-RICH-198" @@ -14365,7 +14365,7 @@ semantic_source_closure = [ "formal/qualification/aeneas/generated/model/FunsExternal.lean", "formal/qualification/aeneas/generated/model/Types.lean", ] -semantic_source_closure_sha256 = "1a9d3309c0f56c88f64aa0d60d4048d93f6ae0da6336af00d09f342294e9b249" +semantic_source_closure_sha256 = "a625715ca60dcf7c1c9f14b063fd20152a36e46b82c5a8494273c45049cea638" scope = "The length guard that precedes every condition evaluation." residual_assumptions = [ "Lean's kernel, the pinned Rust/Charon/Aeneas/Lean toolchain, the reviewed transparent external bridges, the listed foundational axioms, and the theorem's explicit representation-validity premises (every compared text fits the u32 UTF-8 byte bound) are trusted.", @@ -14386,12 +14386,12 @@ sha256 = "0bb2cdcf0806b77a207ed0196f697249d394c3036758ddcf9545c63eb3f7afc7" [[claims.evidence]] kind = "mechanical-translation" artifact = "formal/qualification/aeneas/generated/model/Funs.lean" -sha256 = "3836a626ec93077801d41fbf8e11e3086fc5b416af668c488710ab0717c66c92" +sha256 = "aa3f5bf6211f243c8cf937f08bddda0bc5f6219d935bd9a67c9214bb1799f598" [[claims.evidence]] kind = "source-closure" artifact = "formal/qualification/aeneas/source-closure.json" -sha256 = "047b34bfe6deab4196c24256f55987245376abc6ddf57a4de8df1212c73bfec9" +sha256 = "c9eeba1225594d6dba4da1f0fc803480c0384b9c39c27b5ad1257012dd9fe9d0" [[claims]] claim_id = "AP-FORMAL-RICH-199" @@ -14456,7 +14456,7 @@ semantic_source_closure = [ "formal/qualification/aeneas/generated/model/FunsExternal.lean", "formal/qualification/aeneas/generated/model/Types.lean", ] -semantic_source_closure_sha256 = "1a9d3309c0f56c88f64aa0d60d4048d93f6ae0da6336af00d09f342294e9b249" +semantic_source_closure_sha256 = "a625715ca60dcf7c1c9f14b063fd20152a36e46b82c5a8494273c45049cea638" scope = "The conjunction loop when each eqAction condition's supplied action value is the environment's action fact for its reference." residual_assumptions = [ "Lean's kernel, the pinned Rust/Charon/Aeneas/Lean toolchain, the reviewed transparent external bridges, the listed foundational axioms, and the theorem's explicit representation-validity premises (every compared text fits the u32 UTF-8 byte bound) are trusted.", @@ -14477,12 +14477,12 @@ sha256 = "0bb2cdcf0806b77a207ed0196f697249d394c3036758ddcf9545c63eb3f7afc7" [[claims.evidence]] kind = "mechanical-translation" artifact = "formal/qualification/aeneas/generated/model/Funs.lean" -sha256 = "3836a626ec93077801d41fbf8e11e3086fc5b416af668c488710ab0717c66c92" +sha256 = "aa3f5bf6211f243c8cf937f08bddda0bc5f6219d935bd9a67c9214bb1799f598" [[claims.evidence]] kind = "source-closure" artifact = "formal/qualification/aeneas/source-closure.json" -sha256 = "047b34bfe6deab4196c24256f55987245376abc6ddf57a4de8df1212c73bfec9" +sha256 = "c9eeba1225594d6dba4da1f0fc803480c0384b9c39c27b5ad1257012dd9fe9d0" [[claims]] claim_id = "AP-FORMAL-RICH-200" @@ -14538,7 +14538,7 @@ semantic_source_closure = [ "formal/qualification/aeneas/generated/model/FunsExternal.lean", "formal/qualification/aeneas/generated/model/Types.lean", ] -semantic_source_closure_sha256 = "1a9d3309c0f56c88f64aa0d60d4048d93f6ae0da6336af00d09f342294e9b249" +semantic_source_closure_sha256 = "a625715ca60dcf7c1c9f14b063fd20152a36e46b82c5a8494273c45049cea638" scope = "Satisfied before denied before indeterminate, for every pair of eligibility and satisfaction inputs." residual_assumptions = [ "Lean's kernel, the pinned Rust/Charon/Aeneas/Lean toolchain, the reviewed transparent external bridges, the listed foundational axioms, and the theorem's explicit representation-validity premises (every compared text fits the u32 UTF-8 byte bound) are trusted.", @@ -14558,12 +14558,12 @@ sha256 = "0bb2cdcf0806b77a207ed0196f697249d394c3036758ddcf9545c63eb3f7afc7" [[claims.evidence]] kind = "mechanical-translation" artifact = "formal/qualification/aeneas/generated/model/Funs.lean" -sha256 = "3836a626ec93077801d41fbf8e11e3086fc5b416af668c488710ab0717c66c92" +sha256 = "aa3f5bf6211f243c8cf937f08bddda0bc5f6219d935bd9a67c9214bb1799f598" [[claims.evidence]] kind = "source-closure" artifact = "formal/qualification/aeneas/source-closure.json" -sha256 = "047b34bfe6deab4196c24256f55987245376abc6ddf57a4de8df1212c73bfec9" +sha256 = "c9eeba1225594d6dba4da1f0fc803480c0384b9c39c27b5ad1257012dd9fe9d0" [[claims]] claim_id = "AP-FORMAL-RICH-201" @@ -14619,7 +14619,7 @@ semantic_source_closure = [ "formal/qualification/aeneas/generated/model/FunsExternal.lean", "formal/qualification/aeneas/generated/model/Types.lean", ] -semantic_source_closure_sha256 = "1a9d3309c0f56c88f64aa0d60d4048d93f6ae0da6336af00d09f342294e9b249" +semantic_source_closure_sha256 = "a625715ca60dcf7c1c9f14b063fd20152a36e46b82c5a8494273c45049cea638" scope = "The per-requirement verdict when the requirement's action facts are available; unavailable action facts are indeterminate in the model." residual_assumptions = [ "Lean's kernel, the pinned Rust/Charon/Aeneas/Lean toolchain, the reviewed transparent external bridges, the listed foundational axioms, and the theorem's explicit representation-validity premises (every compared text fits the u32 UTF-8 byte bound) are trusted.", @@ -14639,9 +14639,9 @@ sha256 = "0bb2cdcf0806b77a207ed0196f697249d394c3036758ddcf9545c63eb3f7afc7" [[claims.evidence]] kind = "mechanical-translation" artifact = "formal/qualification/aeneas/generated/model/Funs.lean" -sha256 = "3836a626ec93077801d41fbf8e11e3086fc5b416af668c488710ab0717c66c92" +sha256 = "aa3f5bf6211f243c8cf937f08bddda0bc5f6219d935bd9a67c9214bb1799f598" [[claims.evidence]] kind = "source-closure" artifact = "formal/qualification/aeneas/source-closure.json" -sha256 = "047b34bfe6deab4196c24256f55987245376abc6ddf57a4de8df1212c73bfec9" +sha256 = "c9eeba1225594d6dba4da1f0fc803480c0384b9c39c27b5ad1257012dd9fe9d0" diff --git a/formal/qualification/aeneas/source-closure.json b/formal/qualification/aeneas/source-closure.json index e68aa457b..87fd3416e 100644 --- a/formal/qualification/aeneas/source-closure.json +++ b/formal/qualification/aeneas/source-closure.json @@ -1,6 +1,6 @@ { "schema": "auths-proof-translation-source-closure/v2", - "digest": "0e664f3680d5c746ccf37bf25fa5297b94a78a1ff23b5c1673bfbf885fbbdf95", + "digest": "e2686c422e4a94498a2581533e98ecd16efa16d6085cce13277147e4646e3c0a", "files": [ { "path": ".cargo/config.toml", @@ -261,7 +261,7 @@ }, { "path": "xtask/src/formal_qualification.rs", - "sha256": "6626830bb4b2ab417a77c7891621431404d1d9002a5257267e987e52403205bc" + "sha256": "f59d82bdb3ea7b9e7f8751b2c95e9ae0b57edd61a1e06ac3782ac7313995410f" }, { "path": "xtask/src/fuzz.rs", diff --git a/release/semantic-freeze-versions.toml b/release/semantic-freeze-versions.toml index 76b674a5a..02c35684f 100644 --- a/release/semantic-freeze-versions.toml +++ b/release/semantic-freeze-versions.toml @@ -1,4 +1,4 @@ -freeze_version = 313 +freeze_version = 314 # Semantic identity counters live outside the xtask source tree deliberately. # The formal source closure binds xtask's executable code, while the semantic @@ -16,10 +16,10 @@ freeze_version = 313 "auths.frozen-bytes/core/fixtures/v1/manifest.json" = 12 "auths.frozen-bytes/core/formal-vectors/v1/manifest.json" = 1 "auths.frozen-bytes/demos/benchmarks/profiles/release.toml" = 1 -"auths.frozen-bytes/formal/assurance-manifest-v1.toml" = 34 +"auths.frozen-bytes/formal/assurance-manifest-v1.toml" = 35 "auths.frozen-bytes/formal/qualification/aeneas/generated" = 13 "auths.frozen-bytes/formal/qualification/aeneas/qualification.toml" = 9 -"auths.frozen-bytes/formal/qualification/aeneas/source-closure.json" = 73 +"auths.frozen-bytes/formal/qualification/aeneas/source-closure.json" = 74 "auths.frozen-bytes/product/conformance/v1/mechanism-profile-conformance.json" = 1 "auths.frozen-bytes/product/conformance/v1/simplified-product-waist.json" = 3 "auths.frozen-bytes/product/fixtures/v1/bounded-policy/manifest.json" = 3 @@ -67,5 +67,5 @@ freeze_version = 313 "auths.product.simplified-waist" = 17 "auths.product.vocabulary" = 19 "auths.release.benchmark-contract" = 1 -"auths.release.evolution-contract" = 71 -"auths.release.public-surface" = 313 +"auths.release.evolution-contract" = 72 +"auths.release.public-surface" = 314 diff --git a/release/semantic-freeze.json b/release/semantic-freeze.json index 247e167ff..8ce0389c0 100644 --- a/release/semantic-freeze.json +++ b/release/semantic-freeze.json @@ -1,6 +1,6 @@ { "schema": "auths.semantic-freeze/1", - "freezeVersion": 313, + "freezeVersion": 314, "publicSurface": { "rustRoots": [ "auths", @@ -202,7 +202,7 @@ }, { "id": "auths.frozen-bytes/formal/assurance-manifest-v1.toml", - "version": 34, + "version": 35, "classification": "frozen-bytes", "categories": [ "canonical-generated-evidence" @@ -210,7 +210,7 @@ "owners": [ "formal/assurance-manifest-v1.toml" ], - "sha256": "3d73918fdcd465bedca33aa2522fbf8d805a3ac2db333e39e566f91fea22fd7a" + "sha256": "a4d0ac9b42fe674a5a8a4b4790c685c4d94f610b464f60bbbaed45d00e3cff37" }, { "id": "auths.frozen-bytes/formal/qualification/aeneas/generated", @@ -238,7 +238,7 @@ }, { "id": "auths.frozen-bytes/formal/qualification/aeneas/source-closure.json", - "version": 73, + "version": 74, "classification": "frozen-bytes", "categories": [ "canonical-generated-evidence" @@ -246,7 +246,7 @@ "owners": [ "formal/qualification/aeneas/source-closure.json" ], - "sha256": "f01cc696539553634f0054b0b0db79c2276e82023b825c5e07746cab3026962d" + "sha256": "e70c13dec2ac739a275e09019dea174836c1999fea240c0227d7d5a010997a3b" }, { "id": "auths.frozen-bytes/product/conformance/v1/mechanism-profile-conformance.json", @@ -1019,7 +1019,7 @@ }, { "id": "auths.release.evolution-contract", - "version": 71, + "version": 72, "classification": "frozen-meaning", "categories": [ "version-axes", @@ -1040,11 +1040,11 @@ "release/fixtures/evolution", "xtask/src/evolution_policy.rs" ], - "sha256": "d66e42635ada8a97eb3aa166ee4d9a30e4cc0f95a22754b99f6cb1829276d2a9" + "sha256": "af222ac2b5d7babff65db5b64ae4181233ff41e4ff21b1bcf7e0b3f77574d9cb" }, { "id": "auths.release.public-surface", - "version": 313, + "version": 314, "classification": "release-metadata", "categories": [ "package-names", @@ -1136,7 +1136,7 @@ "xtask/src/release_control.rs", "xtask/src/semantic_freeze.rs" ], - "sha256": "306bac86083c1d8b885c1590dd73cfa12cc8493b22c4763a7db59bb7c009cefd" + "sha256": "6b1fb2f6624f97fcab96b44d396859cf2fda926638aded71e76ca1d8015641dc" } ] } diff --git a/xtask/src/formal_qualification.rs b/xtask/src/formal_qualification.rs index 4d2c2df65..b2394df0b 100644 --- a/xtask/src/formal_qualification.rs +++ b/xtask/src/formal_qualification.rs @@ -1388,6 +1388,7 @@ fn validate_ci_workflow_gates(ci: &str) -> Result<(), String> { .to_owned(), ); } + validate_translation_evidence_selection(formal_job)?; for job_name in [ "authoritative-run", "compliance-run", @@ -1477,6 +1478,70 @@ fn validate_ci_workflow_gates(ci: &str) -> Result<(), String> { Ok(()) } +/// Condition of every step on the two-reproduction path: it runs unless a +/// reuse step located evidence, so a cold plan, a same-PR miss, and absent +/// protected-base evidence all reach it. +const TRANSLATION_REPRODUCTION_CONDITION: &str = "steps.prior-pr-translation.outputs.reused != 'true' && steps.protected-base-translation.outputs.found != 'true'"; + +/// Protected-base evidence is an optimization, never a precondition. The base +/// commit's run may have failed in another job, been cancelled by a newer +/// push, still be running, or have expired; the job then executes the same two +/// clean reproductions as a cold plan. A pull-request reproduction runs in +/// update mode and rewrites drifted outputs in place, so the packaging step +/// must share its condition, or drift would qualify instead of stopping the +/// job. Located evidence is reused only through the binding step, whose +/// failure fails the job rather than falling back. +fn validate_translation_evidence_selection(job: &str) -> Result<(), String> { + let locate = workflow_step_source(job, "Locate protected-base translation evidence")?; + let bind = workflow_step_source(job, "Verify and bind protected-base translation evidence")?; + let reproduce = workflow_step_source(job, "Reproduce translation twice")?; + let package = workflow_step_source(job, "Package a bounded translation update")?; + if !locate.contains("- id: protected-base-translation\n") + || !bind.contains("\n if: steps.protected-base-translation.outputs.found == 'true'\n") + || !reproduce.contains(&format!( + "\n if: {TRANSLATION_REPRODUCTION_CONDITION}\n" + )) + || !package.contains(&format!( + "\n if: github.event_name == 'pull_request' && {TRANSLATION_REPRODUCTION_CONDITION}\n" + )) + { + return Err( + "hosted translation must reuse protected-base evidence only once located and bound, and otherwise execute two clean reproductions that package generated drift" + .to_owned(), + ); + } + Ok(()) +} + +/// One step of a workflow job, from its list marker to the next step's, so a +/// condition is read from the step it gates rather than from anywhere in the +/// job. +fn workflow_step_source<'a>(job: &'a str, step_name: &str) -> Result<&'a str, String> { + let name = format!("name: {step_name}"); + let starts: Vec<_> = job + .match_indices("\n - ") + .map(|(index, _)| index) + .collect(); + let ends = starts + .iter() + .skip(1) + .copied() + .chain(std::iter::once(job.len())); + starts + .iter() + .copied() + .zip(ends) + .map(|(start, end)| &job[start..end]) + .find(|step| { + step.lines().any(|line| { + line.strip_prefix(" - ") + .or_else(|| line.strip_prefix(" ")) + == Some(name.as_str()) + }) + }) + .ok_or_else(|| format!("hosted CI omits the `{step_name}` step")) +} + fn workflow_job_source<'a>(workflow: &'a str, job_name: &str) -> Result<&'a str, String> { let marker = format!("\n {job_name}:"); let tail = workflow @@ -2253,12 +2318,24 @@ cargo xtask ci formal-proof-fast needs: [ci-plan, formal-update-gate, repository-preflight] needs.repository-preflight.result == 'success' compiler-cache: "false" -AUTHS_FORMAL_UPDATE_MODE -formal-update-artifact create -Preserve the bounded translation update -Stop qualification until generated translation is committed -cargo xtask ci formal-translation-reproduce -cargo xtask ci formal-translation-reuse + - id: protected-base-translation + name: Locate protected-base translation evidence + if: needs.ci-plan.outputs.formal_cold_required != 'true' + run: echo 'found=false' >> "$GITHUB_OUTPUT" + - name: Verify and bind protected-base translation evidence + if: steps.protected-base-translation.outputs.found == 'true' + run: cargo xtask ci formal-translation-reuse + - name: Reproduce translation twice + if: steps.prior-pr-translation.outputs.reused != 'true' && steps.protected-base-translation.outputs.found != 'true' + env: + AUTHS_FORMAL_UPDATE_MODE: ${{ github.event_name == 'pull_request' && 'true' || 'false' }} + run: cargo xtask ci formal-translation-reproduce + - id: formal-update + name: Package a bounded translation update + if: github.event_name == 'pull_request' && steps.prior-pr-translation.outputs.reused != 'true' && steps.protected-base-translation.outputs.found != 'true' + run: cargo run --locked -p auths-ci-plan -- formal-update-artifact create + - name: Preserve the bounded translation update + - name: Stop qualification until generated translation is committed formal-kani-run: needs: [ci-plan, formal-update-gate, repository-preflight] needs.repository-preflight.result == 'success' @@ -2337,6 +2414,47 @@ needs.formal-kani.result validate_ci_workflow_gates(CI_GATES).expect("hosted CI gates must satisfy formal policy"); } + #[test] + fn committed_hosted_ci_satisfies_formal_policy() { + validate_ci_workflow_gates(include_str!("../../.github/workflows/ci.yml")) + .expect("the committed hosted CI workflow must satisfy formal policy"); + } + + #[test] + fn missing_protected_base_evidence_executes_two_clean_reproductions() { + let base_run_required = CI_GATES.replace( + "name: Reproduce translation twice\n if: steps.prior-pr-translation.outputs.reused != 'true' && steps.protected-base-translation.outputs.found != 'true'\n", + "name: Reproduce translation twice\n if: needs.ci-plan.outputs.formal_cold_required == 'true' && steps.prior-pr-translation.outputs.reused != 'true'\n", + ); + let error = validate_ci_workflow_gates(&base_run_required).expect_err( + "a base commit without successful CI must not fail every pull request on it", + ); + assert!(error.contains("otherwise execute two clean reproductions")); + } + + #[test] + fn every_update_mode_reproduction_packages_its_drift() { + let unpackaged = CI_GATES.replace( + "if: github.event_name == 'pull_request' && steps.prior-pr-translation.outputs.reused != 'true' && steps.protected-base-translation.outputs.found != 'true'\n", + "if: github.event_name == 'pull_request' && needs.ci-plan.outputs.formal_cold_required == 'true' && steps.prior-pr-translation.outputs.reused != 'true'\n", + ); + let error = validate_ci_workflow_gates(&unpackaged).expect_err( + "a fallback reproduction that rewrote drifted outputs must still stop the job", + ); + assert!(error.contains("that package generated drift")); + } + + #[test] + fn protected_base_reuse_requires_located_evidence() { + let unlocated = CI_GATES.replace( + "if: steps.protected-base-translation.outputs.found == 'true'\n", + "if: needs.ci-plan.outputs.formal_cold_required != 'true'\n", + ); + let error = validate_ci_workflow_gates(&unlocated) + .expect_err("binding must not run when no evidence was located"); + assert!(error.contains("only once located and bound")); + } + #[test] fn hosted_ci_cannot_omit_pinned_lean_setup() { let error = validate_ci_workflow_gates(