Open_Ultra_SAST/.kiro/specs/access-control-prover/tasks.md

# Implementation Plan

## Completed baseline

The completed work below produced the immutable 2026-10-28 development baseline. Amendment tasks 7-13 replace
its final resolution, dominance, fact-acquisition and measurement semantics without erasing the evidence.

- [x] 1. Baseline paths and checker premise
- [x] 1.1 Add bounded caller-index paths with concrete hop records
  - Delivered depth/fan-out traversal, entry stopping, file-qualified hops and unreached targets.
  - Baseline fixtures cover depth, fan-out, deduplication and multiple same-name files.
  - The final call semantics are superseded by tasks 8-9.
  - _Requirements: 3.1, 3.9, 3.10_
  - _Boundary: Concrete Paths_
- [x] 1.2 Add the opt-in recognised-entry-is-protected premise
  - Existing checker defaults remain unchanged; prover evidence identifies the premise.
  - _Requirements: 4.6_
  - _Boundary: Obligation Checker_

- [x] 2. Baseline entry recognition
- [x] 2.1 Add the first Java entry recognisers and evidence
  - Delivered development cases for declared web methods, servlets, resources and handlers.
  - _Requirements: 1.1, 1.5_
  - _Boundary: Mapping_
- [x] 2.2 Add the initial PHP, JavaScript, TypeScript and Python entry recognisers
  - Delivered positive and negative fixture coverage with entry evidence.
  - _Requirements: 1.1, 1.5_
  - _Boundary: Mapping_

- [x] 3. Baseline enforcement and operation facts
- [x] 3.1 Add route-, declaration- and policy-scoped enforcement witnesses
  - Delivered initial external-handler witnesses and integration fixtures.
  - _Requirements: 2.2, 2.4_
  - _Boundary: Enforcement Adapter_
- [x] 3.2 Close the unfinished per-target fact inventory as superseded
  - The partially completed inventory is not treated as complete implementation.
  - Tasks 11.3-11.7 replace it with label-blind acquisition and promoted target knowledge.
  - _Requirements: 2.1, 2.2, 2.9, 2.10_
  - _Boundary: Target Knowledge_
- [x] 3.3 Add handler-named operation facts
  - Delivered opt-in handler operations at declaration lines for recognised entries.
  - _Requirements: 2.3_
  - _Boundary: Fact Interpreter_

- [x] 4. Baseline prover, traces and structural control flow
- [x] 4.1 Integrate entries, paths, operations and witnesses in the deterministic prover
  - Delivered hunt-defect findings and failure-visible baseline coverage with no model calls.
  - Final three-way judgment is superseded by task 10.6.
  - _Requirements: 4.7_
  - _Boundary: Prover Integration_
- [x] 4.2 Emit deterministic ordered traces and local argument provenance
  - Delivered canonical text/JSON traces for discharged and unguarded baseline pairs.
  - _Requirements: 9.1, 9.2, 9.3, 9.5_
  - _Boundary: Canonical Trace_
- [x] 4.3 Attach traces to prover records and findings
  - Delivered trace references through the replay envelope.
  - _Requirements: 8.1, 9.7_
  - _Boundary: Prover Integration_
- [x] 4.4 Build structural control-flow graphs
  - Delivered branches, loops, exits, exception regions, dominators and control context.
  - _Requirements: 10.1, 10.2, 10.3, 10.4_
  - _Boundary: Structural CFG_
- [x] 4.5 Add baseline CFG dominance and guard effects
  - Delivered value-only rejection and control-context trace fields.
  - Strict unknown semantics are superseded by task 10.1.
  - _Requirements: 10.1, 10.2, 10.3, 10.4, 10.5_
  - _Boundary: CFG Dominance_

- [x] 5. Baseline replay arm
  - Delivered checkpointed records, standard metrics, coverage tables, zero-byte refusal and immutable records.
  - _Requirements: 5.1, 5.2, 5.4, 5.6_
  - _Boundary: Development Runner_

- [x] 6. Baseline development measurement
  - Measured 23 repositories and 483 changes: 65.2% fix-push recall, 15.0 flagged ordinary pushes per 100,
    0 instrument failures; recorded at benchmarks/measurements/2026-10-28-access-control-prover/.
  - The population is development evidence only and remains immutable.
  - _Requirements: 5.2, 5.7, 12.9_
  - _Boundary: Development Measurement_

## Amendment implementation

