Slice 34 third-party OSS recon: relational/dataflow is the demand-validated next lever

[TSavo]

Slice 34 recon finding

Read-only third-party Rust OSS recon ran the kit end-to-end on external code with no kit/source changes.

Milestone

• External smoke test passed on itoa.
  • Scratch: /home/tsavo/remote/provekit-oss-recon/slice34-phase-a-clean-20260603054425
  • Prove exited 0: totalCallsites=2, discharged=10, violations=0, falsePass=0, loadErrors=[].
• Phase B ran on version-compare 0.2.1 with the rust-std shim catalog imported.
  • Scratch: /home/tsavo/remote/provekit-oss-recon/slice34-phase-b-version-compare-20260603055537
  • PROVEKIT_LINKERD_BIN pinned to /home/tsavo/remote/provekit-bcargo-d17ab89f79d4/provekit/implementations/rust/target/debug/provekit-linkerd.
  • Crate tests passed: 30 + 26.
  • falsePass=0 on real external code.

Coverage reality

Target bundle: blake3-512:28f6b1cf92b9986e55a56e927aa34bd0e620beb28604b03e1dfea514babf34f08fbc7fb6a8c6e2d8055414e00730437b605700bc14776375e5fca35da19685c4.

• Target rows: 139.
• Discharged: 32 (~23%).
• Open: 107 (97 undecidable, 10 unsatisfied).
• Target panic rows: 7, all still unsatisfied.
• Closed by current machinery on target bundle:
  • 8 kit/reflexive/body-call-expected
  • 3 rust-tests/reflexive/body-call-expected
  • 21 rust-tests/vacuous
  • 0/7 target panic rows

Demand-validated gap priority

1. Relational/dataflow + opaque enum/Option reasoning: 62/107 open target rows. This is the dominant gap and matches the dogfood Slice 33: classify and close independent provekit-cli panic rows #1901 residual shape.
2. No-contract coverage: 77 lift gaps.
3. Body-contract shapes: 32 open target rows.
4. Unsupported macro handling: 14 lift gaps.
5. Unwrap/index-style preconditions: 7 target panic rows remain open.

Mint telemetry:

• 34 fn-contracts (33 body-discharge-eligible, 1 missing-result-equation).
• dep_forwarded=127, dep_dropped=0.
• 68 bridges emitted.
• 91 lift gaps: 77 no-contract-for-callee, 14 unsupported-macro-callsite.

References

• Slice 33: classify and close independent provekit-cli panic rows #1901: same relational/dataflow demand from dogfood rows.
• mint pipeline drops method:strip_prefix producer bridge from final proof #1907: strip_prefix / bundle-inclusion dependency remains parked.
• Track Rust index-bounds panic coverage #1904: index-bounds follow-up remains separate.

Decision signal

The kit now has an external-code soundness milestone (falsePass=0 on a real parser crate), but vendor-meaningful coverage needs a machinery stack. The dominant next lever is relational/dataflow + opaque enum/Option reasoning, now validated by both dogfood and third-party Rust OSS evidence.

[TSavo]

Slice 35 Phase 1 design pin: keyset-membership guard

Status: read-only design only. No kit/source changes in this phase.

Enumerated shapes

version-compare target bundle relational/opaque rows: 62 open rows classified as:

• 49 enum/discriminant mapping rows over Cmp::{Eq,Ne,Lt,Le,Ge,Gt} through name, invert, opposite, flip, sign, factor, ord.
• 6 Option presence/dataflow rows involving method:is_some / has_manifest / has_max_depth.
• 6 enum mapping rows over Ordering::{Less,Equal,Greater}.
• 1 method-result/dataflow row involving method:compare / compare_to.

The version-compare source has no .get, .keys, .difference, or .intersection hits, so it validates the broader relational/dataflow + opaque-symbol demand, but not the clean keyset-membership first shape. Those rows are later slices.

Dogfood #1901 rows 3-5 are the clean keyset target:

• cmd_protocol.rs:426: to_keys.difference(&from_keys) then to_props.get(key).expect("present").
• cmd_protocol.rs:439: to_keys.intersection(&from_keys) then from_props.get(key).expect("present").
• cmd_protocol.rs:440: same intersection then to_props.get(key).expect("present").

First shape

Implement only keyset-membership as an internal lifter proof source. The emitted verifier-facing guard should remain the existing panic-precondition atom:

is_some(method:get(map, key))

That atom is carried with the existing cf_guarded(guard, value) mechanism and matches Option::{unwrap,expect} preconditions syntactically. No verifier proof-engine rewrite and no new verifier relational semantics are part of this slice.

Internal proof rule

Track visible, scoped key provenance only when structurally apparent in the Rust AST.

Modeled provenance sources:

• Direct map keys: for key in map.keys() establishes key in keyset(map).
• Direct map iteration: for (key, _) in map.iter() and for (key, _) in &map establish key in keyset(map).
• Keyset snapshot: immutable let keys = map.keys().cloned().collect::<BTreeSet<_>>() establishes keys == keyset(map) while both keys and map remain stable.
• Difference: for key in keys_a.difference(&keys_b) establishes membership only in the map behind keys_a.
• Intersection: for key in keys_a.intersection(&keys_b) establishes membership in the maps behind both keys_a and keys_b.

