Co-Authored-By: Claude Fable 5.1 <[email protected]> Claude-Session: https://claude.ai/code/session_01T7XD7x5KonMdmGRkp63EQG
14 KiB
Implementation Plan
-
1. Foundation: closed facts and obligation shapes
-
1.1 Load obligated operations and dischargers as closed facts
data/facts/obligations.tomlwith[[operation]](id, kind, language, calls, resource_arg, requires, sensitivity) and[[discharger]](id, kind, language, calls, decorators, identity_sources, constraint_params) for python, javascript, typescript;load_obligation_facts(dir)withfor_language;OPERATION_KINDS,DISCHARGER_KINDS,PROVENANCE_KINDSclosed.- Observable: the loader returns Python operation facts for ORM query and raw execute calls and discharger facts for
login_required, token validators anduser/owner_idconstraint params; a file naming kind"maybe_guard"or an unknown field raisesObligationFactsErrornaming the entry; no code path detects an obligation without a matching fact. - Requirements: 1.1, 1.2, 1.3, 1.4, 1.5
- Boundary: ObligationFacts
-
1.2 Derive obligation shapes from trusted pairs
ObligationShape(language, operation_kind, discharger_kind, provenance, resource_class, mechanism, family="obligation") with text-freekey(),to_dict(),from_dict();derive_obligationfinds the obligated operation in the labeled function on the vulnerable side and classifies the discharger the fixed side added together with the provenance of the value it binds (authenticated context, request input, constant) viavariants.source_kind_of_name-style tracing over the identity sources.- Observable: the
vampi-books-get-by-titlepair yieldsprotected_read/identity_constraint/authenticated_context/owned; a permissive-default pair yieldssecurity_setting/non_permissive_value/constant; a pair whose fixed side adds no discharger returns None with reasonno_discharger_added;key()contains no path, line or literal and is identical for renamed identifiers. - Requirements: 2.1, 2.3, 2.5
- Boundary: ObligationShapes
- Depends: 1.1
-
1.3 Export obligation shapes through the existing store and exporter
seed.pair_lessonsderives obligation shapes for rows carryingobligation; onlyseeded|reviewed, non-known-limit, parsing pairs seed; rows written withappend_from_pair(family in the shape dict,guard= discharger kind), deduped by key with accumulated pairs;obligation_mechanisms(records)selector; sink-shapesearch_treeignores obligation rows.- Observable:
ousast mechanisms export --slice vibe-pyreports the absence pairs that seeded and skips advisory/title/known_limit/parse-failed rows with reasons; two pairs with the same shape produce one row listing both;search_treeover a store holding only obligation rows searches 0 mechanisms. - Requirements: 2.1, 2.2, 2.4
- Depends: 1.2
-
2. Core: operations, dischargers, siblings, policy, dominance, checker
-
2.1 Find operations and discharge witnesses in a parsed file (P)
find_operations(ir, facts, ranges)returns operation sites with kind, fact id, enclosing function and resource token;find_discharges(ir, facts, flow_facts, ranges, entry)returns witnesses with kind, provenance and scope (decorator, router, statement, hop) using the entry point's decorators and the handler's binds.- Observable: a Flask fixture with three handlers yields three
protected_readoperations on resourcebook; the handler with@login_requiredyields apath_guarddecorator witness; the handler that bindsuserfromrequest.useryields anidentity_constraintwitness withauthenticated_context, and one binding fromrequest.argsyieldsrequest_input. - Requirements: 3.1, 5.4
- Boundary: Operations
- Depends: 1.1
-
2.2 Group sibling handlers and find consistency anomalies (P)
sibling_sets(entries, operations, discharges)keyed by (router or module, resource token);consistency_anomalies(sets, min_siblings)flags a handler that reaches an operation kind without a discharge its siblings perform; under-populated sets are counted, never reported; a public route among authenticated siblings is a missingpath_guardwith the access classification as evidence.- Observable: three
/bookshandlers where two constrain by owner produce one anomaly naming the two siblings; withmin_siblings = 4the same set produces none and is counted under-populated; anomalies never reference or alter existing findings. - Requirements: 3.1, 3.2, 3.3, 3.4, 3.5
- Boundary: Siblings
- Depends: 2.1
-
2.3 Load the declared policy with a closed schema (P)
load_declared_policy(path)reads version, identity_source,[[resource]](name, sensitivity, identity_field),[[route]](path, access, roles); unknown field or value raisesPolicyErrornaming it;version_hash; absent file returns None.- Observable: a valid file loads with its hash; a file with
access = "sometimes"or an extra key is rejected naming the field; the scan wrapper recordspolicy_invalidand continues. - Requirements: 4.1, 4.2
- Boundary: DeclaredPolicy
-
2.4 Dominance protocol with an order-based default (P)
Dominanceprotocoldominates(witness, operation, path);OrderDominance: decorator and router witnesses dominate the handler; a statement witness dominates when it precedes the operation with an early exit between them or is a guard call; along aPathRecorda witness on an earlier hop dominates.- Observable: a guard call before the operation with a
returnin between dominates; the same call after the operation does not; a witness on hop 1 of a stubPathRecorddominates an operation on hop 3; the checker accepts any object implementing the protocol. - Requirements: 5.1, 5.2
- Boundary: Dominance
-
2.5 The obligation checker: path-aware and function-local
check_obligations(irs, entries, facts, flow_facts, policy, paths, dominance, store_shapes, min_siblings)→ObligationResult; reached = a path ends at the operation or (no paths) the operation's function is an entry point; label precedence declared > consistency >function_local; a declared public route suppressespath_guardobligations for that route only;known_fixfrom a matching store shape; identity constraints bound from request input are reported with that provenance;findings_to_staticemitsobligation:<kind>:<path>:<line>atsuspicionwith tagsobligation:*,discharger:*,obligation_evidence:*.- Observable: the three-handler fixture without paths yields one finding labeled
consistency_violationnaming the missingidentity_constraintand both siblings with afunction_local-mode degradation recorded once; with a declared protected resource the label becomesdeclared_policy_violationnaming the clause; a declared public route removes the guard finding but keeps the identity one; with a stub path whose earlier hop discharges, no finding; evidence level is alwayssuspicion. - Requirements: 3.6, 4.3, 4.4, 5.1, 5.2, 5.3, 5.4, 6.1
- Depends: 2.2, 2.3, 2.4
-
3. Integration: scan, reports, ranking, intent
-
3.1 Run the checker in MAP with config and manifest counters
[obligations] enabled=true, min_siblings=3, policy_path; MAP runs_check_obligationsafter variant search in standard and deep only, withPathRecords when the reachability artifact is present andOrderDominanceotherwise; findings appended; manifestobligations = {sibling_sets, under_populated, operations, findings_by_label, policy_version, degradations}; obligation findings never enter the sandbox candidate set.- Observable: a standard scan of the fixture writes one
obligation:finding and the manifest block withpolicy_version: null; quick has neither; with a policy file the block carries its hash; the deep scan's verdicts contain no obligation finding. - Requirements: 4.1, 5.3, 5.5, 6.5
- Depends: 2.5
-
3.2 Reports and ranking name the obligation (P)
- Markdown lines
Obligation,Missing discharger,Evidence,Known fix,Intentper finding and a## Obligationssection (sibling sets, policy version); SARIFobligation_*properties;rankweight = sensitivity x label weight (declared > consistency > function_local), capped strictly below the lowest sandbox-proven finding. - Observable: the fixture's report shows the missing
identity_constraint, the two siblings and the known fix learned from the pairs; SARIF carries the properties withevidence_level = "suspicion"; in a run with one sandbox-proven finding the obligation finding ranks below it; reports without obligations are unchanged. - Requirements: 6.1, 6.2, 6.4
- Boundary: reports, rank
- Depends: 2.5
- Markdown lines
-
3.3 Hunter adjudicates intent without raising evidence (P)
- When the hunter client resolves, ask one closed question per route-bearing finding ("is this route meant to be public?") with redacted handler text and sibling names; record
intentand the rationale; absent client →intent_adjudication_unavailableonce; the label and evidence level never change. - Observable: with a scripted client answering
public, the finding's rationale carries the adjudication and its label is unchanged; without a client the degradation appears once and findings are identical. - Requirements: 6.3
- Boundary: IntentAdjudication
- Depends: 2.5
- When the hunter client resolves, ask one closed question per route-bearing finding ("is this route meant to be public?") with redacted handler text and sibling names; record
-
4. Corpus: absence pairs with context, labels, leave-one-out
-
4.1 Harvest mode
handler_contextand theobligationlabel (P)- Harvest library mode keeping the labeled function with its decorators and the registration statements naming it on both sides;
ExpectedFinding.obligationadditive; the pair scorer counts a finding taggedobligation:<kind>inside the labeled function as a detection for obligation-labeled rows; vocabulary gainsunconstrained_protected_read,unconstrained_protected_write,unguarded_privileged_action; loader rejects unknown obligation kinds. - Observable: harvesting a fixture handler keeps
@app.routeand@login_requiredin the excerpt; a catalog row withobligation = "protected_read"loads and is detected by an obligation finding in its function; a row withobligation = "guess"is rejected; existing catalogs load unchanged. - Requirements: 7.1, 7.2, 7.3
- Boundary: harvest, pairs
- Harvest library mode keeping the labeled function with its decorators and the registration statements naming it on both sides;
-
4.2 Leave-one-out per obligation kind
loo.score_pair_with_storerunscheck_obligationson both sides for obligation rows with the held-out store's obligation shapes;per_obligation_kindmetrics;found_bynames the shape record that suppliedknown_fix;pairs --loopayload and roadmap table gain the obligation kinds.- Observable: a three-pair toy slice (two teach
protected_read/identity_constraint, one teachessecurity_setting) reports the identity pairs found by each other and the setting pair unfound; the real vibe-py and agent-vfc absence pairs report a baseline per kind; the roadmap table row is present and no gate reads it. - Requirements: 7.4, 7.5
- Depends: 1.3, 2.5, 4.1
-
4.3 Relabel and re-harvest the corpus absence pairs
- vibe-py and agent-vfc rows whose mechanism is an absence kind gain
obligation; the agent-vfc absence rows are re-harvested inhandler_contextmode (pointer rows through the cache); catalogs regenerated idempotently; nothing unlicensed vendored. - Observable:
mechanisms exportseeds at least one obligation shape from vibe-py; the vendored catalogs still load with unchanged vendored counts; gates unchanged. - Requirements: 7.2, 7.5
- Depends: 4.1
- vibe-py and agent-vfc rows whose mechanism is an absence kind gain
-
5. Integration: the obligations lever
-
5.1 Validator dispatch on shape family and pending policy clauses
validate_mechanismdispatches onshape["family"]: obligation rows check operation kind, discharger kind, provenance and resource class against the closed sets;PolicyClauseEdit(kind, fields, evidence, rationale)validated against the policy schema and journaled underpending_policy_clauses, never applied.- Observable: an obligation row with
discharger_kind = "if user"is rejected; a valid row admits; a clause edit lands in the journal as pending and a following scan reads no policy from it. - Requirements: 4.5, 8.1, 8.2, 8.4, 8.5
- Boundary: Lever
- Depends: 1.3
-
5.2 Propose obligation admissions and retractions under the existing gate
propose_mechanism_editstreats obligation rows like sink rows (a trial store recovers a missed holdout absence pair without leaking → admit; an admitted row firing on a fixed twin → retract);evaluate_mechanism_profilesruns the checker for obligation rows; rejection reverts the store byte for byte; journal carries pair or sibling provenance and metrics before and after.- Observable: a scripted admission that recovers a holdout absence pair is accepted and persisted; one that fires on a fixed twin is rejected with
mechanism_leakand the store unchanged;ousast improvepicks obligation candidates up from the same candidates file. - Requirements: 8.3, 8.5
- Depends: 5.1, 4.2
-
6. Validation
-
6.1 Prove offline tests and unchanged gates
- Every component unit-tested on local fixtures; semantic-marked tests skip without the extra; detection, map and local pair gates unchanged; extra-free suite green; no test needs network, model or sandbox.
- Observable: both pytest matrices green; gate stdout byte-identical to the pre-spec commit; a network-blocked run of the obligation tests passes.
- Requirements: 9.1, 9.2, 9.3
- Depends: 3.1, 3.2, 3.3, 4.3, 5.2
Implementation Notes
- Requirements approved 2026-09-05, design approved 2026-09-05 (maintainer, in session).
- Path-aware evaluation (5.1) is wired through the
Dominanceprotocol and an optionalPathRecordinput; untilreachability-flow-modellands, every run is function-local by construction and tests use a stubPathRecord. No task here waits on the upstream specs. - Sibling grouping keys on (router or module, resource token). If the maintainer prefers data-model-only grouping, only task 2.2 and its tests change.