- [ ] 7. Abstract evidence foundation
- [x] 7.1 Implement the evidence-relation algebra and completeness value
  - Encode the specified precision order, complete join table, dimension conjunction and witness aggregation.
  - Preserve every incompleteness reason deterministically and deduplicate reasons without losing stage identity.
  - Done when exhaustive table tests and algebraic law tests pass for every relation pair.
  - _Requirements: 11.1, 11.6, 11.7_
  - _Boundary: Abstract Evidence Domain_
- [x] 7.2 Add resource abstract values and operation-fact fields
  - Represent exact resources, finite alias sets, request-global scope and unknown resources.
  - Extend operation facts to state when a request-global guard is sufficient.
  - Done when resource parsing and joins distinguish exact, alias, global and unknown fixtures.
  - _Requirements: 2.1, 2.5, 2.6, 2.7, 11.1_
  - _Boundary: Resource Domain_
  - _Depends: 7.1_
- [x] 7.3 Add authority abstract values and promoted implication facts
  - Represent exact, finite and unknown authorities separately from resources.
  - Load authority implications from promoted facts and retain the supporting fact identifier.
  - Done when sufficient, insufficient and unknown authority fixtures produce the specified relations.
  - _Requirements: 2.1, 2.2, 2.5, 2.7, 2.8, 11.1_
  - _Boundary: Authority Domain_
  - _Depends: 7.1_
- [x] 7.4 Extend judgment, trace and coverage contracts with abstract state
  - Add three-way judgments, completeness and evidence relations without changing legacy defaults.
  - Add canonical serialization for resource and authority relations and all incompleteness reasons.
  - Done when old trace fixtures remain stable in legacy mode and new fixtures round-trip all abstract fields.
  - _Requirements: 7.1, 7.2, 7.5, 7.6, 9.1, 9.2, 9.6_
  - _Boundary: Judgment Contracts, Canonical Trace_
  - _Depends: 7.1, 7.2, 7.3_

- [ ] 8. Stable symbols and conservative call resolution
- [x] 8.1 Capture call receiver and arity evidence in the semantic IR
  - Preserve receiver expression and argument count for supported syntax while keeping existing constructors valid.
  - Done when language fixtures retain receiver and arity evidence without regressing existing IR consumers.
  - _Requirements: 3.2, 3.3_
  - _Boundary: Semantic IR_
- [x] 8.2 Build stable declaration identities and the per-change symbol index
  - Identify declarations by module, enclosing type, name and available signature.
  - Cache the symbol and inheritance indexes on the per-change context.
  - Done when duplicate type names, same-name methods and overloads receive stable distinct identities.
  - _Requirements: 3.2, 3.5, 6.2_
  - _Boundary: Symbol Index_
  - _Depends: 8.1_
- [x] 8.3 Resolve exact, finite-candidate and unresolved call targets
  - Return complete exact targets, incomplete finite candidate sets, or unresolved results with reasons.
  - Remove global bare-name fallback from prover-mode resolution.
  - Done when ambiguity never merges methods and unresolved calls cannot produce complete paths.
  - _Requirements: 3.3, 3.4, 11.1, 11.6_
  - _Boundary: Call Resolution_
  - _Depends: 8.2_
- [x] 8.4 Resolve inheritance and base-declaration attachment
  - Attach base operations and entries only through repository-defined descendant relations.
  - Preserve ambiguous inheritance as incomplete rather than projecting to unrelated routes.
  - Done when subclass and unrelated-class fixtures produce distinct attachments and judgments.
  - _Requirements: 3.5_
  - _Boundary: Call Resolution_
  - _Depends: 8.2, 8.3_

- [ ] 9. Interprocedural summaries and concrete paths
- [ ] 9.1 Extract local function summaries
  - Collect each function's operations, witnesses, resolved calls and local completeness without traversing callers.
  - Done when summaries are deterministic and contain no target names outside fact identifiers.
  - _Requirements: 3.1, 3.6, 11.7_
  - _Boundary: Function Summaries_
  - _Depends: 7.4, 8.3_
- [ ] 9.2 Compute monotone summaries over recursive call components
  - Iterate finite summary sets over strongly connected components until stable.
  - Done when direct recursion and mutual recursion terminate with stable accumulated evidence.
  - _Requirements: 3.7, 11.6_
  - _Boundary: Function Summaries_
  - _Depends: 9.1_
