Raised by the implementing agent: the design named only exits on the failing arm; if (can(x)) { op(); } is the
common shape and the operation is unreachable from the failing arm there too.
Co-Authored-By: Claude Fable 5.1 <[email protected]>
Requirement 10, the structural control-flow graph per function and CfgDominance behind the existing protocol,
tasks 4.4 and 4.5. Textual order stays the checker's default; the prover selects control flow.
Co-Authored-By: Claude Fable 5.1 <[email protected]>
The maintainer's correction: counts over a function, language or framework carry nothing about safety; the
object a decision model may see is the path from an attacker-reachable entry to a protected operation, with the
checks on it in control-flow order and the provenance of the operation's arguments. Requirement 9, the trace
contract and tasks 4.2 and 4.3.
Co-Authored-By: Claude Fable 5.1 <[email protected]>
Codex delivery under spec access-control-prover. `semantic/obligations/paths.py` builds entry-to-function path
records from the cached caller index; `mapping.py` names Stapler web methods and Jetty handlers as entries;
`check_obligations` gains the opt-in premise `assume_entries_protected` with the label `unguarded_path`;
`hunt/prover.py` proves a change with no model call and states its coverage; `benchmarks/valid/prover_arm.py`
scores it with the valid-benchmark metrics. Two fixes after the first smoke run: a product file git holds empty
is read, not unread (four changes failed on `__init__.py` and empty assets), and absent-input reasons are
counted by name.
Smoke on the 23 fix changes of the training pool: 7 pushes caught (30 percent, Wilson 16 to 51), 28 of 93
locations, precision 7 of 8 flagged, no instrument failure; three changes over the 120 second bound. Twelve of
the 17 Jenkins fixes reach the fixed method but check no operation because the method is the operation;
the spec now carries handler-named operations for delivery B.
Co-Authored-By: Claude Fable 5.1 <[email protected]>
Codex stopped on a real conflict: with path records and no clause or sibling norm the checker returns no finding
by design. The prover's premise (a recognised entry is protected unless declared public) is now an opt-in keyword
with its own label and evidence, default off, existing behaviour and tests unchanged.
Co-Authored-By: Claude Fable 5.1 <[email protected]>
A deterministic check that a protected operation is reachable from an entry point without a check dominating
the path, per framework, built on the existing obligations checker, caller index and entry mapper; scored as a
rule arm on the access-control training pool. Follows the maintainer's finding that the hunter's features
describe shape and cannot decide unsafety.
Co-Authored-By: Claude Fable 5.1 <[email protected]>
