phase 1.4.2: deepen spool protected resource semantics - #30
Conversation
📝 WalkthroughWalkthroughPhase 1.4.2 introduces Dafny formal verification for SpoolEntry as a protected resource with access-control predicates, audit-linkage lemmas, and fail-closed behavior guarantees. Supporting test fixtures, golden outputs, validation scripts, and documentation updates reflect the completion of 206 verified Dafny modules (up from 184). ChangesSpool Protected-Resource Formal Verification and Testing
Sequence DiagramThe changes do not satisfy the conditions for sequence diagram generation; they primarily constitute formal verification infrastructure, test data, validation logic, and documentation updates without novel multi-component interaction flows suitable for visualization. Estimated code review effort🎯 4 (Complex) | ⏱️ ~60 minutes 🚥 Pre-merge checks | ✅ 4 | ❌ 1❌ Failed checks (1 warning)
✅ Passed checks (4 passed)
✏️ Tip: You can configure your own custom pre-merge checks in the settings. ✨ Finishing Touches📝 Generate docstrings
🧪 Generate unit tests (beta)
Thanks for using CodeRabbit! It's free for OSS, and your support helps us grow. If you like it, consider giving us a shout-out. Comment |
|
@coderabbitai review |
✅ Actions performedReview triggered.
|
![coderabbitai[bot]](https://avatars.githubusercontent.com/in/347564?s=60&v=4){kind=small}
There was a problem hiding this comment.
Actionable comments posted: 10
Caution
Some comments are outside the diff and can’t be posted inline due to platform limitations.
⚠️ Outside diff range comments (2)
tests/fixtures/job/spool-browse-nonowner-0913.yml (1)
36-38:⚠️ Potential issue | 🟡 Minor | ⚡ Quick winUse scenario-specific input ID/seed for 0913.
Line 36 and Line 38 still reference Phase09 values. Keeping these stale IDs in a Phase142 fixture reduces artifact clarity and can introduce duplicate identifiers across spool scenarios.
Suggested fix
inputs: -- input_id: INPUT-MFOS-PHASE09-0001 +- input_id: INPUT-MFOS-SPOOL-BROWSE-NONOWNER-0913 operation: SPOOL-BROWSE-NONOWNER - deterministic_seed: SEED-MFOS-PHASE09-0001 + deterministic_seed: SEED-MFOS-PHASE142-0913🤖 Prompt for AI Agents
Verify each finding against the current code and only fix it if needed. In `@tests/fixtures/job/spool-browse-nonowner-0913.yml` around lines 36 - 38, The fixture still uses Phase09 identifiers; update the input_id and deterministic_seed fields in the SPOOL-BROWSE-NONOWNER fixture so they are scenario-specific for 0913 (e.g., rename input_id from INPUT-MFOS-PHASE09-0001 to a unique INPUT-MFOS-PHASE142-0913-0001 and rename deterministic_seed from SEED-MFOS-PHASE09-0001 to SEED-MFOS-PHASE142-0913-0001), ensuring the new values are unique across spool fixtures and reflect the 0913 scenario.tests/fixtures/job/spool-browse-owner-0912.yml (1)
34-36:⚠️ Potential issue | 🟡 Minor | ⚡ Quick winAlign input identifiers to the 0912 / Phase 1.4.2 scenario.
Line 34 and Line 36 still carry Phase09 identifiers while this fixture has been migrated to Phase142 resource IDs. This weakens traceability and can cause ID collisions in tooling.
Suggested fix
inputs: -- input_id: INPUT-MFOS-PHASE09-0001 +- input_id: INPUT-MFOS-SPOOL-BROWSE-OWNER-0912 operation: SPOOL-BROWSE-OWNER - deterministic_seed: SEED-MFOS-PHASE09-0001 + deterministic_seed: SEED-MFOS-PHASE142-0912🤖 Prompt for AI Agents
Verify each finding against the current code and only fix it if needed. In `@tests/fixtures/job/spool-browse-owner-0912.yml` around lines 34 - 36, The fixture's identifiers still reference Phase09; update the values of input_id and deterministic_seed (currently "INPUT-MFOS-PHASE09-0001" and "SEED-MFOS-PHASE09-0001") to the correct 0912 / Phase 1.4.2 resource IDs used across this fixture set (replace the "PHASE09" segment with the Phase142/0912 identifier scheme used in this migration) so they match the scenario naming convention and avoid collisions.
🤖 Prompt for all review comments with AI agents
Verify each finding against the current code and only fix it if needed.
Inline comments:
In `@reports/phases/phase-1-4/spool-protected-resource/coverage-report.md`:
- Around line 5-27: The Phase 1.4 content in coverage-report.md is publishing
generated traceability and concrete C5 rows as if they are implemented; change
this to planning-only by: update the header and the "Generated traceability
lives under `evidence/traceability/generated/phase-1-4-2/`" line to indicate
"planning-only / draft" (or move the generated artifacts behind an explicit
implementation gate), and mark the Coverage Summary and each C5 scenario row
(e.g., entries like `spool-browse-owner-0912`, `spool-purge-denied-0914`,
`spool-evidence-not-audit-0916`) as planning intent rather than concrete
verification (or remove them from published paths) so Phase 1.4 artifacts are
not treated as implemented until an explicit reviewed implementation gate flips
scope.
In `@reports/phases/phase-1-4/spool-protected-resource/red-team-review.md`:
- Around line 12-26: Reword the assertions in the block starting with "Spool
browse without authorization is blocked..." (lines 12–26) so they read as
planned/targeted semantics rather than implementation guarantees: prepend or
replace phrasing with qualifiers like "planned to be", "intended to", or
"expected to" (or reference an explicit Phase 1.4 scope-change/entry-exit gate)
for each bullet (e.g., "Spool browse without authorization is planned to be
blocked"); ensure consistency across all bullets and retain the residual-risk
framing unchanged.
In `@reports/phases/phase-1-4/spool-protected-resource/report.md`:
- Around line 33-37: Remove the implementation-traceability specifics from the
Phase 1.4 planning report: delete the reference to the generated evidence path
"evidence/traceability/generated/phase-1-4-2/" and any asserted C5 claim
language (mentions of C5 being claimed "only for rows with fixture, embedded
oracle, and golden-vector links"); instead replace with a planning-scoped
statement clarifying Phase 1.4 is planning-only and that implementation
traceability and hosted/service behavior will be addressed in a later
implementation gate. Ensure the edited paragraph in report.md no longer reads
like implementation status or lists generated artifacts.
In `@reports/phases/phase-1-4/spool-protected-resource/validation-report.md`:
- Around line 22-23: Update the two occurrences of the spool coverage checker
command in the report so they use the canonical validator path used by the
pipeline; replace any `python3 scripts/check-phase1-4-2-spool-coverage.py`
references with the canonical `python3
scripts/phases/phase-1/check-phase1-4-2-spool-coverage.py` in both command lists
mentioned in the document (the entries around the spool coverage checks),
ensuring the report commands match the validator's `scripts/validate-all.sh`
invocation.
In `@scripts/checks/semantic-coverage/check-semantic-coverage-mapping.py`:
- Around line 111-116: The code assumes negative_failure_conditions is iterable
but it can be None; ensure negative_symbols is a list before membership checks
by normalizing it (e.g. replace None with [] right after assignment of
negative_symbols) or by guarding each membership test with an existence check;
update the block using negative_symbols, LEVEL_RANK, test_id and errors so lines
that check `"INV_AUTH_UNSUPPORTED_NOT_SUCCESS" in negative_symbols` and
`"INV_AUTH_SPEC_GAP_NOT_SUCCESS" in negative_symbols` only run against a
non-None iterable (or use negative_symbols =
test.get("negative_failure_conditions") or [] to coerce None to an empty list).
In `@scripts/generators/generate-spool-coverage.py`:
- Around line 142-153: The catalog entry linking test ID
NEG-MFOS-JOB-SPOOL-EVIDENCE-NOT-AUDIT-0916 to lemma
INV_SPOOL_EVIDENCE_NOT_AUDIT_EVIDENCE overclaims coverage because that lemma
only proves type separation, not the result-level rejection
(MFOS_ERR_INVALID_AUDIT_RECORD) expected by the catalog at the job-spool test;
update the generator mapping so this row is not mapped to
INV_SPOOL_EVIDENCE_NOT_AUDIT_EVIDENCE (either remove the mapping or mark it as
uncovered) and instead leave it unmapped until a Dafny lemma that asserts the
result-level error path exists, referencing the test ID
NEG-MFOS-JOB-SPOOL-EVIDENCE-NOT-AUDIT-0916, lemma
INV_SPOOL_EVIDENCE_NOT_AUDIT_EVIDENCE, and the catalog entry in
tests/catalog/job-spool.yml.
In `@scripts/phases/phase-1/check-phase1-4-2-spool-coverage.py`:
- Around line 297-306: The current checks iterate repository-wide paths (using
ROOT and forbidden tuples) and always fail if those directories exist anywhere;
instead restrict validation to only files/paths introduced or modified by this
phase/PR: obtain the list of changed paths (e.g., the existing
changed_files/changed_paths variable or the PR diff) and replace the
repository-wide exists() checks with tests against that list (check if any
changed path is under ROOT/"formal"/"executable-semantics"/"rust" or
ROOT/"implementation"/"services"/"jobd"/"spoold"/"operatord" and similarly if
any changed path matches reports/current/*phase-1-4-2*), appending errors only
when a forbidden path is present in the changed set; keep using the same errors
list and preserve the same error messages.
- Around line 231-243: collect_mapped_symbols currently calls load_yaml on every
file in TRACE_FILES without checking existence, causing exceptions when
traceability files are missing; change it to skip non-existent files by checking
for file presence under TRACEABILITY_DIR (use TRACEABILITY_DIR / name) before
calling load_yaml, and only attempt to parse when the file exists; keep the rest
of the logic (iterating rows, reading "coverage_mappings", using "dafny_symbol")
the same so the function still returns the symbols dict when some trace files
are absent.
In `@tests/catalog/job-spool.yml`:
- Around line 678-688: The test YAML's decision block includes ALLOW_WITH_AUDIT
with obligation AUDIT_SECURITY_DECISION but the audit flag is incorrect; update
the audit_obligation_required field from false to true so the fixture's metadata
matches the decision/obligation (ensure the audit_obligation_required value
aligns with the decisions: [{decision_id:
DECISION-MFOS-SPOOL-EVIDENCE-NOT-AUDIT-0916, result: ALLOW_WITH_AUDIT,
obligations: [AUDIT_SECURITY_DECISION]}] and final_state: FAILED).
In `@tests/fixtures/job/spool-evidence-not-audit-0916.yml`:
- Around line 27-32: The fixture's semantic_facts state spool_evidence_present
and audit_evidence_present but do not encode that an audit is required, so the
negative case lacks grounding; update the semantic_facts (same block containing
dafny_property: INV_SPOOL_EVIDENCE_NOT_AUDIT_EVIDENCE and spool_operation:
OP_EXPORT) to explicitly assert the audit obligation for this path (e.g., add an
entry like audit_obligation: ALLOW_WITH_AUDIT or audit_required: true) so the
fixture reflects that the request is on an ALLOW_WITH_AUDIT path.
---
Outside diff comments:
In `@tests/fixtures/job/spool-browse-nonowner-0913.yml`:
- Around line 36-38: The fixture still uses Phase09 identifiers; update the
input_id and deterministic_seed fields in the SPOOL-BROWSE-NONOWNER fixture so
they are scenario-specific for 0913 (e.g., rename input_id from
INPUT-MFOS-PHASE09-0001 to a unique INPUT-MFOS-PHASE142-0913-0001 and rename
deterministic_seed from SEED-MFOS-PHASE09-0001 to SEED-MFOS-PHASE142-0913-0001),
ensuring the new values are unique across spool fixtures and reflect the 0913
scenario.
In `@tests/fixtures/job/spool-browse-owner-0912.yml`:
- Around line 34-36: The fixture's identifiers still reference Phase09; update
the values of input_id and deterministic_seed (currently
"INPUT-MFOS-PHASE09-0001" and "SEED-MFOS-PHASE09-0001") to the correct 0912 /
Phase 1.4.2 resource IDs used across this fixture set (replace the "PHASE09"
segment with the Phase142/0912 identifier scheme used in this migration) so they
match the scenario naming convention and avoid collisions.
🪄 Autofix (Beta)
Fix all unresolved CodeRabbit comments on this PR:
- Push a commit to this branch (recommended)
- Create a new PR with the fixes
ℹ️ Review info
⚙️ Run configuration
Configuration used: Path: .coderabbit.yaml
Review profile: CHILL
Plan: Pro
Run ID: 98298f43-d5e7-48f0-ab31-c176be2d9f27
⛔ Files ignored due to path filters (9)
evidence/traceability/generated/phase-1-4-2/coverage-summary.ymlis excluded by!**/generated/**evidence/traceability/generated/phase-1-4-2/fixture-to-dafny.ymlis excluded by!**/generated/**evidence/traceability/generated/phase-1-4-2/formal-claim-to-dafny.ymlis excluded by!**/generated/**evidence/traceability/generated/phase-1-4-2/requirement-to-dafny.ymlis excluded by!**/generated/**evidence/traceability/generated/phase-1-4-2/spool-access-to-dafny.ymlis excluded by!**/generated/**evidence/traceability/generated/phase-1-4-2/test-to-dafny.ymlis excluded by!**/generated/**reports/generated/phase-1-1/semantic-coverage-report.mdis excluded by!**/generated/**reports/generated/phase-1-1/semantic-coverage.ymlis excluded by!**/generated/**reports/generated/phase-1-3/dafny-dataset-catalog-validation-report.mdis excluded by!**/generated/**
📒 Files selected for processing (46)
docs/design/STATUS.mddocs/design/specs/43-dafny-executable-semantics-policy.mdevidence/traceability/index.ymlformal/executable-semantics/dafny/README.mdformal/executable-semantics/dafny/modules/job_spool.dfyformal/executable-semantics/dafny/modules/types.dfyreports/current/dafny/dafny-semantics-red-team-review.mdreports/current/dafny/dafny-semantics-report.mdreports/current/dafny/dafny-semantics-validation-report.mdreports/current/dafny/dafny-toolchain-red-team-review.mdreports/current/dafny/dafny-verification-report.mdreports/current/readiness/post-merge-integration-sweep-report.mdreports/index.ymlreports/phases/phase-1-4/spool-protected-resource/coverage-report.mdreports/phases/phase-1-4/spool-protected-resource/open-issues.mdreports/phases/phase-1-4/spool-protected-resource/red-team-review.mdreports/phases/phase-1-4/spool-protected-resource/report.mdreports/phases/phase-1-4/spool-protected-resource/validation-report.mdscripts/check-phase1-4-2-spool-coverage.pyscripts/checks/artifact-hygiene/check-artifact-layout.pyscripts/checks/semantic-coverage/check-semantic-coverage-mapping.pyscripts/generators/generate-dataset-catalog-coverage.pyscripts/generators/generate-semantic-coverage.pyscripts/generators/generate-spool-coverage.pyscripts/index.ymlscripts/phases/phase-1/check-phase1-4-2-spool-coverage.pyscripts/validate-all.shtests/catalog/job-spool.ymltests/fixtures/job/spool-browse-nonowner-0913.ymltests/fixtures/job/spool-browse-owner-0912.ymltests/fixtures/job/spool-cross-request-replay-0917.ymltests/fixtures/job/spool-deny-audit-0920.ymltests/fixtures/job/spool-evidence-not-audit-0916.ymltests/fixtures/job/spool-export-no-audit-0915.ymltests/fixtures/job/spool-purge-denied-0914.ymltests/fixtures/job/spool-spec-gap-not-success-0918.ymltests/fixtures/job/spool-unsupported-fails-0919.ymltests/golden/job/spool-browse-nonowner-0913.ymltests/golden/job/spool-browse-owner-0912.ymltests/golden/job/spool-cross-request-replay-0917.ymltests/golden/job/spool-deny-audit-0920.ymltests/golden/job/spool-evidence-not-audit-0916.ymltests/golden/job/spool-export-no-audit-0915.ymltests/golden/job/spool-purge-denied-0914.ymltests/golden/job/spool-spec-gap-not-success-0918.ymltests/golden/job/spool-unsupported-fails-0919.yml
📜 Review details
⏰ Context from checks skipped due to timeout of 90000ms. You can increase the timeout in your CodeRabbit configuration to a maximum of 15 minutes (900000ms). (1)
- GitHub Check: validate design registries and lint gates
🧰 Additional context used
📓 Path-based instructions (3)
**
⚙️ CodeRabbit configuration file
**: MFOS is in Phase 1. CodeRabbit review is advisory only and must not be treated as the sole merge gate. Prioritize correctness, source-grounding, artifact lifecycle, validator coverage, and boundary preservation.
Files:
reports/current/readiness/post-merge-integration-sweep-report.mdreports/current/dafny/dafny-semantics-red-team-review.mdreports/current/dafny/dafny-semantics-report.mdtests/golden/job/spool-purge-denied-0914.ymltests/fixtures/job/spool-export-no-audit-0915.ymlscripts/generators/generate-dataset-catalog-coverage.pytests/fixtures/job/spool-evidence-not-audit-0916.ymlformal/executable-semantics/dafny/README.mdtests/fixtures/job/spool-cross-request-replay-0917.ymltests/fixtures/job/spool-deny-audit-0920.ymltests/fixtures/job/spool-purge-denied-0914.ymltests/golden/job/spool-spec-gap-not-success-0918.ymlreports/current/dafny/dafny-verification-report.mdscripts/validate-all.shtests/fixtures/job/spool-spec-gap-not-success-0918.ymlreports/phases/phase-1-4/spool-protected-resource/open-issues.mdreports/current/dafny/dafny-semantics-validation-report.mdtests/fixtures/job/spool-unsupported-fails-0919.ymldocs/design/STATUS.mdreports/phases/phase-1-4/spool-protected-resource/report.mdreports/phases/phase-1-4/spool-protected-resource/red-team-review.mdtests/fixtures/job/spool-browse-owner-0912.ymltests/golden/job/spool-evidence-not-audit-0916.ymltests/fixtures/job/spool-browse-nonowner-0913.ymlreports/current/dafny/dafny-toolchain-red-team-review.mdtests/golden/job/spool-deny-audit-0920.ymltests/golden/job/spool-unsupported-fails-0919.ymltests/golden/job/spool-browse-nonowner-0913.ymldocs/design/specs/43-dafny-executable-semantics-policy.mdreports/phases/phase-1-4/spool-protected-resource/validation-report.mdreports/index.ymltests/golden/job/spool-export-no-audit-0915.ymlreports/phases/phase-1-4/spool-protected-resource/coverage-report.mdscripts/checks/artifact-hygiene/check-artifact-layout.pytests/golden/job/spool-cross-request-replay-0917.ymlscripts/generators/generate-semantic-coverage.pyscripts/checks/semantic-coverage/check-semantic-coverage-mapping.pyformal/executable-semantics/dafny/modules/types.dfyscripts/index.ymlscripts/check-phase1-4-2-spool-coverage.pytests/golden/job/spool-browse-owner-0912.ymlevidence/traceability/index.ymlscripts/generators/generate-spool-coverage.pyscripts/phases/phase-1/check-phase1-4-2-spool-coverage.pytests/catalog/job-spool.ymlformal/executable-semantics/dafny/modules/job_spool.dfy
formal/executable-semantics/**
⚙️ CodeRabbit configuration file
formal/executable-semantics/**: Do not suggest Rust semantic-core work, generated production code, hosted daemon behavior, or production implementation. Dafny artifacts remain non-production executable-semantics evidence.
Files:
formal/executable-semantics/dafny/README.mdformal/executable-semantics/dafny/modules/types.dfyformal/executable-semantics/dafny/modules/job_spool.dfy
reports/phases/phase-1-4/**
⚙️ CodeRabbit configuration file
reports/phases/phase-1-4/**: Phase 1.4 is planning-only unless a later reviewed implementation gate explicitly changes scope. Flag accidental implementation, generated Phase 1.4 traceability, hosted daemons, semantic-runner commands, and service behavior.
Files:
reports/phases/phase-1-4/spool-protected-resource/open-issues.mdreports/phases/phase-1-4/spool-protected-resource/report.mdreports/phases/phase-1-4/spool-protected-resource/red-team-review.mdreports/phases/phase-1-4/spool-protected-resource/validation-report.mdreports/phases/phase-1-4/spool-protected-resource/coverage-report.md
🪛 Ruff (0.15.12)
scripts/phases/phase-1/check-phase1-4-2-spool-coverage.py
[error] 79-79: subprocess call: check for execution of untrusted input
(S603)
🔇 Additional comments (28)
reports/current/dafny/dafny-semantics-red-team-review.md (1)
30-30: Verification count update looks consistent.No issue in this report update.
reports/current/dafny/dafny-toolchain-red-team-review.md (1)
24-24: Toolchain report count update is coherent.Looks good.
scripts/generators/generate-dataset-catalog-coverage.py (1)
500-500: Generated validation text update is consistent.No concerns with this change.
docs/design/specs/43-dafny-executable-semantics-policy.md (1)
283-283: Policy doc verification total update is fine.This is consistent with the rest of the PR artifacts.
formal/executable-semantics/dafny/README.md (1)
125-125: README verification count update is consistent.No issues detected.
reports/current/readiness/post-merge-integration-sweep-report.md (1)
87-87: Integration sweep report count update looks good.No concerns here.
scripts/generators/generate-semantic-coverage.py (2)
279-280: Phase filter update is correct for Phase 1.1 scoping.Good adjustment to exclude Phase 1.4.2 entries from Phase 1.1 coverage generation.
432-432: Summary verification count update is consistent.Looks good.
reports/current/dafny/dafny-verification-report.md (1)
31-31: Verification report totals are internally consistent.No issues with these updates.
Also applies to: 49-49
docs/design/STATUS.md (1)
204-204: Boundary language and status update look consistent.The Phase 1.4.2 addition clearly preserves non-production constraints, and the verifier count update is aligned with the same scope narrative.
Also applies to: 235-243
reports/current/dafny/dafny-semantics-validation-report.md (1)
44-44: LGTM — verification result sync is clear and precise.reports/current/dafny/dafny-semantics-report.md (1)
66-66: LGTM — count update is consistent with the current Dafny verification state.reports/phases/phase-1-4/spool-protected-resource/open-issues.md (1)
9-15: Scope boundaries are clearly preserved.The deferred-items list correctly keeps real service/daemon behavior outside Phase 1.4.2.
scripts/validate-all.sh (1)
45-45: Good integration of Phase 1.4.2 validation + generation hooks.This keeps spool coverage checks and traceability generation wired into the standard validation path.
Also applies to: 73-73
evidence/traceability/index.yml (1)
123-135: Traceability inventory registration for Phase 1.4.2 looks complete.
generated_by,coverage_summary, andcontainsare all captured with the expected phase pathing.reports/index.yml (1)
233-234: Looks consistent with the report inventory model.The new Phase 1.4.2 section and report entries follow the existing index schema and naming pattern.
Also applies to: 392-401
tests/golden/job/spool-browse-nonowner-0913.yml (1)
12-12: Good golden update for spool browse denial path.The decision/state-transition updates are coherent with the spool-specific non-owner browse scenario.
Also applies to: 23-25
scripts/check-phase1-4-2-spool-coverage.py (1)
10-11: Wrapper delegation is clean and direct.The target resolution and
runpyhandoff match the root-wrapper pattern.scripts/index.yml (1)
125-132: Registry wiring is internally consistent.Entrypoint, generator, phase helper, and root-wrapper records align to the same Phase 1.4.2 spool coverage target.
Also applies to: 274-276, 306-308, 385-392
tests/golden/job/spool-purge-denied-0914.yml (1)
12-12: This golden transition update looks correct for purge-denied semantics.The spool object/state/action mapping now matches the OP_PURGE denial path.
Also applies to: 23-25
tests/fixtures/job/spool-purge-denied-0914.yml (1)
17-25: Fixture enrichment is solid and semantically aligned.The explicit
spool_entryplus purge-denial semantic facts strengthen traceability to the intended deny behavior.Also applies to: 27-30
tests/fixtures/job/spool-export-no-audit-0915.yml (1)
17-26: Good fail-closed fixture modeling for export-without-audit.The state and semantic facts clearly encode the required audit dependency and expected non-completion of export.
Also applies to: 28-33
tests/fixtures/job/spool-deny-audit-0920.yml (1)
1-41: Looks consistent with deny-with-audit-before-return semantics.Fixture structure and semantic facts are coherent for the Phase 1.4.2 spool deny/audit scenario.
tests/golden/job/spool-browse-owner-0912.yml (1)
10-42: Golden updates are coherent with the spool browse-owner semantics.Decision ID, state transition path, and expected final state are internally consistent.
scripts/checks/artifact-hygiene/check-artifact-layout.py (1)
43-67: Wrapper registration looks correct.The added allowlist entry and
ROOT_CHECK_WRAPPERSmapping are consistent forcheck-phase1-4-2-spool-coverage.py.tests/golden/job/spool-spec-gap-not-success-0918.yml (1)
1-45: Fail-closed SPEC_GAP golden is well-formed.Expected decision, audit record, failure mode, and final state are consistent with the scenario intent.
tests/fixtures/job/spool-spec-gap-not-success-0918.yml (1)
1-37: Fixture is consistent for SPEC_GAP-not-success behavior.The semantic facts and expected oracle/evidence linkage are coherent for this negative scenario.
tests/golden/job/spool-export-no-audit-0915.yml (1)
12-21: All three artifacts consistently useSEED-MFOS-PHASE09-0001, but verify identifier/seed alignment is intentional.The verification confirms that fixture, golden, and catalog all retain
SEED-MFOS-PHASE09-0001for the 0915 test case—this is not a golden-specific inconsistency. However, this reveals a broader alignment gap: decision identifiers in lines 12-21 useDECISION-MFOS-SPOOL-EXPORT-NO-AUDIT-0915andPHASE142naming, while the seed remains atPHASE09-0001. If identifier and seed versions are required to stay in sync for traceability tooling, this systematic inconsistency across all three artifacts should be addressed.
| Generated traceability lives under | ||
| `evidence/traceability/generated/phase-1-4-2/`. | ||
|
|
||
| ## Coverage Summary | ||
|
|
||
| - Spool protected-resource aggregate: `C4_VERIFIED_PROPERTY` | ||
| - Required scenario rows: `C5_CONFORMANCE_LINKED` | ||
| - Fixture/golden rows: `C5_CONFORMANCE_LINKED` | ||
| - Requirement aggregate: `C2_PARTIAL_SEMANTIC` | ||
| - Formal claim aggregate: `C3_FULL_SEMANTIC` | ||
| - C5 overclaim remaining: false | ||
|
|
||
| ## C5 Scenario Rows | ||
|
|
||
| - `spool-browse-owner-0912`: owner browse allowed. | ||
| - `spool-browse-nonowner-0913`: non-owner browse denied with no content. | ||
| - `spool-purge-denied-0914`: purge without authority denied. | ||
| - `spool-export-no-audit-0915`: export with required audit unavailable fails closed. | ||
| - `spool-evidence-not-audit-0916`: SpoolEvidence is not AuditEvidence. | ||
| - `spool-cross-request-replay-0917`: cross-request authorization replay blocked. | ||
| - `spool-spec-gap-not-success-0918`: SPEC_GAP is not success. | ||
| - `spool-unsupported-fails-0919`: UNSUPPORTED fails closed. | ||
| - `spool-deny-audit-0920`: DENY with audit obligation links to before-return audit. |
There was a problem hiding this comment.
Phase 1.4 planning boundary is being crossed here.
Line 5 through Line 27 publish generated Phase 1.4 traceability and concrete conformance rows in a planning-only report path. This should be downgraded to planning intent (or moved behind an explicitly reviewed implementation gate artifact).
As per coding guidelines, "Phase 1.4 is planning-only unless a later reviewed implementation gate explicitly changes scope. Flag accidental implementation, generated Phase 1.4 traceability, hosted daemons, semantic-runner commands, and service behavior."
🤖 Prompt for AI Agents
Verify each finding against the current code and only fix it if needed.
In `@reports/phases/phase-1-4/spool-protected-resource/coverage-report.md` around
lines 5 - 27, The Phase 1.4 content in coverage-report.md is publishing
generated traceability and concrete C5 rows as if they are implemented; change
this to planning-only by: update the header and the "Generated traceability
lives under `evidence/traceability/generated/phase-1-4-2/`" line to indicate
"planning-only / draft" (or move the generated artifacts behind an explicit
implementation gate), and mark the Coverage Summary and each C5 scenario row
(e.g., entries like `spool-browse-owner-0912`, `spool-purge-denied-0914`,
`spool-evidence-not-audit-0916`) as planning intent rather than concrete
verification (or remove them from published paths) so Phase 1.4 artifacts are
not treated as implemented until an explicit reviewed implementation gate flips
scope.
| - Spool browse without authorization is blocked by bound decision and | ||
| Authorization predicate linkage. | ||
| - Non-owner browse without explicit allowing authorization releases no content. | ||
| - Purge without authority is denied. | ||
| - Export without satisfied audit obligation fails closed. | ||
| - SpoolEvidence is distinct from AuditEvidence. | ||
| - Cross-request Spool authorization replay is blocked by correlation binding. | ||
| - DENY creates no successful Spool browse, purge, or export result. | ||
| - Required audit on DENY links to before-return audit or audit-unavailable | ||
| fail-closed behavior. | ||
| - Python tooling validates structure/linkage only and does not decide Spool | ||
| allow/deny/audit behavior. | ||
| - Scope does not expand into operator commands, full FVS, production spoold, | ||
| Rust semantic-core, or hosted daemons. | ||
| - C4/C5 coverage is not overclaimed. |
There was a problem hiding this comment.
🧩 Analysis chain
🏁 Script executed:
#!/bin/bash
set -euo pipefail
# 1) Find explicit Phase 1.4 scope-change or implementation-gate evidence.
rg -n -C2 "planning-only|implementation gate|changes scope|Phase 1\.4\.2|scope change|entry gate|exit gate" \
reports/phases/phase-1-4 \
reports/current/readiness \
reports/current/source-grounding || true
# 2) List likely gate/readiness docs under the Phase 1.4 tree for manual confirmation.
fd -i "gate|readiness|scope|review" reports/phases/phase-1-4Repository: minto-dane/mfos
Length of output: 7774
Reframe lines 12-26 as planned/targeted semantics, not implementation guarantees.
These statements ("is blocked", "is denied", "releases no content") read as implementation behavior guarantees within a planning-only Phase 1.4.2 document. No reviewed implementation gate exists to promote this document to implementation status (entry-gate and exit-gate remain planning-only and deferred). Either reference an explicit Phase 1.4 scope-change gate, or add qualifying language (e.g., "planned to be blocked", "intended to deny") to align with planning scope. The residual-risk section correctly bounds scope, but lines 12-26 need consistent framing.
🤖 Prompt for AI Agents
Verify each finding against the current code and only fix it if needed.
In `@reports/phases/phase-1-4/spool-protected-resource/red-team-review.md` around
lines 12 - 26, Reword the assertions in the block starting with "Spool browse
without authorization is blocked..." (lines 12–26) so they read as
planned/targeted semantics rather than implementation guarantees: prepend or
replace phrasing with qualifiers like "planned to be", "intended to", or
"expected to" (or reference an explicit Phase 1.4 scope-change/entry-exit gate)
for each bullet (e.g., "Spool browse without authorization is planned to be
blocked"); ensure consistency across all bullets and retain the residual-risk
framing unchanged.
| Generated traceability is under | ||
| `evidence/traceability/generated/phase-1-4-2/`. C5 is claimed only for rows with | ||
| fixture, embedded oracle, and golden-vector links. Broad parent requirement | ||
| coverage remains partial where production spool service behavior is outside | ||
| Phase 1.4.2. |
There was a problem hiding this comment.
Remove generated traceability/C5 claims from the Phase 1.4 planning report.
This section goes past planning scope by naming generated evidence output and asserting C5 claim conditions. In this directory, that reads like implementation-traceability status rather than planning material and weakens the Phase 1 boundary.
Suggested rewording
## Evidence
-Generated traceability is under
-`evidence/traceability/generated/phase-1-4-2/`. C5 is claimed only for rows with
-fixture, embedded oracle, and golden-vector links. Broad parent requirement
-coverage remains partial where production spool service behavior is outside
-Phase 1.4.2.
+Traceability and evidence handling for this topic are tracked separately from
+this Phase 1.4 planning report. This document should stay limited to planned
+scope, constraints, and verification intent.As per coding guidelines, "Phase 1.4 is planning-only unless a later reviewed implementation gate explicitly changes scope. Flag accidental implementation, generated Phase 1.4 traceability, hosted daemons, semantic-runner commands, and service behavior."
📝 Committable suggestion
‼️ IMPORTANT
Carefully review the code before committing. Ensure that it accurately replaces the highlighted code, contains no missing lines, and has no issues with indentation. Thoroughly test & benchmark the code to ensure it meets the requirements.
| Generated traceability is under | |
| `evidence/traceability/generated/phase-1-4-2/`. C5 is claimed only for rows with | |
| fixture, embedded oracle, and golden-vector links. Broad parent requirement | |
| coverage remains partial where production spool service behavior is outside | |
| Phase 1.4.2. | |
| Traceability and evidence handling for this topic are tracked separately from | |
| this Phase 1.4 planning report. This document should stay limited to planned | |
| scope, constraints, and verification intent. |
🤖 Prompt for AI Agents
Verify each finding against the current code and only fix it if needed.
In `@reports/phases/phase-1-4/spool-protected-resource/report.md` around lines 33
- 37, Remove the implementation-traceability specifics from the Phase 1.4
planning report: delete the reference to the generated evidence path
"evidence/traceability/generated/phase-1-4-2/" and any asserted C5 claim
language (mentions of C5 being claimed "only for rows with fixture, embedded
oracle, and golden-vector links"); instead replace with a planning-scoped
statement clarifying Phase 1.4 is planning-only and that implementation
traceability and hosted/service behavior will be addressed in a later
implementation gate. Ensure the edited paragraph in report.md no longer reads
like implementation status or lists generated artifacts.
| - `python3 scripts/check-phase1-4-2-spool-coverage.py` | ||
| - `python3 -m py_compile $(find scripts tools -name '*.py' -type f | sort)` |
There was a problem hiding this comment.
Use one canonical spool coverage checker path in both command lists.
Line 22 and Line 50 include python3 scripts/check-phase1-4-2-spool-coverage.py, while the validator pipeline uses python3 scripts/phases/phase-1/check-phase1-4-2-spool-coverage.py (see scripts/validate-all.sh, Line 45). This makes the report non-reproducible for readers following it verbatim.
Suggested doc fix
-- `python3 scripts/check-phase1-4-2-spool-coverage.py`
+- `python3 scripts/phases/phase-1/check-phase1-4-2-spool-coverage.py`
...
-- `python3 scripts/check-phase1-4-2-spool-coverage.py`
+- `python3 scripts/phases/phase-1/check-phase1-4-2-spool-coverage.py`As per coding guidelines, "Prioritize correctness, source-grounding, artifact lifecycle, validator coverage, and boundary preservation."
Also applies to: 50-51
🤖 Prompt for AI Agents
Verify each finding against the current code and only fix it if needed.
In `@reports/phases/phase-1-4/spool-protected-resource/validation-report.md`
around lines 22 - 23, Update the two occurrences of the spool coverage checker
command in the report so they use the canonical validator path used by the
pipeline; replace any `python3 scripts/check-phase1-4-2-spool-coverage.py`
references with the canonical `python3
scripts/phases/phase-1/check-phase1-4-2-spool-coverage.py` in both command lists
mentioned in the document (the entries around the spool coverage checks),
ensuring the report commands match the validator's `scripts/validate-all.sh`
invocation.
| negative_symbols = test.get("negative_failure_conditions", []) | ||
| if LEVEL_RANK.get(level, -1) >= LEVEL_RANK["C4_VERIFIED_PROPERTY"] and not negative_symbols: | ||
| errors.append(f"{test_id}: verified negative test lacks negative_failure_conditions") | ||
| if "UNSUPPORTED" in test_id and "INV_AUTH_UNSUPPORTED_NOT_SUCCESS" not in negative_symbols: | ||
| if LEVEL_RANK.get(level, -1) >= LEVEL_RANK["C4_VERIFIED_PROPERTY"] and "UNSUPPORTED" in test_id and "INV_AUTH_UNSUPPORTED_NOT_SUCCESS" not in negative_symbols: | ||
| errors.append(f"{test_id}: unsupported negative test must map to INV_AUTH_UNSUPPORTED_NOT_SUCCESS") | ||
| if "SPEC-GAP" in test_id and "INV_AUTH_SPEC_GAP_NOT_SUCCESS" not in negative_symbols: | ||
| if LEVEL_RANK.get(level, -1) >= LEVEL_RANK["C4_VERIFIED_PROPERTY"] and "SPEC-GAP" in test_id and "INV_AUTH_SPEC_GAP_NOT_SUCCESS" not in negative_symbols: |
There was a problem hiding this comment.
Guard negative_failure_conditions before membership checks.
If negative_failure_conditions is present but null, Line 114 and Line 116 will raise a TypeError (argument of type 'NoneType' is not iterable) instead of reporting a validation error.
Suggested fix
- negative_symbols = test.get("negative_failure_conditions", [])
+ negative_symbols = test.get("negative_failure_conditions", [])
+ if not isinstance(negative_symbols, list):
+ errors.append(f"{test_id}: negative_failure_conditions must be a list")
+ negative_symbols = []As per coding guidelines, "Prioritize correctness, source-grounding, artifact lifecycle, validator coverage, and boundary preservation."
🤖 Prompt for AI Agents
Verify each finding against the current code and only fix it if needed.
In `@scripts/checks/semantic-coverage/check-semantic-coverage-mapping.py` around
lines 111 - 116, The code assumes negative_failure_conditions is iterable but it
can be None; ensure negative_symbols is a list before membership checks by
normalizing it (e.g. replace None with [] right after assignment of
negative_symbols) or by guarding each membership test with an existence check;
update the block using negative_symbols, LEVEL_RANK, test_id and errors so lines
that check `"INV_AUTH_UNSUPPORTED_NOT_SUCCESS" in negative_symbols` and
`"INV_AUTH_SPEC_GAP_NOT_SUCCESS" in negative_symbols` only run against a
non-None iterable (or use negative_symbols =
test.get("negative_failure_conditions") or [] to coerce None to an empty list).
| c5_test( | ||
| "NEG-MFOS-JOB-SPOOL-EVIDENCE-NOT-AUDIT-0916", | ||
| "spool-evidence-not-audit-0916", | ||
| "INV_SPOOL_EVIDENCE_NOT_AUDIT_EVIDENCE", | ||
| "Spool evidence is distinct from AuditEvidence and cannot satisfy audit evidence.", | ||
| required_fixture_fact_keys=[ | ||
| "dafny_property", | ||
| "spool_operation", | ||
| "spool_evidence_present", | ||
| "audit_evidence_present", | ||
| "audit_satisfied_by_spool_evidence", | ||
| ], |
There was a problem hiding this comment.
Don't claim C5 coverage for behavior this lemma doesn't express.
This row links NEG-MFOS-JOB-SPOOL-EVIDENCE-NOT-AUDIT-0916 to INV_SPOOL_EVIDENCE_NOT_AUDIT_EVIDENCE, but that lemma only proves type separation (SpoolEvidence is not an AuditRecord). The catalog row at tests/catalog/job-spool.yml Lines 662-689 expects a stronger fail-closed behavior: the request must reject with MFOS_ERR_INVALID_AUDIT_RECORD. Until there's a result-level Dafny property for that path, this mapping overstates Phase 1.4.2 coverage.
As per coding guidelines, "Prioritize correctness, source-grounding, artifact lifecycle, validator coverage, and boundary preservation."
🤖 Prompt for AI Agents
Verify each finding against the current code and only fix it if needed.
In `@scripts/generators/generate-spool-coverage.py` around lines 142 - 153, The
catalog entry linking test ID NEG-MFOS-JOB-SPOOL-EVIDENCE-NOT-AUDIT-0916 to
lemma INV_SPOOL_EVIDENCE_NOT_AUDIT_EVIDENCE overclaims coverage because that
lemma only proves type separation, not the result-level rejection
(MFOS_ERR_INVALID_AUDIT_RECORD) expected by the catalog at the job-spool test;
update the generator mapping so this row is not mapped to
INV_SPOOL_EVIDENCE_NOT_AUDIT_EVIDENCE (either remove the mapping or mark it as
uncovered) and instead leave it unmapped until a Dafny lemma that asserts the
result-level error path exists, referencing the test ID
NEG-MFOS-JOB-SPOOL-EVIDENCE-NOT-AUDIT-0916, lemma
INV_SPOOL_EVIDENCE_NOT_AUDIT_EVIDENCE, and the catalog entry in
tests/catalog/job-spool.yml.
| def collect_mapped_symbols() -> dict[str, list[tuple[str, str, dict[str, Any]]]]: | ||
| symbols: dict[str, list[tuple[str, str, dict[str, Any]]]] = {} | ||
| for name in TRACE_FILES: | ||
| data = load_yaml(TRACEABILITY_DIR / name) | ||
| rows = data.get("entries") or data.get("tests") or data.get("fixtures") or data.get("requirements") or data.get("formal_claims") or [] | ||
| if not isinstance(rows, list): | ||
| continue | ||
| for row in rows: | ||
| for mapped in row.get("coverage_mappings") or []: | ||
| symbol = mapped.get("dafny_symbol") | ||
| if symbol: | ||
| symbols.setdefault(str(symbol), []).append((name, str(row.get("coverage_level")), row)) | ||
| return symbols |
There was a problem hiding this comment.
Skip missing traceability files before reading them.
compare_generated() already records missing generated artifacts, but this helper still calls load_yaml() for every expected file unconditionally. If one file is absent, the validator raises here before it can print the collected diagnostics, which makes artifact-lifecycle failures much harder to root-cause.
Suggested fix
def collect_mapped_symbols() -> dict[str, list[tuple[str, str, dict[str, Any]]]]:
symbols: dict[str, list[tuple[str, str, dict[str, Any]]]] = {}
for name in TRACE_FILES:
- data = load_yaml(TRACEABILITY_DIR / name)
+ path = TRACEABILITY_DIR / name
+ if not path.exists():
+ continue
+ data = load_yaml(path)
rows = data.get("entries") or data.get("tests") or data.get("fixtures") or data.get("requirements") or data.get("formal_claims") or []
if not isinstance(rows, list):
continueAs per coding guidelines, "Prioritize correctness, source-grounding, artifact lifecycle, validator coverage, and boundary preservation."
📝 Committable suggestion
‼️ IMPORTANT
Carefully review the code before committing. Ensure that it accurately replaces the highlighted code, contains no missing lines, and has no issues with indentation. Thoroughly test & benchmark the code to ensure it meets the requirements.
| def collect_mapped_symbols() -> dict[str, list[tuple[str, str, dict[str, Any]]]]: | |
| symbols: dict[str, list[tuple[str, str, dict[str, Any]]]] = {} | |
| for name in TRACE_FILES: | |
| data = load_yaml(TRACEABILITY_DIR / name) | |
| rows = data.get("entries") or data.get("tests") or data.get("fixtures") or data.get("requirements") or data.get("formal_claims") or [] | |
| if not isinstance(rows, list): | |
| continue | |
| for row in rows: | |
| for mapped in row.get("coverage_mappings") or []: | |
| symbol = mapped.get("dafny_symbol") | |
| if symbol: | |
| symbols.setdefault(str(symbol), []).append((name, str(row.get("coverage_level")), row)) | |
| return symbols | |
| def collect_mapped_symbols() -> dict[str, list[tuple[str, str, dict[str, Any]]]]: | |
| symbols: dict[str, list[tuple[str, str, dict[str, Any]]]] = {} | |
| for name in TRACE_FILES: | |
| path = TRACEABILITY_DIR / name | |
| if not path.exists(): | |
| continue | |
| data = load_yaml(path) | |
| rows = data.get("entries") or data.get("tests") or data.get("fixtures") or data.get("requirements") or data.get("formal_claims") or [] | |
| if not isinstance(rows, list): | |
| continue | |
| for row in rows: | |
| for mapped in row.get("coverage_mappings") or []: | |
| symbol = mapped.get("dafny_symbol") | |
| if symbol: | |
| symbols.setdefault(str(symbol), []).append((name, str(row.get("coverage_level")), row)) | |
| return symbols |
🤖 Prompt for AI Agents
Verify each finding against the current code and only fix it if needed.
In `@scripts/phases/phase-1/check-phase1-4-2-spool-coverage.py` around lines 231 -
243, collect_mapped_symbols currently calls load_yaml on every file in
TRACE_FILES without checking existence, causing exceptions when traceability
files are missing; change it to skip non-existent files by checking for file
presence under TRACEABILITY_DIR (use TRACEABILITY_DIR / name) before calling
load_yaml, and only attempt to parse when the file exists; keep the rest of the
logic (iterating rows, reading "coverage_mappings", using "dafny_symbol") the
same so the function still returns the symbols dict when some trace files are
absent.
| for forbidden in ( | ||
| ROOT / "formal" / "executable-semantics" / "rust", | ||
| ROOT / "implementation" / "services" / "jobd", | ||
| ROOT / "implementation" / "services" / "spoold", | ||
| ROOT / "implementation" / "services" / "operatord", | ||
| ): | ||
| if forbidden.exists(): | ||
| errors.append(f"Phase 1.4.2 must not introduce Rust semantic-core or daemon implementation artifact: {forbidden}") | ||
| for path in sorted((ROOT / "reports/current").glob("*phase-1-4-2*")): | ||
| errors.append(f"Phase 1.4.2 report must not be under reports/current: {path}") |
There was a problem hiding this comment.
Scope these boundary checks to Phase 1.4.2 artifacts, not repo-wide existence.
These guards fail the validator whenever the checkout already contains implementation/services/jobd, implementation/services/spoold, implementation/services/operatord, or any reports/current/*phase-1-4-2* path, even if this PR never introduced them. That makes the phase check non-local and brittle; it should validate the artifacts owned by this phase, not assert whole-repo absence.
As per coding guidelines, "Prioritize correctness, source-grounding, artifact lifecycle, validator coverage, and boundary preservation."
🤖 Prompt for AI Agents
Verify each finding against the current code and only fix it if needed.
In `@scripts/phases/phase-1/check-phase1-4-2-spool-coverage.py` around lines 297 -
306, The current checks iterate repository-wide paths (using ROOT and forbidden
tuples) and always fail if those directories exist anywhere; instead restrict
validation to only files/paths introduced or modified by this phase/PR: obtain
the list of changed paths (e.g., the existing changed_files/changed_paths
variable or the PR diff) and replace the repository-wide exists() checks with
tests against that list (check if any changed path is under
ROOT/"formal"/"executable-semantics"/"rust" or
ROOT/"implementation"/"services"/"jobd"/"spoold"/"operatord" and similarly if
any changed path matches reports/current/*phase-1-4-2*), appending errors only
when a forbidden path is present in the changed set; keep using the same errors
list and preserve the same error messages.
| decisions: [{decision_id: DECISION-MFOS-SPOOL-EVIDENCE-NOT-AUDIT-0916, result: ALLOW_WITH_AUDIT, policy_version: 1, obligations: [AUDIT_SECURITY_DECISION]}] | ||
| state_transitions: [{object: SPOOL-MFOS-PHASE142-0916, from: SPOOL_AUDIT_EVIDENCE_CHECK, action: OP_EXPORT, to: FAILED, reason: MFOS_ERR_INVALID_AUDIT_RECORD}] | ||
| audit_records: [] | ||
| failure_mode: MFOS_ERR_INVALID_AUDIT_RECORD | ||
| final_state: FAILED | ||
| oracle_ref: tests/golden/job/spool-evidence-not-audit-0916.yml | ||
| fixture_ref: tests/fixtures/job/spool-evidence-not-audit-0916.yml | ||
| golden_ref: tests/golden/job/spool-evidence-not-audit-0916.yml | ||
| negative: true | ||
| security_sensitive: true | ||
| audit_obligation_required: false |
There was a problem hiding this comment.
Align audit_obligation_required with the expected decision.
Line 678 marks this scenario as ALLOW_WITH_AUDIT with an AUDIT_SECURITY_DECISION obligation, so audit_obligation_required: false on Line 688 contradicts the contract the row is asserting. That can let catalog/coverage checks treat an audit-gated failure path as if no audit obligation existed.
Suggested fix
- audit_obligation_required: false
+ audit_obligation_required: trueAs per coding guidelines, "Prioritize correctness, source-grounding, artifact lifecycle, validator coverage, and boundary preservation."
📝 Committable suggestion
‼️ IMPORTANT
Carefully review the code before committing. Ensure that it accurately replaces the highlighted code, contains no missing lines, and has no issues with indentation. Thoroughly test & benchmark the code to ensure it meets the requirements.
| decisions: [{decision_id: DECISION-MFOS-SPOOL-EVIDENCE-NOT-AUDIT-0916, result: ALLOW_WITH_AUDIT, policy_version: 1, obligations: [AUDIT_SECURITY_DECISION]}] | |
| state_transitions: [{object: SPOOL-MFOS-PHASE142-0916, from: SPOOL_AUDIT_EVIDENCE_CHECK, action: OP_EXPORT, to: FAILED, reason: MFOS_ERR_INVALID_AUDIT_RECORD}] | |
| audit_records: [] | |
| failure_mode: MFOS_ERR_INVALID_AUDIT_RECORD | |
| final_state: FAILED | |
| oracle_ref: tests/golden/job/spool-evidence-not-audit-0916.yml | |
| fixture_ref: tests/fixtures/job/spool-evidence-not-audit-0916.yml | |
| golden_ref: tests/golden/job/spool-evidence-not-audit-0916.yml | |
| negative: true | |
| security_sensitive: true | |
| audit_obligation_required: false | |
| decisions: [{decision_id: DECISION-MFOS-SPOOL-EVIDENCE-NOT-AUDIT-0916, result: ALLOW_WITH_AUDIT, policy_version: 1, obligations: [AUDIT_SECURITY_DECISION]}] | |
| state_transitions: [{object: SPOOL-MFOS-PHASE142-0916, from: SPOOL_AUDIT_EVIDENCE_CHECK, action: OP_EXPORT, to: FAILED, reason: MFOS_ERR_INVALID_AUDIT_RECORD}] | |
| audit_records: [] | |
| failure_mode: MFOS_ERR_INVALID_AUDIT_RECORD | |
| final_state: FAILED | |
| oracle_ref: tests/golden/job/spool-evidence-not-audit-0916.yml | |
| fixture_ref: tests/fixtures/job/spool-evidence-not-audit-0916.yml | |
| golden_ref: tests/golden/job/spool-evidence-not-audit-0916.yml | |
| negative: true | |
| security_sensitive: true | |
| audit_obligation_required: true |
🤖 Prompt for AI Agents
Verify each finding against the current code and only fix it if needed.
In `@tests/catalog/job-spool.yml` around lines 678 - 688, The test YAML's decision
block includes ALLOW_WITH_AUDIT with obligation AUDIT_SECURITY_DECISION but the
audit flag is incorrect; update the audit_obligation_required field from false
to true so the fixture's metadata matches the decision/obligation (ensure the
audit_obligation_required value aligns with the decisions: [{decision_id:
DECISION-MFOS-SPOOL-EVIDENCE-NOT-AUDIT-0916, result: ALLOW_WITH_AUDIT,
obligations: [AUDIT_SECURITY_DECISION]}] and final_state: FAILED).
| semantic_facts: | ||
| dafny_property: INV_SPOOL_EVIDENCE_NOT_AUDIT_EVIDENCE | ||
| spool_operation: OP_EXPORT | ||
| spool_evidence_present: true | ||
| audit_evidence_present: false | ||
| audit_satisfied_by_spool_evidence: false |
There was a problem hiding this comment.
Encode the audit obligation in the fixture semantics.
The negative case only becomes meaningful if this request is already in an ALLOW_WITH_AUDIT path. Right now the fixture says spool evidence is present and audit evidence is absent, but it never states that audit is actually required, even though the golden and catalog both do. That leaves the fail-closed reason under-grounded in the fixture itself.
Suggested fix
semantic_facts:
dafny_property: INV_SPOOL_EVIDENCE_NOT_AUDIT_EVIDENCE
spool_operation: OP_EXPORT
+ authorization_result: ALLOW_WITH_AUDIT
+ audit_required: true
spool_evidence_present: true
audit_evidence_present: false
audit_satisfied_by_spool_evidence: falseAs per coding guidelines, "Prioritize correctness, source-grounding, artifact lifecycle, validator coverage, and boundary preservation."
📝 Committable suggestion
‼️ IMPORTANT
Carefully review the code before committing. Ensure that it accurately replaces the highlighted code, contains no missing lines, and has no issues with indentation. Thoroughly test & benchmark the code to ensure it meets the requirements.
| semantic_facts: | |
| dafny_property: INV_SPOOL_EVIDENCE_NOT_AUDIT_EVIDENCE | |
| spool_operation: OP_EXPORT | |
| spool_evidence_present: true | |
| audit_evidence_present: false | |
| audit_satisfied_by_spool_evidence: false | |
| semantic_facts: | |
| dafny_property: INV_SPOOL_EVIDENCE_NOT_AUDIT_EVIDENCE | |
| spool_operation: OP_EXPORT | |
| authorization_result: ALLOW_WITH_AUDIT | |
| audit_required: true | |
| spool_evidence_present: true | |
| audit_evidence_present: false | |
| audit_satisfied_by_spool_evidence: false |
🤖 Prompt for AI Agents
Verify each finding against the current code and only fix it if needed.
In `@tests/fixtures/job/spool-evidence-not-audit-0916.yml` around lines 27 - 32,
The fixture's semantic_facts state spool_evidence_present and
audit_evidence_present but do not encode that an audit is required, so the
negative case lacks grounding; update the semantic_facts (same block containing
dafny_property: INV_SPOOL_EVIDENCE_NOT_AUDIT_EVIDENCE and spool_operation:
OP_EXPORT) to explicitly assert the audit obligation for this path (e.g., add an
entry like audit_obligation: ALLOW_WITH_AUDIT or audit_required: true) so the
fixture reflects that the request is on an ALLOW_WITH_AUDIT path.
|
@codex pls review |
![chatgpt-codex-connector[bot]](https://avatars.githubusercontent.com/in/1144995?s=60&v=4){kind=small}
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: fe6f2c4917
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
| owner_principal: PRIN-MFOS-SPOOL-OWNER | ||
| subject_principal: PRIN-MFOS-SPOOL-OWNER | ||
| authorization_result: ALLOW | ||
| content_released: true |
There was a problem hiding this comment.
This newly C5-linked fixture marks content_released: true for INV_SPOOL_OWNER_BROWSE_ALLOWED, but the corresponding golden decision still carries AUDIT_SECURITY_DECISION while its audit record has before_return: false. The Dafny predicate reached by this fixture requires Audit.RequiredAuditSatisfiedForFinalResult before content can be returned, so this conformance row can now certify an owner-browse vector that does not satisfy the modeled audit precondition whenever the decision has an audit obligation.
Useful? React with 👍 / 👎.
| "INV_SPOOL_PURGE_WITHOUT_AUTHORITY_DENIED", | ||
| "Spool purge without an allowing authorization is fail-closed.", |
There was a problem hiding this comment.
This C5 row describes purge denial as fail-closed and its golden expects a failed final state plus a before-return audit record, but the mapped lemma only restates that a non-allowing OP_PURGE decision satisfies SpoolPurgeDeniedWithoutAuthority; it does not mention the bound spool entry, audit records, or !SpoolPurgeCanRemoveContent. As a result, the new traceability check can pass even if this scenario stops proving the no-purge/no-content effect that the fixture and oracle claim.
Useful? React with 👍 / 👎.
| "INV_SPOOL_SPEC_GAP_NOT_SUCCESS", | ||
| "SPEC_GAP is not a successful Spool access decision.", |
There was a problem hiding this comment.
The SPEC_GAP C5 row, and the analogous UNSUPPORTED row just below it, map to lemmas that only prove the result is not a valid allow decision, while the corresponding goldens assert FAILED with a specific error and a before-return security audit record. With only access_success required in the fixture facts, these rows can be validated as C5 without any Dafny property covering the fail-closed transition or audit-before-return behavior they claim.
Useful? React with 👍 / 👎.
| ValidCorrelationId(ctx.correlation_id) && | ||
| Authorization.DecisionWellFormed(decision) && | ||
| decision.subject == ctx.subject && | ||
| decision.object_ref.object_id == spool.spool_id && |
There was a problem hiding this comment.
When a spool id is reused or a purged/stale reference is presented with the same object_id but a different ObjectRef.generation/decision context generation, this predicate still treats the old decision as bound because it ignores the generation fields. The browse/export/purge success predicates all depend on BoundSpoolDecisionValid, so a stale authorization for a prior generation can satisfy the new protected-resource model even though the spool spec requires stale or purged refs to be rejected before content/effects.
Useful? React with 👍 / 👎.
1 participant
Scope
Phase 1.4.2 deepens only the Dafny executable semantics for Spool protected-resource behavior.
This PR covers:
What Changed
types.dfy.job_spool.dfy.evidence/traceability/generated/phase-1-4-2/.scripts/generators/generate-spool-coverage.pyandscripts/phases/phase-1/check-phase1-4-2-spool-coverage.py, with a thin root wrapper.206 verified, 0 errors.What Did Not Change
jobd,spoold, oroperatordimplementation.Dafny Verification Result
./scripts/validate-dafny-semantics.sh --require-dafnypassed with:Coverage Summary
C4_VERIFIED_PROPERTYC5_CONFORMANCE_LINKEDC5_CONFORMANCE_LINKEDC2_PARTIAL_SEMANTICC3_FULL_SEMANTICValidation
All required local validation commands passed:
./scripts/validate-all.sh --check./scripts/validate-naming-safety.sh release./scripts/validate-artifact-hygiene.sh./scripts/validate-component-scaffold.sh./scripts/validate-language-formal-assurance.sh./scripts/validate-dafny-semantics.sh --require-dafnypython3 scripts/check-semantic-coverage-mapping.pypython3 scripts/check-formal-claim-coverage.pypython3 scripts/check-phase1-gap-triage.pypython3 scripts/check-phase1-2-auth-audit-coverage.pypython3 scripts/check-phase1-3-dataset-catalog-coverage.pypython3 scripts/phases/phase-1/check-phase1-4-1-job-dd-coverage.pypython3 scripts/phases/phase-1/check-phase1-4-2-spool-coverage.pypython3 scripts/check-phase1-4-2-spool-coverage.pypython3 -m py_compile $(find scripts tools -name '*.py' -type f | sort)find scripts tools -type d -name __pycache__ -prune -exec rm -rf {} +./scripts/validate-artifact-hygiene.shgit diff --checkRed-Team Summary
No Critical or Major findings remain. Checked: browse without authorization, non-owner browse, purge without authority, export without audit, SpoolEvidence as AuditEvidence, cross-request replay, DENY success leakage, audit-obligation bypass, Python semantic leakage, operator/FVS scope creep, production daemon/Rust semantic-core boundary, and C4/C5 overclaim.
CodeRabbit Status
CodeRabbit advisory review is requested by opening this PR under the Phase 1 advisory policy. CodeRabbit remains advisory and is not a required merge gate.
Remaining Gaps
Real spool storage, SYSOUT/device behavior, operator command semantics, production service provenance,
spoold/jobd/operatord, Rust semantic-core, and hosted daemons remain out of scope and unimplemented.