- [ ] 9.3 Add summary caches and explicit exploration cutoffs
  - Reuse summaries per change and carry depth, fan-out, deadline and other cutoff reasons into completeness.
  - Done when each cutoff fixture returns accumulated evidence plus the exact incomplete reason.
  - _Requirements: 3.8, 6.2, 6.3, 7.2_
  - _Boundary: Function Summaries, Context Cache_
  - _Depends: 9.2_
- [ ] 9.4 Materialise exact evidence paths from summaries
  - Emit concrete entry-to-operation hops only through exact target edges.
  - Preserve every complete chain independently and retain candidate-edge diagnostics separately.
  - Done when guarded and unguarded paths to one operation remain separate and candidate edges never complete a path.
  - _Requirements: 3.9, 3.10, 11.4, 11.5_
  - _Boundary: Concrete Paths_
  - _Depends: 9.3_

- [ ] 10. Strict authorization judgment
- [ ] 10.1 Return abstract dominance relations without prover fallback
  - Return MUST, MAY, NO or UNKNOWN with guard effect and control context.
  - Keep legacy order dominance unchanged, but return UNKNOWN in prover mode for unavailable graphs or line mappings.
  - Done when no prover fixture is discharged or flagged solely through textual-order fallback.
  - _Requirements: 10.1, 10.2, 10.3, 10.4, 10.5, 10.6, 10.7_
  - _Boundary: CFG Dominance_
  - _Depends: 7.1_
- [ ] 10.2 Match witness kind, scope and resource
  - Apply request-global sufficiency only when the operation fact declares it.
  - Return NO for definite mismatch and UNKNOWN for unresolved resource compatibility.
  - Done when same-resource, alias, global, mismatch and unknown fixtures match the design algebra.
  - _Requirements: 2.1, 2.2, 2.5, 2.6, 2.7, 11.1_
  - _Boundary: Witness Matcher_
  - _Depends: 7.2, 10.1_
- [ ] 10.3 Match authority and promoted implications
  - Apply only promoted authority implications and preserve their evidence.
  - Return NO for insufficient authority and UNKNOWN when compatibility cannot be decided.
  - Done when stronger, weaker, unrelated and unknown authorities produce the expected relations.
  - _Requirements: 2.2, 2.5, 2.7, 2.8, 11.1_
  - _Boundary: Witness Matcher_
  - _Depends: 7.3, 10.1_
- [ ] 10.4 Compute one judgment per complete or diagnostic path
  - Conjoin witness dimensions, aggregate witnesses per obligation and apply the mixed-obligation rule.
  - Emit discharged only for all-MUST, indeterminate for any MAY/UNKNOWN, and unguarded for at least one NO.
  - Done when MUST/NO, MAY/NO, UNKNOWN and empty-witness fixtures match the specified truth table.
  - _Requirements: 4.1, 4.2, 4.3, 11.2, 11.3, 11.4_
  - _Boundary: Pair Judgment_
  - _Depends: 10.2, 10.3_
- [ ] 10.5 Aggregate multiple paths in the opt-in checker mode
  - Return unguarded if any complete path is unguarded, discharged only for complete all-discharged enumeration,
    and indeterminate otherwise.
  - Keep the legacy checker API and defaults unchanged.
  - Done when mixed guarded, unguarded and incomplete path sets produce the specified aggregate.
  - _Requirements: 3.10, 4.1, 4.2, 4.3, 4.4, 4.5, 11.5_
  - _Boundary: Obligation Checker_
  - _Depends: 9.4, 10.4_
- [ ] 10.6 Integrate three-way judgments into the prover
  - Emit hunt findings only for unguarded pairs and send no indeterminate pair to the proof arm.
  - Carry all judgments, completeness reasons, resources, authorities and stable identifiers in traces and coverage.
  - Record stage-specific exceptions without folding them into quiet coverage.
  - Done when end-to-end fixtures distinguish unguarded, discharged and indeterminate records and findings.
  - _Requirements: 4.4, 4.5, 4.6, 4.7, 7.1, 7.2, 7.3, 7.4, 7.5, 7.6, 8.1, 8.2, 8.3, 9.1, 9.2, 9.3, 9.4, 9.5, 9.6, 9.7_
  - _Boundary: Prover Integration, Canonical Trace_
  - _Depends: 7.4, 9.4, 10.5_

- [ ] 11. Target knowledge registry and acquisition
- [ ] 11.1 (P) Add the entry-recognition strategy registry
  - Route mapping dispatch through one registry without embedding target names in engine modules.
  - Done when a fixture strategy registers, runs and records its strategy identifier and evidence.
  - _Requirements: 1.1, 1.5, 1.7_
  - _Boundary: Mapping Registry_
  - _Depends: 7.1_
