feat(abi): S2 — consonance transitions (MERGE/SPLIT/NORMALISE) end-to-end#61
Merged
Conversation
Core S2 certificate logic on the Idris side. NEW src/core/Transition.idr: SubjectRef (identity-handle newtype, distinct from read-location Source), RepairJustification (mirrors the engine regenerator), data Transition (TMerge/TSplit/TNormalise — multi-subject / result-less), data VclOp = Query Statement | Transit Transition. Deciders subjectsDistinct / evidenceInjectionSafe (L4 absence polarity) / evidenceTypeCompat (reuses Decide.whereComparisonsCompatible on the evidence Expr); TransitionSafe certificate (reflection style) + soundness + certifiedSubjectsDistinct non-vacuity extractor + certifiedTransitionLevel. Verb extended with VMerge/VSplit/VNormalise (tag-only, reopens nothing). NORMALISE honestly OMITS L5/L6 (no result set). Provenance-descent, engine-liveness, modality-presence, identity-vs-location are disclosed OWEDs. Wired into corpus: symlink + vclut-core.ipkg module line + proof-corpus.yml honesty-guard list. Verified: idris2 --build exit 0 (L0..L10 untouched), honesty-guard Clean, cargo build OK. WIP — Rust mirror / VCLT wire / parser / callers / VERIFICATION-STANCE still to come. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…ansition certifier Wire the S2 consonance transitions (MERGE/SPLIT/NORMALISE) end-to-end across the doubly-trusted Idris<->Rust seam, stacked on slice 1's proof module. The L0..L10 statement corpus stays byte-identical — transitions are a SEPARATE type, so no statement proof is re-opened, weakened, or made vacuous. Rust mirror (src/interface/parse): - ast.rs: SubjectRef / RepairJustification / Transition / VclOp — a positional one-to-one mirror of Transition.idr (Query boxed for enum size balance). - parser.rs: parse_op dispatcher + parse_transition/parse_subject/parse_repair; parse() stays query-only. Depth-guarded expression grammar (MAX_EXPR_DEPTH) so deeply-nested evidence / NOT-chains fail closed with a typed ParseError instead of a stack-overflow process abort (adversarial-review finding). - wire.rs: VCLT magic + to_wire_op/from_wire_op codec (total, bounds-checked, no untrusted pre-alloc) — distinct from the byte-unchanged VCLW statement stream. - decider.rs: certified_transition_level — faithful port of certifiedTransitionLevel; the Transit arm routes here, NEVER down-casting a transition to the Statement certifier (the type system forbids it). - bin/vclt-gate.rs: routes VclOp::Transit -> run_transition. Certified Idris side: - WireDecode.idr: fromWireOp (%default total, zero proof-escape, fuel-bounded). - WireConformance.idr: conformOpQ1/T1/T2 + ctlVerdict1/2 — Refl-pin the cross-language wire AND verdict agreement on the EXACT bytes the Rust to_wire_op emits (oracle tests/conformance_emit.rs goldenOpQ1/T1/T2). Honest scope (VERIFICATION-STANCE §S2): the InjectionProof ceiling (4); the genuine L5/L6 omission for result-less NORMALISE; the certificate proved NON-vacuous (certifiedSubjectsDistinct); the 4 disclosed OWEDs (provenance-descent / engine-liveness / modality-presence / identity-vs- location); and the statement-only recompute/attest boundary. Verified: idris2 --build exit 0 (13/13), honesty-guard Clean, cargo test (35) + clippy -D warnings clean. Independently checked by a 4-dimension adversarial review (wire/decider faithfulness + proof honesty: clean; the one confirmed parser-totality gap is fixed here). Co-Authored-By: Claude Opus 4.8 (1M context) <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
1 participant
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.
S2 — consonance transitions (MERGE / SPLIT / NORMALISE), end-to-end
Follows #60 (S1 verb discriminant, merged). Base:
main.Wires the three remaining consonance verbs across the doubly-trusted Idris↔Rust seam. They do not fit
Statement(multi-subject / result-less), so they are a separateTransitiontype and the top-level op isVclOp = Query Statement | Transit Transition. The entire L0..L10 statement corpus stays byte-identical — no statement proof is re-opened, weakened, or made vacuous.What landed
src/interface/parse):SubjectRef/RepairJustification/Transition/VclOp(positional one-to-one mirror ofTransition.idr);parse_opdispatcher +parse_transition(parsestays query-only);VCLTwire codec (to_wire_op/from_wire_op, total, bounds-checked);certified_transition_level(faithful port, routes from theTransitarm, never down-casts to the statement certifier);vclt-gateroutesTransit → run_transition.fromWireOpdecoder (%default total, zero proof-escape, fuel-bounded);conformOpQ1/conformT1/conformT2+ctlVerdict1/ctlVerdict2Refl-pin the cross-language wire and verdict agreement on the exact bytes the Rust encoder emits (oracletests/conformance_emit.rs).Honest scope (
VERIFICATION-STANCE.adoc§S2)NORMALISEgenuinely omits L5/L6 (absent, not vacuously passed); certificate proved non-vacuous (certifiedSubjectsDistinct).recompute-wasm) + attestation (attest) stay statement-only this slice.Verification
idris2 --buildexit 0 (13/13) · honesty-guard Clean ·cargo test(35) ·clippy -D warningsclean.MERGE … WHERE ((…))— is fixed here: the expression grammar is depth-guarded (MAX_EXPR_DEPTH) so deep nesting fails closed with a typedParseError, with three big-stack regression tests.🤖 Generated with Claude Code