briansrls · Jun 22, 2026 · Jun 22, 2026
diff --git a/src/v2/extdeps/coercion_widening.dag b/src/v2/extdeps/coercion_widening.dag
@@ -1,12 +1,5 @@
-// src/v2/extdeps/coercion_widening.dag
-// Scope: cross-target faithful refinement widening pair registry (MVP rust i32 → python int).
-// Anchor: ROADMAP.md coercion (i32 → arbitrary-precision int); W3.2 Leg B.
-// Status: MVP pair table lives here; std/refinement_widening_predicate proves bundle evidence (P2).
-
-
 module v2.extdeps.coercion_widening
 
-
 import v2.extdeps.languages.python { python_int_inhabitant_node }
 import v2.extdeps.languages.rust { rust_inhabitant_i32_node }
 import v2.std.coercion {
@@ -66,7 +59,6 @@ fn coercion_widening_python_integer_value_set_from_inhabitant(inhabitant: Node)
   }
 }
 
-
 fn mvp_rust_i32_python_int_refinement_widening_predicate() -> PreservationPredicate {
   let source = rust_inhabitant_i32_node()
   let candidate = python_int_inhabitant_node()
@@ -95,7 +87,6 @@ fn mvp_python_int_rust_i32_refinement_narrowing_predicate() -> PreservationPredi
   }
 }
 