- [ ] 11.2 Add the generic call-site registration strategy
  - Resolve repository-defined registered handlers through stable symbols and return unresolved registration coverage.
  - Done when exact and unresolved registration fixtures produce entries or coverage respectively.
  - _Requirements: 1.2, 1.3, 1.4, 1.5, 1.6_
  - _Boundary: Registration Adapter_
  - _Depends: 8.4, 11.1_
- [ ] 11.3 (P) Extract existing target knowledge into candidate records
  - Read legacy recognition strategies and current facts without changing promoted outputs.
  - Done when extraction produces deterministic candidate records with source/version/region evidence.
  - _Requirements: 2.9_
  - _Boundary: Fact Initialization_
  - _Depends: 7.1_
- [ ] 11.4 Verify and promote proposed target knowledge
  - Accept source- or approved-documentation proposals, reject contradictions, and write only verified outputs.
  - Done when matching proposals promote and contradicted or evidence-free proposals leave promoted knowledge unchanged.
  - _Requirements: 2.9, 2.10_
  - _Boundary: Fact Initialization_
  - _Depends: 11.3_
- [ ] 11.5 Record acquisition provenance and enforce label-isolated mode
  - Persist input revision, evidence digest, accepted/rejected proposals and output digest.
  - Reject admission acquisition inputs containing vulnerability, fix-location or ordinary-change labels.
  - Done when changed output after labels are opened marks the population spent.
  - _Requirements: 12.1, 12.2, 12.3_
  - _Boundary: Fact Initialization, Admission Guard_
  - _Depends: 11.4_
- [ ] 11.6 Migrate one legacy recogniser through the registry
  - Move one development-evidence family out of inline dispatch without changing its entries.
  - Done when old fixtures stay stable and inline target-specific matching is removed for that family.
  - _Requirements: 1.1, 1.7_
  - _Boundary: Mapping Registry_
  - _Depends: 11.1_
- [ ] 11.7 Run the first label-blind development acquisition
  - Produce registration, handler-operation, enforcement, resource and authority knowledge through the gate.
  - Treat the output as development data and record its acquisition digest; do not encode names in engine modules.
  - Done when promoted outputs load, rejected proposals have reasons, and the old unfinished task 3.2 has no residue.
  - _Requirements: 2.1, 2.2, 2.3, 2.4, 2.5, 2.6, 2.7, 2.8, 2.9, 2.10, 5.7, 12.9_
  - _Boundary: Target Knowledge_
  - _Depends: 10.3, 11.2, 11.5, 11.6_

- [ ] 12. Development and admission runners
- [ ] 12.1 Materialise and verify baseline and candidate analyzer bundles
  - Resolve analyzer revisions, fact sets, acquisition records and configurations to immutable digest-verified inputs.
  - Refuse comparison when any bundle artifact is unavailable or mismatched.
  - Done when the immutable baseline and a fixture candidate bundle can be reconstructed exactly.
  - _Requirements: 5.1, 5.5, 12.1_
  - _Boundary: Run Manifests_
- [ ] 12.2 Add record provenance, stage funnel and judgment transitions
  - Persist analyzer, fact, acquisition, configuration, population and input digests per record.
  - Summarise every analysis stage, completeness reason and transition between compared judgments.
  - Done when a fixture run accounts for every record from entry recognition through final judgment.
  - _Requirements: 5.1, 5.3, 5.4, 7.1, 7.6, 9.7, 11.8_
  - _Boundary: Development Runner_
  - _Depends: 10.6, 12.1_
- [ ] 12.3 Enforce instrument and hard runtime gates
  - Preserve zero-byte and stale-anchor refusal and add stage-aware deadline records.
  - Fail the run if any measured change exceeds 120 seconds; never summarize the overrun as a passing result.
  - Done when zero-byte, stale-anchor, deadline and 121-second fixtures all refuse the summary.
  - _Requirements: 5.6, 6.1, 6.3_
  - _Boundary: Runner Gates_
  - _Depends: 12.2_
- [ ] 12.4 Register the four-arm development comparison
  - Run baseline/candidate analyzer crossed with baseline/candidate facts over identical inputs.
  - Report metric deltas, stage-funnel deltas and judgment transitions without admission language.
  - Done when fixture arms isolate a fact-only lift from an analyzer-only lift.
  - _Requirements: 5.2, 5.5, 5.7, 11.8_
  - _Boundary: Development Runner_
  - _Depends: 12.1, 12.2, 12.3_