Consume only at a matching panic receiver:

• map.get(key).unwrap() / map.get(key).expect(...) may be wrapped with cf_guarded(is_some(method:get(map,key)), ...) only when the current scoped facts prove key in keyset(map).
• difference polarity is exact: to_keys.difference(&from_keys) proves to_props.get(key), not from_props.get(key).
• intersection proves both participating maps, not any third map.

Soundness conditions

• The key must be bound by the modeled loop/keyset operation. Opaque or arbitrary key origins refuse.
• The map term and key term must match structurally after existing term normalization. No alias guessing.
• The source map, snapshot keyset, and key binding must remain stable from provenance creation through the get receiver.
• Reuse the existing narrow-collect / complete-invalidate discipline. The current visible lift.rs invalidation covers let/assignment/mutable roots; implementation must extend the shared invalidation predicate before emitting keyset guards so collection mutations and mutable borrows invalidate/refuse.
• Mutating or potentially mutating methods on tracked map/keyset roots refuse, including at least insert, remove, clear, retain, append, split_off, entry, get_mut, iter_mut, and any &mut borrow. Unknown methods on tracked roots default-refuse unless explicitly whitelisted as pure reads.
• Whitelisted pure reads for this slice are narrow: keys, iter, difference, intersection, get, cloned, and the specific collect::<BTreeSet<_>>() snapshot shape.
• Unknown iterators, macros, closures, aliases, field-returned keysets, and function-returned keysets refuse.

Discrimination suite required before implementation is green

Positive gates:

• map.keys() loop proves map.get(key).expect.
• map.iter() / &map pair loop proves map.get(key).expect.
• to_keys.difference(&from_keys) proves to_props.get(key).expect.
• to_keys.intersection(&from_keys) proves both to_props.get(key).expect and from_props.get(key).expect.

False-pass guards:

• Wrong map: to_keys.difference(&from_keys) then from_props.get(key).expect refuses.
• Reversed polarity: from_keys.difference(&to_keys) then to_props.get(key).expect refuses.
• Third map: to_keys.intersection(&from_keys) then other_props.get(key).expect refuses.
• Mutation between provenance and get refuses: remove, clear, insert, retain, entry, get_mut, iter_mut, assignment, and &mut borrow.
• Key removed between membership and get refuses, e.g. to_props.remove(key); to_props.get(key).expect(...).
• Opaque key refuses: let key = some_fn(); map.get(&key).expect(...).
• Keyset from opaque source refuses: let keys = get_keys(); for key in keys { map.get(key).expect(...) }.
• Transformed or different key refuses: map.get(transform(key)).expect(...) or map.get(other_key).expect(...).
• Unmodeled collection op refuses by default.

Implementation boundary after approval

Expected slice remains kit/lifter-side: extend provekit-walk guard/provenance tracking and tests. Do not touch #1907/strip_prefix. Do not change verifier enumeration or add verifier relational semantics for this first keyset shape.

[TSavo]

Slice 35 design amendment: machinery-first framing

Claude/architecture review had no veto on the keyset-membership soundness design, but required this reframe before implementation approval:

Reframe

Keyset-membership is dogfood-only in the current evidence. The version-compare Phase B source has no .get, .keys, .difference, or .intersection rows. Its 62 relational/opaque rows are mostly enum/Option/dataflow:

• 49 Cmp enum/discriminant mapping rows.
• 6 Ordering enum mapping rows.
• 6 Option presence/dataflow rows.
• 1 compare/result dataflow row.

So slice 35 should not be framed as +3 dogfood K as the prize. The deliverable is the sound relational-guard machinery, validated first on the cleanest available shape. Keyset-membership is the low-risk validation vehicle: visible provenance, exact membership semantics, and a strong falsePass discrimination suite.

Slice 36 should cash the real third-party leverage by applying the same machinery to the 55 Cmp/Ordering enum-mapping rows from version-compare.

Shape-agnostic machinery requirement

The slice 35 implementation must avoid keyset-only infrastructure. The abstraction should be:

provenance-tracked fact F + stability conditions S => guard fact G that discharges obligation O.

Keyset-membership is the first registered fact shape:

• Fact: key in keyset(map).
• Stability: key provenance, map root, and keyset/snapshot root remain valid under shared invalidation.
• Guard: is_some(method:get(map,key)).
• Obligation: map.get(key).unwrap()/expect precondition.

This needs to be extensible so slice 36 can register enum/discriminant facts without rebuilding the provenance/stability/guard-emission framework.

Strict whitelist confirmation

Collection provenance must be whitelist-gated, never blocklist-gated. Only these modeled ops can emit keyset membership:

• map.keys() / map.iter() / &map pair iteration => membership in that map.
• keys_a.difference(&keys_b) => membership in the map behind keys_a only.
• keys_a.intersection(&keys_b) => membership in maps behind both keysets.
• The audited keyset snapshot shape: immutable map.keys().cloned().collect::<BTreeSet<_>>().