-
 fn coercion_fold_mvp_rust_i32_to_python_int_widening(
   source: CanonicalGrounding,
   candidates: CoercionCandidateSet,

diff --git a/src/v2/extdeps/coordination.dag b/src/v2/extdeps/coordination.dag
@@ -1,7 +1,3 @@
-// src/v2/extdeps/coordination.dag
-// Scope: Multi-program coordination as effect-typed Bind composition.
-// Status: T-4.8 modeled; WIRECONTRACT-OBLIGATION-TABLE-T4.8 is executable as per-arm obligation rows, with CoordinationEffectKind retained as a tracked bridge until binds reference canonical obligation rows directly.
-
 module v2.extdeps.coordination
 
 import v2.std.collection { List }
@@ -17,7 +13,6 @@ type FrameworkRef {
   identity: Symbol
 }
 
-// 🟢 coproduct dissolution — #coordination-coproduct-ledgers.
 type FrameworkBinding
   = HostedByFramework { framework: FrameworkRef }
   | NoFramework
@@ -45,26 +40,20 @@ type RequiredSettleBound {}
 
 type RequiredConvergeBound {}
 
-// Anchor: https://en.wikipedia.org/wiki/Messaging_pattern
-// 🟢 coproduct dissolution — #coordination-coproduct-ledgers.
 type ExchangePattern
   = RequestReply
   | FireAndForget
   | StreamExchange
   | PublishSubscribe
 
-// 🟢 coproduct dissolution — #coordination-coproduct-ledgers.
 type SettlementGuarantee<Bound>
   = ImmediateSettlement
   | SettlesWithin { bound: Bound }
 
-// Anchor: https://en.wikipedia.org/wiki/Eventual_consistency
-// 🟢 coproduct dissolution — #coordination-coproduct-ledgers.
 type ConsistencyGuarantee<Bound>
   = NoReplicaConvergence
   | EventuallyConsistent { bound: Bound }
 
-// 🟡 coproduct dissolution — consumer:coordination-bind-obligation-row-authority; dissolves when CoordinationBind references canonical CoordinationEffectObligation rows directly.
 type CoordinationEffectKind
   = Http
   | Queue
@@ -133,13 +122,11 @@ type WireContractFacts {
   consistency: ConsistencyGuarantee<ConvergeBound>
 }
 
-// Anchor: https://en.wikipedia.org/wiki/Inter-process_communication
 type WireContract {
   facts: WireContractFacts,
   bind: CoordinationBind
 }
 
-// Anchor: https://en.wikipedia.org/wiki/Distributed_computing
 type DeploymentUnit {
   endpoints: List<Endpoint>,
   wire_contracts: List<WireContract>

diff --git a/src/v2/extdeps/coordination_claims_test.dag b/src/v2/extdeps/coordination_claims_test.dag
@@ -1,13 +1,5 @@
-// Scope: v2.extdeps.coordination WIRECONTRACT-OBLIGATION-TABLE-T4.8 as
-// discriminating claim-run witnesses, routed through v2 (`dag run --claim-run`).
-// The executable receipt is the in-file claim witness, run in-process by the
-// claim_batch binary (the witnesses ARE the coverage).
-// Importing v2.extdeps.coordination forces v2 to tokenize/parse/infer it, so the
-// parse-surface fact rides every witness below.
-
 module v2.test.extdeps.coordination_claims
 
-
 import v2.std.logic { Bool }
 import v2.extdeps.coordination {
   ExchangePattern,
@@ -26,8 +18,6 @@ import v2.extdeps.coordination {
   coordination_effect_obligation
 }
 
-
-
 import v2.std.verification {
   BoolWitness,
   BoolWitnessClaim,
@@ -37,8 +27,6 @@ fn coord_not(b: Bool) -> Bool {
   b == false
 }
 
-
-// ExchangePattern arm probes (one per variant; a wrong stored variant fails its probe).
 fn exchange_is_request_reply(e: ExchangePattern) -> Bool {
   match e {
     RequestReply => true
@@ -67,8 +55,6 @@ fn exchange_is_publish_subscribe(e: ExchangePattern) -> Bool {
   }
 }
 
-
-// SettlementGuarantee<RequiredSettleBound> arm probes.
 fn settlement_is_immediate(s: SettlementGuarantee<RequiredSettleBound>) -> Bool {
   match s {
     ImmediateSettlement => true
@@ -83,10 +69,6 @@ fn settlement_is_within(s: SettlementGuarantee<RequiredSettleBound>) -> Bool {
   }
 }
 
-
-// Receipt A1 (obligation exchange table is arm-sharp): every CoordinationEffectKind maps to
-// its own ExchangePattern AND the table is not a constant — Http's exchange is NOT Queue's.
-// Discriminates: mutate any arm's required_exchange in coordination.dag → this goes red.
 test fn coordination_obligation_exchange_arm_sharp_holds() -> Bool {
   exchange_is_request_reply(e: coordination_effect_obligation(effect: Http).required_exchange)
     && exchange_is_fire_and_forget(e: coordination_effect_obligation(effect: Queue).required_exchange)
@@ -95,10 +77,6 @@ test fn coordination_obligation_exchange_arm_sharp_holds() -> Bool {
     && coord_not(b: exchange_is_fire_and_forget(e: coordination_effect_obligation(effect: Http).required_exchange))
 }
 
-
-// Receipt A2 (obligation settlement discriminant is arm-sharp): Http settles immediately,
-// the async effects (Queue/Stream/PubSub) settle-within; the negative arms pin that the
-// discriminant tracks the effect, not a constant.
 test fn coordination_obligation_settlement_arm_sharp_holds() -> Bool {
   settlement_is_immediate(s: coordination_effect_obligation(effect: Http).required_settlement)
     && settlement_is_within(s: coordination_effect_obligation(effect: Queue).required_settlement)

diff --git a/src/v2/extdeps/cpp_abi.dag b/src/v2/extdeps/cpp_abi.dag
@@ -1,24 +1,16 @@
-// src/v2/extdeps/cpp_abi.dag
-// Scope: C++ ABI / target data-model facts for implementation-defined fundamental widths.
-// Anchor: ISO/IEC 14882:2024 [basic.fundamental] + Itanium C++ ABI revision 1.86.
-// Status: T-29 modeled 2026-05-18.
-
 module v2.extdeps.cpp_abi
 
-// 🟢 grounded.
 type CppMachineWidth8
 type CppMachineWidth16
 type CppMachineWidth32
 type CppMachineWidth64
 
-// 🟢 coproduct dissolution — T29-ABI.
 type CppIntegerWidth
   = CppWidth8 { width: CppMachineWidth8 }
   | CppWidth16 { width: CppMachineWidth16 }
   | CppWidth32 { width: CppMachineWidth32 }
   | CppWidth64 { width: CppMachineWidth64 }
 
-// 🟢 grounded.
 type CppCoreIntegerWidthModel {
   char_width: CppIntegerWidth
   short_width: CppIntegerWidth
@@ -29,23 +21,20 @@ type CppCoreIntegerWidthModel {
   wchar_t_width: CppIntegerWidth
 }
 
-// 🟢 coproduct dissolution — T29-ABI.
 type CppPlainCharSignedness
   = PlainCharSigned { tag: CppPlainCharSigned }
   | PlainCharUnsigned { tag: CppPlainCharUnsigned }
 
 type CppPlainCharSigned
 type CppPlainCharUnsigned
 
-// 🟢 coproduct dissolution — T29-ABI.
 type CppWcharTSignedness
   = WcharTSigned { tag: CppWcharTSigned }
   | WcharTUnsigned { tag: CppWcharTUnsigned }
 
 type CppWcharTSigned
 type CppWcharTUnsigned
 
-// 🟢 coproduct dissolution — T29-ABI.
 type CppDataModelFamily
   = ILP32 { tag: CppDataModelFamilyILP32 }
   | LP64 { tag: CppDataModelFamilyLP64 }
@@ -57,25 +46,21 @@ type CppDataModelFamilyLP64
 type CppDataModelFamilyLLP64
 type CppDataModelFamilyILP64
 
-// 🟢 coproduct dissolution — T29-ABI.
 type CppAbiModel
   = ItaniumCxxAbi186 { tag: CppAbiModelItaniumCxxAbi186 }
   | PlatformCxxAbi { tag: CppAbiModelPlatformCxxAbi }
 
 type CppAbiModelItaniumCxxAbi186
 type CppAbiModelPlatformCxxAbi
 
-// 🟢 grounded.
 type CppTargetDataModel<family, integer_widths, plain_char_signedness, wchar_t_signedness>
 type CppTargetProfile<abi_model, data_model>
 
-// 🟢 grounded.
 type CppIntegerWidth8 = CppWidth8 { width: CppMachineWidth8 }
 type CppIntegerWidth16 = CppWidth16 { width: CppMachineWidth16 }
 type CppIntegerWidth32 = CppWidth32 { width: CppMachineWidth32 }
 type CppIntegerWidth64 = CppWidth64 { width: CppMachineWidth64 }
 
-// 🟢 grounded.
 type CppILP32IntegerWidths = CppCoreIntegerWidthModel {
   char_width: CppIntegerWidth8,
   short_width: CppIntegerWidth16,

diff --git a/src/v2/extdeps/file_system.dag b/src/v2/extdeps/file_system.dag
@@ -1,101 +1,76 @@
-// src/v2/extdeps/file_system.dag
-// Scope: External file-system resource model + modeled file effects (read/write).
-// Status: scaffold — Wave-2 fail-closed boundary (POSIX substrate retained for posix/testgen consumers).
-
 module v2.extdeps.file_system
 
-
 import v2.std.algebra { FreeMonoid }
 import v2.std.diagnostic { Outcome }
 import v2.std.machine { Byte }
 
-
-// Anchor: https://pubs.opengroup.org/onlinepubs/9799919799/basedefs/V1_chap03.html#tag_03_241
 type PosixByteString = FreeMonoid<Byte>
 
 type NamedPathComponent {
   bytes: PosixByteString
 }
 
-// 🟡 coproduct dissolution — OS-1.
 type PathComponent
   = CurrentComponent
   | ParentComponent
   | NamedComponent { component: NamedPathComponent }
 
-
-// Anchor: https://pubs.opengroup.org/onlinepubs/9799919799/basedefs/V1_chap03.html#tag_03_271
 type AbsolutePath {
   components: List<PathComponent>
 }
 
-// 🟡 coproduct dissolution — OS-1.
 type RelativePathHead
   = ParentHead
   | NamedHead { component: NamedPathComponent }
 
-// 🟡 coproduct dissolution — OS-1.
 type RelativePath
   = CurrentDirectory
   | CurrentDescendant { first: RelativePathHead, rest: List<PathComponent> }
   | RelativeDescendant { first: RelativePathHead, rest: List<PathComponent> }
 
-// 🟡 coproduct dissolution — OS-1.
 type FilesystemPath
   = Absolute { path: AbsolutePath }
   | Relative { path: RelativePath }
 
-
-// Anchor: https://pubs.opengroup.org/onlinepubs/9799919799/basedefs/sys_stat.h.html
-// 🟡 coproduct dissolution — OS-1.
 type FileKind
   = RegularFile
   | Directory
   | Symlink
 
-// 🟡 coproduct dissolution — OS-1.
 type FileKindResolutionPolicy
   = FollowSymlinks
   | DoNotFollowSymlinks
 
-
-// Anchor: https://pubs.opengroup.org/onlinepubs/9799919799/functions/read.html + https://pubs.opengroup.org/onlinepubs/9799919799/functions/write.html + https://pubs.opengroup.org/onlinepubs/9799919799/functions/readdir.html
 type Filesystem
 
 type FileBody = FreeMonoid<Byte>
 
-// Anchor: https://pubs.opengroup.org/onlinepubs/9799919799/basedefs/V1_chap03.html#tag_03_271
 type FileResource {
   filesystem: Filesystem
 }
 
-// Anchor: https://pubs.opengroup.org/onlinepubs/9799919799/basedefs/V1_chap03.html#tag_03_271
 type FilePath {
   path: FilesystemPath
 }
 
 type FileContent = FileBody
 
-// 🟢 grounded.
 type FileRead {
   resource: FileResource,
   path: FilePath
 }
 
-// 🟢 grounded.
 type FileWrite {
   resource: FileResource,
   path: FilePath,
   content: FileContent
 }
 
-// 🟢 grounded.
 type FileReadReceipt {
   request: FileRead,
   content: FileContent
 }
 
-// 🟢 grounded.
 type FileWriteReceipt {
   request: FileWrite,
   resource: FileResource
@@ -110,12 +85,6 @@ type ModeledFileEffects {
   file_write: fn(FileWrite) -> FileWriteResult
 }
 
-// 🟡 P5 bridge — legacy POSIX operation payload table (consumer: v2.lens.testgen
-// only — CorpusEnumerationRequest.operations: FileSystemOperations). Dissolution
-// trigger: wave2-c2-testgen-modeled-file-effects — delete ReadFileRequest,
-// WriteFileRequest, ListDirRequest, FileKindRequest, and FileSystemOperations
-// when v2/lens/testgen.dag CorpusEnumerationRequest.operations is
-// ModeledFileEffects-only.
 type ReadFileRequest {
   filesystem: Filesystem
   path: AbsolutePath