T-ruled: delete the experimental promotion/consensus apparatus; keep contract composition.
Composition over AST trees is not cruft — contradiction detection is the unsatisfiability of the composition (C₁ ∧ C₂ UNSAT ⟺ contradiction). No composition → no conjunction for the solver → no contradiction → the refuse arm of the trichotomy has nothing to fire on. Composition is upstream of supra omnia, rectum. It stays forever.
This is a separating refactor, not an rm: the promotion policy and the core composition live tangled in the same files (libprovekit/src/core/source_transform.rs, core/bind.rs, ir-types).
KEEP — the spine (do not touch)
libprovekit::compose (canonical contract-composition primitive).- Composition over AST trees in
core/source_transform.rs + core/bind.rs — where contracts conjoin at the positions they touch.
- The solver / discharge path;
provekit-verifier/src/solvers/* solver consensus (three-way Z3/CVC5/Vampire — diverse convergence, a different 'consensus' from promotion; core).
MigrateReceiptEnvelope only if still used by kept materialize/witness after the cut.
CUT — the bolted-on governance layer
PromotionDecision / promotion-decision registry (libprovekit/src/promotion_decision_registry.rs, ir-types types + serde tests, provekit-cli/src/promotion_query.rs).witness consensus subcommand + verify --require-empirically-witnessed flag + consensus-policy / policy_profile apparatus.- Cross-language witnessed consensus admission ceremony (was fed by the now-deleted migrate path).
- Tests:
witness_consensus_test, promotion_decision_registry, policy_profile_*, promotion_decision_serde, catalog_snapshot_serde (as they pertain to promotion).
Map (consumers to re-fit, not blanket-remove)
PromotionDecision referenced from core/bind.rs + libprovekit/src/lib.rs; MigrateReceiptEnvelope from cmd_materialize, cmd_witness. Each caller must be classified: composition-spine (keep, re-fit) vs promotion-policy (cut). Do not delete a reference that's actually in the Name-verb algebra or the composition path.
Follows the night's pattern: direction ruled, landing is its own careful piece of work (cf. catalog-store, C-macros).
🤖 Generated with Claude Code
T-ruled: delete the experimental promotion/consensus apparatus; keep contract composition.
Composition over AST trees is not cruft — contradiction detection is the unsatisfiability of the composition (
C₁ ∧ C₂UNSAT ⟺ contradiction). No composition → no conjunction for the solver → no contradiction → the refuse arm of the trichotomy has nothing to fire on. Composition is upstream of supra omnia, rectum. It stays forever.This is a separating refactor, not an
rm: the promotion policy and the core composition live tangled in the same files (libprovekit/src/core/source_transform.rs,core/bind.rs, ir-types).KEEP — the spine (do not touch)
libprovekit::compose(canonical contract-composition primitive).core/source_transform.rs+core/bind.rs— where contracts conjoin at the positions they touch.provekit-verifier/src/solvers/*solver consensus (three-way Z3/CVC5/Vampire — diverse convergence, a different 'consensus' from promotion; core).MigrateReceiptEnvelopeonly if still used by kept materialize/witness after the cut.CUT — the bolted-on governance layer
PromotionDecision/ promotion-decision registry (libprovekit/src/promotion_decision_registry.rs, ir-types types + serde tests,provekit-cli/src/promotion_query.rs).witness consensussubcommand +verify --require-empirically-witnessedflag + consensus-policy /policy_profileapparatus.witness_consensus_test,promotion_decision_registry,policy_profile_*,promotion_decision_serde,catalog_snapshot_serde(as they pertain to promotion).Map (consumers to re-fit, not blanket-remove)
PromotionDecisionreferenced fromcore/bind.rs+libprovekit/src/lib.rs;MigrateReceiptEnvelopefromcmd_materialize,cmd_witness. Each caller must be classified: composition-spine (keep, re-fit) vs promotion-policy (cut). Do not delete a reference that's actually in the Name-verb algebra or the composition path.Follows the night's pattern: direction ruled, landing is its own careful piece of work (cf. catalog-store, C-macros).
🤖 Generated with Claude Code