- [ ] 12.5 Consume and validate an externally reviewed admission manifest
  - Accept only a manifest produced by valid-detection-benchmark with review, isolation and immutable digest fields.
  - Reject label exposure, changed acquisition output or a spent population.
  - Done when valid, malformed, exposed and spent manifests produce deterministic accept/refuse results.
  - _Requirements: 12.1, 12.2, 12.3, 12.6, 12.8_
  - _Boundary: Admission Runner_
  - _Depends: 11.5, 12.3_
- [ ] 12.6 Add paired scoring and the admission report
  - Score vulnerable/fixed twins, reviewed ordinary changes, indeterminate rate, coverage, runtime and instruments.
  - Preserve sample counts and uncertainty intervals and return NO-GO on any pre-registered gate failure.
  - Done when fixture pairs detect vulnerable-only, fixed-side regression and mislabeled-negative cases.
  - _Requirements: 5.2, 12.4, 12.5, 12.7, 12.8, 12.9_
  - _Boundary: Admission Runner_
  - _Depends: 12.5_

- [ ] 13. Cross-cutting validation and measurements
- [ ] 13.1 Validate abstract-domain and metamorphic laws
  - Cover the full join table, conjunction, witness aggregation, monotonicity and mixed-obligation rule.
  - Prove that type renaming preserves a judgment and adding ambiguity can only preserve it or make it indeterminate.
  - Done when property and fixture tests pass deterministically across repeated runs.
  - _Requirements: 11.2, 11.3, 11.4, 11.5, 11.6, 11.7_
  - _Boundary: Abstract Evidence Validation_
  - _Depends: 10.5_
- [ ] 13.2 (P) Validate cross-component analysis scenarios
  - Exercise helper guards, registration entries, base attachment, resource mismatch, authority insufficiency,
    ambiguous calls, unavailable CFGs, recursion and budget cutoff.
  - Done when every scenario yields the expected trace, coverage reasons and three-way judgment.
  - _Requirements: 1.1, 1.2, 1.3, 2.1, 2.2, 2.5, 2.7, 3.4, 3.5, 3.6, 3.7, 3.8, 4.1, 4.2, 4.3, 10.6_
  - _Boundary: Prover Integration Validation_
  - _Depends: 10.6, 11.7_
- [ ] 13.3 Run the four-arm development regression
  - Run all four registered arms on the immutable current development population after proving nonzero input reads.
  - Publish analyzer/fact attribution, stage funnel, three-way judgments, budget result and comparison to the
    2026-10-28 baseline; label the result development-only.
  - Done when all arm records and summary digests are complete and no admission claim appears.
  - _Requirements: 5.1, 5.2, 5.3, 5.4, 5.5, 5.6, 5.7, 6.1, 7.3, 11.8, 12.9_
  - _Boundary: Development Measurement_
  - _Depends: 12.4, 13.1, 13.2_
- [ ] 13.4 Run admission from an externally prepared untouched manifest
  - Consume a reviewed manifest from valid-detection-benchmark after analyzer and facts are frozen.
  - Verify label isolation, paired vulnerable/fixed behavior, reviewed ordinary labels and every admission gate.
  - Done when the report returns an evidence-backed GO or NO-GO without modifying facts, strategies or thresholds.
  - _Requirements: 12.1, 12.2, 12.3, 12.4, 12.5, 12.6, 12.7, 12.8, 12.9_
  - _Boundary: Admission Measurement_
  - _Depends: 12.6, 13.3_

## Task constraints

- Complexity: McCabe at most 10 per touched function, at most 50 logical lines per function and 400 per new module.
- Engine/target split: abstract-domain, resolution, summary, judgment and trace modules contain no target names.
- Target knowledge: names enter only through promoted facts or registered target-aware strategies.
- Compatibility: legacy checker defaults and completed baseline records remain unchanged.
- Instrument rule: validation must prove nonzero input reads before interpreting any clean or zero result.

## Baseline implementation record

- Deliveries A-C implemented the baseline paths, recognisers, witnesses, handler facts, prover, traces and CFG with
  static checks and focused tests passing at delivery time.
- The full development arm then processed all 483 changes with zero instrument failures. Its maximum runtime exceeded
  the amended hard budget, so the baseline is evidence, not an eligible arm.
- The 2026-10-28 ablation identified call resolution, resource/authority precision and failure visibility as the
  amendment levers. Those observations inform tasks 7-13 but are not admission labels.