Repository navigation
P5b: Verification part 2 — INV-FUNC-001 reachability, P5 gate evidence - #22
Merged
Merged
Conversation
Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com>
…146) One missing address in the middle, the first or the last address uncovered, a single-address member at the cursor, consecutive single-address members tiling a network, and order and duplicates, for IPv4 and IPv6. Tests only; nothing under core/ changes. Scratch-copy proof (outside the repository): the three mutants named in the P5a verdict (first > cursor + 1; return cursor >= wanted.last; member.last > cursor) all survive the 12 existing verification test files (396 tests) and are all killed by the new tests. Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com>
…s, R17 self-test for the new modules (registry §6; C-151 to C-154) C-151 boundary, entry and parameters; C-152 endpoint resolution across moves and indeterminate endpoints; C-153 rows 1 to 9 and the definitions they need (src_sg, self, partly covers, could satisfy, ADDR(S), M3, the R5 cases); C-154 assumptions, observations and the baseline list. Ten closed reason codes are added to the vocabulary. The R17 self-test names the two modules that step 3 and 4 add; it fails when R17 is broken (shown in a scratch copy). Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com>
… §6.6; C-151, C-153) func_view.py reads instance, database, subnet, VPC, group VPC and route table from the stored C-112 encoding into frozen views. A fact is absent, known, unknown or unsupported; a stored shape that cannot be read is a ViewError, never absent; a placeholder keeps its support status so it is not mistaken for a resource without the argument. Routes carry a destination state and a local/other/unresolved target; interface blocks and propagating_vgws are read as presence. Tests first (module not found), including every functional resource of every fixture. 13 deliberate breakages checked; two survivors got tests. Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com>
….4, §8; C-151 to C-154) reachability.py implements E1 to E7 and the first-row-wins table of §6.4: endpoints followed across moves through the identity report (a deleted one is absent, an uncertain or placeholder one is indeterminate), every row 2 cause collected and reported, rows 3 to 5 on resolved values only, E5 and E6 per rule, and rows 7 to 9 with "could satisfy" and "partly covers" as C-153 defines them. Vectors F1 to F20 are tests with the derivation written before the predicate. Shared code extended for it (SEC results unchanged, whole SEC suite rerun): views.group_is_mixed, retention.inline_retention with a direction, Rule.sources_unresolved / self_unresolved (a reference is a resolved source: values.has_unresolved), cidr.overlaps. A rule in an UNRESOLVED:* pseudo-group is determinate but may belong to a group of the side: a bug found by the tests and fixed before this commit. 26 deliberate breakages were each caught. C-153 corrected to per-rule coverage. Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com>
…aseline list, replace the interim assertions (registry §2.7, §6.7; C-151, C-154) dail.verify.reachability_cfg v1 is in DEFAULT_VERIFIERS; a pair the table does not have is still UNSUPPORTED verifier.not_available (one test keeps that, with the pair removed). A created resource of any of the 26 relevant-unsupported types is UNSUPPORTED in the baseline. The interim "FUNC is UNSUPPORTED" assertions are replaced by stronger ones: the engine's FUNC result of all 20 fixtures equals expected.json, the aggregate over all four invariants follows expected.json, the safe repair aggregates to PASS and the repair that breaks the database path to FAIL from the engine's own records, and without the functional result nothing passes. The cost metric now counts the functional verifier (6 runs on a full work set, not 5). Tests first: the rewritten tests were shown failing before the verifier was registered. Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com>
…pers (registry §6.3, §6.4; Doc 15 §12.2; C-151 to C-154) test_reachability_properties.py: all 270 configurations of a determinate family against an oracle written in the test (plain ipaddress arithmetic, hand-derived in its docstring), then seeded random properties (order independence; added permission is monotone; irrelevant types change nothing; anything outside the model is UNSUPPORTED; indeterminate, partial or unsupported input is never a PASS), and demonstrations that each checker fails on a broken verifier. test_p5_gate_probes.py: (a) the unresolved direction form, (b) every verifier fault is VERIFIER_ERROR for each of the three verifiers, (c) stale hashes and versions are never sufficient, (d) the canonical scenario through the real fixtures: PASS and FAIL. Mutation checks (scratch copy outside the repository): 36 breakages of the functional verifier, the dispatch table, the baseline list and the boundary, all caught. Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com>
…eaves to v1.1 (registry §6.3, §6.4; C-150 to C-154) Twelve points that the registry text does not decide and that this package settled conservatively (R5): E2 in row 4, the "it" of row 7, "could satisfy", the UNSUPPORTED endpoint resource, rules of unknown direction, pseudo-groups, literal ids, M1, M3, per-rule coverage, the src_sg of an egress rule and ADDR(S). Open until the authors decide. Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
P5b — Verification part 2: INV-FUNC-001 reachability, P5 gate evidence
Implements
dail.verify.reachability_cfgv1 per registry §6 (E1–E7, rows 1–9), registers it in the dispatch table, extends the baseline relevant-unsupported list to the 26 FUNC types, replaces the interim FUNC assertions, and adds the P5 gate evidence tests. Step 0 records the P5a verdict indocs/PHASE_GATES.md; step 1 adds the CIDR boundary tests from the P5a carry-forward.Process (C-28): do not merge until the external review verdict is pasted into this PR. This description contains no verdict.
Decisions register
Evidence (from the P5b report)
dev.py testOK on 3.12 (skipped=1) and 3.14 (skipped=2); black, ruff, mypy clean; pytest exit 0 (3487 collected, 1 skipped); fresh-clonedev.py bootstrapexit 0.expected.jsonin every cell.🤖 Generated with Claude Code