Every other collection operation refuses by default: union, symmetric_difference, chain, filter, map, transformed keys, opaque keyset-returning functions, aliases, macros, closures, and unknown methods.

Implementation gate still closed

No implementation until explicit approval after reviewing this amended design. On approval, implementation must be RED-first with the full positive and false-pass discrimination suite from the prior design comment.

[TSavo]

Slice 36(A) design pin: exhaustive-match-totality

Approved implementation scope: exhaustive enum-match totality only.

Recognition:

• Identify a match whose scrutinee resolves to a known enum definition.
• Read the enum's full declared variant set from the resolved enum definition, never from the arms.
• Accept only explicit variant-pattern arms; Pat::Or is allowed when every alternative is an explicit variant of the same enum.
• Require the explicit arm coverage set to equal the enum's full declared variant set.
• Refuse _/wildcard arms, arm guards, unknown/unresolved enum definitions, non-enum scrutinees, and #[non_exhaustive] enums.

Mechanism fit:

• Use the existing function-contract post/body-discharge carrier.
• Do not use cf_guarded and do not add a TOML singleton/function_postconditions entry.
• This proves totality/no-panic for all scrutinee variants; it does not prove a specific variant value or reduce a match to a specific branch value.

Soundness boundary:

• Cardinal sin: assuming a match is exhaustive when it is not.
• The variant set must come from the resolved enum definition; inferring it from observed arms is circular and unsound.
• A non-exhaustive enum must refuse, because explicit local coverage is not a closed-world proof.

RED-first discrimination set:

• _ wildcard present -> refuse/defer.
• Explicit arms missing a declared variant -> refuse.
• Scrutinee not a known enum -> refuse.
• Enum definition unresolvable -> refuse.
• #[non_exhaustive] enum -> refuse.

Positive fixtures:

• Cmp::{name,invert,opposite,sign,factor} with explicit coverage; factor may use Pat::Or over explicit variants.
• From<std::cmp::Ordering> for Cmp when Ordering is resolved from the std catalog/known enum set.

Deferred buckets:

• flip/ord value-wildcard matches are sound follow-up work, but outside this explicit-all-variants slice.
• _ => unreachable!() variant-impossibility and version.rs:303 require range/variant reasoning and remain deferred.

Scope fence:

• Kit/lifter-side only (provekit-walk), no verifier change, no strip_prefix/mint pipeline drops method:strip_prefix producer bridge from final proof #1907, no conformance-test drain in this slice.

[TSavo]

Slice 36(A) enum-match-totality measurement, post-implementation rerun.

Base/worktree:

• Slice branch based on current origin/main / e8485b1a2c3ac4069a6914e165c02b9a5418925e.
• Kit-side implementation only: provekit-walk/src/bin/walk_rpc.rs.
• RED-first guard tests were load-bearing: wildcard arm, missing declared variant, non-enum scrutinee, unresolved enum def, and #[non_exhaustive] all over-discharged before the coverage gate and refuse after it.

Dogfood cold gate on battleaxe:

• libprovekit: panicSafe=24, falsePass=0, silentlyDropped=0, droppedSites=[].
• provekit-cli: panicSafe=35, falsePass=0, silentlyDropped=0, droppedSites=[].
• Dogfood delta is +0 panic K; this is regression/floor evidence, not the value story for this slice.

version-compare recon rerun:

• Scratch: /home/tsavo/remote/provekit-oss-recon/slice34-phase-b-version-compare-20260603055537/slice36-rerun-20260603.
• Used the slice-36 target mint and the original pinned std-shim proof from the slice-34 scratch to keep the vendored imports apples-to-apples.
• Baseline prove.json: totalCallsites=287, discharged=102, violations=246, panicSafe=5, falsePass=0.
• Slice-36 rerun: totalCallsites=272, discharged=158, violations=175, panicSafe=5, falsePass=0, loadErrors=[].
• Aggregate delta: discharged +56, violations -71, panic K +0.

Enum-totality recognition/refusal evidence:

• Cmp::name, Cmp::invert, Cmp::opposite, Cmp::sign, Cmp::factor, and <Cmp as From<Ordering>>::from carry bodyDischargeProofKind = "exhaustive-enum-match-totality".
• Cmp::flip and Cmp::ord carry enum-match-totality-refused:wildcard-arm; the value-wildcard bucket stayed deferred and did not route.
• Cmp::from_sign / Cmp::from_name carry enum-match-totality-refused:non-enum-scrutinee.

Important caveat:

• Exhaustive totality is sound and firing, but it does not prove value mapping. The 30 caller rows for name/invert/opposite/sign/factor that require reducing Cmp::Eq, Cmp::Ne, etc. to specific return values remain undecidable with the same opaque-variant reasons.
• <Cmp as From<Ordering>>::from now has 6 discharged/vacuous rows; internal constructor obligations such as Err at cmp.rs:72 and Some at cmp.rs:309 also close vacuously.
• Closing the remaining value-mapping rows requires a value-reduction/mapping mechanism, not totality. Forcing those rows through totality would be a falsePass risk.