P4 SPICE/analog lane MANAGER closeout (fierce-ibex-308) — close only after SP-M3 + decisive dual-emission witness green

src/v4/extdeps/formats/modelica.dag

@@ -0,0 +1,70 @@
+// src/v4/extdeps/formats/modelica.dag
+//
+// Scope: Modelica passive analog circuit model — acausal, equation-based.
+//        Components, port connections, model declarations. NO control flow.
+// Anchor: Modelica Language Specification 3.5 (Modelica Association, 2012).
+//         Modelica Standard Library (MSL 4.0) — Electrical.Analog.{Basic,Sources}.
+// Stress (T-4.10 paradigm-challenger): the SAME .dag RC circuit fixture → a Modelica
+//   acausal model. Acausal paradigm: components carry port connectors, equations are
+//   undirected; `connect(A.p, B.p)` is a pair of equalities (potential + flow), not a
+//   directed wire. No node-voltage annotation on components — that is SPICE's causal
+//   topology. If the format data-model requires causal annotation to represent a passive
+//   circuit, that is a substrate-design signal to surface immediately (stop + escalate).
+// Splitting this file requires explicit operator ratification.
+
+module v4.extdeps.formats.modelica
+
+import v4.std.diagnostic { Outcome }
+import v4.std.node { Symbol }
+
+
+// Modelica instance name or port name (variable-like identifier).
+type ModelicaIdentifier { name: Symbol }
+
+
+// Port reference in a connect() equation: <component>.<port>
+// The connector pair carries equal potential and summed flow — the acausal contract.
+type ModelicaPortRef {
+  component: ModelicaIdentifier
+  port: ModelicaIdentifier
+}
+
+
+// Undirected connection equation: connect(left, right).
+// Semantics: left.potential = right.potential ∧ left.flow + right.flow = 0.
+// This is the paradigm difference from SPICE node-voltage reference: no direction.
+type ModelicaConnection {
+  left: ModelicaPortRef
+  right: ModelicaPortRef
+}
+
+
+// 🟢 coproduct dissolution — passive analog circuit component variants.
+// Variant field names follow MSL 4.0 Electrical.Analog parameter conventions
+// (R for resistance in Ω, C for capacitance in F, V for voltage in V).
+// Value lexemes are String (same carrier as SpiceValue.lexeme) to support the
+// paradigm-comparison witnesses; an exact-quantity carrier defers to T-3 Dimension/Volt.
+type ModelicaPassiveComponent
+  = ModelicaResistor        { name: ModelicaIdentifier, r: String }
+  | ModelicaCapacitor       { name: ModelicaIdentifier, c: String }
+  | ModelicaConstantVoltage { name: ModelicaIdentifier, v: String }
+  | ModelicaGround          { name: ModelicaIdentifier }
+
+
+// A Modelica circuit model — name, component declarations, connection equations.
+type ModelicaCircuitModel {
+  name: ModelicaIdentifier
+  components: List<ModelicaPassiveComponent>
+  connections: List<ModelicaConnection>
+}
+
+
+type ModelicaParseResult = Outcome<ModelicaCircuitModel>
+
+type ModelicaParse = fn(String) -> ModelicaParseResult
+
+type ModelicaEmit = fn(ModelicaCircuitModel) -> String
+
+type ModelicaIoContract {
+  emit: ModelicaEmit
+}

src/v4/test/claim/extdeps/spice_rc_modelica_claims.dag

@@ -0,0 +1,215 @@
+// src/v4/test/claim/extdeps/spice_rc_modelica_claims.dag
+//
+// Scope: Cross-paradigm BoolWitnessClaim witnesses for the RC passive circuit fixture.
+//        Proves the SAME composed .dag deck (rc_circuit.dag) feeds BOTH a SPICE causal
+//        netlist emitter AND a Modelica acausal model emitter with consistent values.
+//
+// Witnesses fall into three groups:
+//   (A) SPICE structural — each component is the correct coproduct variant.
+//   (B) Modelica structural — same check on the Modelica side.
+//   (C) Cross-paradigm (discriminating) — SPICE value lexeme == Modelica parameter value.
+//       Group C is the paradigm-falsification gate: it turns red when either projection
+//       diverges from the shared constants in rc_circuit.dag without updating its sibling.
+//
+// T-4.10 receipt: every claim is arm-sharp — a wrong variant (A/B) or a value mismatch (C)
+//   turns the witness red. The green is not vacuous.
+
+module v4.test.claim.extdeps.spice_rc_modelica_claims
+
+import v4.std.logic { Bool }
+import v4.std.verification { BoolWitness, BoolWitnessClaim, UnifiedTestClaim }
+import v4.extdeps.formats.spice {
+  Capacitor,
+  Component,
+  Resistor,
+  SpiceValue,
+  VoltageSource
+}
+import v4.extdeps.formats.modelica {
+  ModelicaCapacitor,
+  ModelicaConstantVoltage,
+  ModelicaPassiveComponent,
+  ModelicaResistor
+}
+import v4.test.fixture.rc_circuit {
+  rc_fixture_spice_c1,
+  rc_fixture_spice_r1,
+  rc_fixture_spice_v1,
+  rc_fixture_modelica_c1,
+  rc_fixture_modelica_r1,
+  rc_fixture_modelica_v1
+}
+
+
+// --- (A) SPICE structural witnesses -----------------------------------------
+
+fn rc_spice_r1_is_resistor() -> Bool {
+  match rc_fixture_spice_r1() {
+    Resistor { name: _, n_plus: _, n_minus: _, value: _ } => true
+    _ => false
+  }
+}
+
+fn rc_spice_c1_is_capacitor() -> Bool {
+  match rc_fixture_spice_c1() {
+    Capacitor { name: _, n_plus: _, n_minus: _, value: _ } => true
+    _ => false
+  }
+}
+
+fn rc_spice_v1_is_voltage_source() -> Bool {
+  match rc_fixture_spice_v1() {
+    VoltageSource { name: _, n_plus: _, n_minus: _, value: _ } => true
+    _ => false
+  }
+}
+
+
+// --- (B) Modelica structural witnesses --------------------------------------
+
+fn rc_modelica_r1_is_resistor() -> Bool {
+  match rc_fixture_modelica_r1() {
+    ModelicaResistor { name: _, r: _ } => true
+    _ => false
+  }
+}
+
+fn rc_modelica_c1_is_capacitor() -> Bool {
+  match rc_fixture_modelica_c1() {
+    ModelicaCapacitor { name: _, c: _ } => true
+    _ => false
+  }
+}
+
+fn rc_modelica_v1_is_voltage_source() -> Bool {
+  match rc_fixture_modelica_v1() {
+    ModelicaConstantVoltage { name: _, v: _ } => true
+    _ => false
+  }
+}
+
+
+// --- (C) Cross-paradigm discriminating witnesses ----------------------------
+// Each witness extracts the value lexeme from both projections and asserts equality.
+// Mutating rc_resistance_lexeme in spice.dag but not modelica.dag (or vice versa) → red.
+
+fn rc_spice_r1_value_lexeme() -> String {
+  match rc_fixture_spice_r1() {
+    Resistor { name: _, n_plus: _, n_minus: _, value: sv } => sv.lexeme
+    _ => ""
+  }
+}
+
+fn rc_modelica_r1_r_value() -> String {
+  match rc_fixture_modelica_r1() {
+    ModelicaResistor { name: _, r: rv } => rv
+    _ => ""
+  }
+}
+
+// Discriminates: mutate rc_resistance_lexeme in one projection → red.
+fn rc_cross_paradigm_r1_resistance_equal() -> Bool {
+  rc_spice_r1_value_lexeme() == rc_modelica_r1_r_value()
+}
+
+fn rc_spice_c1_value_lexeme() -> String {
+  match rc_fixture_spice_c1() {
+    Capacitor { name: _, n_plus: _, n_minus: _, value: sv } => sv.lexeme
+    _ => ""
+  }
+}
+
+fn rc_modelica_c1_c_value() -> String {
+  match rc_fixture_modelica_c1() {
+    ModelicaCapacitor { name: _, c: cv } => cv
+    _ => ""
+  }
+}
+
+fn rc_cross_paradigm_c1_capacitance_equal() -> Bool {
+  rc_spice_c1_value_lexeme() == rc_modelica_c1_c_value()
+}
+
+fn rc_spice_v1_value_lexeme() -> String {
+  match rc_fixture_spice_v1() {
+    VoltageSource { name: _, n_plus: _, n_minus: _, value: sv } => sv.lexeme
+    _ => ""
+  }
+}
+
+fn rc_modelica_v1_v_value() -> String {
+  match rc_fixture_modelica_v1() {
+    ModelicaConstantVoltage { name: _, v: vv } => vv
+    _ => ""
+  }
+}
+
+fn rc_cross_paradigm_v1_voltage_equal() -> Bool {
+  rc_spice_v1_value_lexeme() == rc_modelica_v1_v_value()
+}
+
+
+// --- UnifiedTestClaim data declarations -------------------------------------
+
+data unified_claim_rc_spice_r1_is_resistor: UnifiedTestClaim = BoolWitnessClaim {
+  witness: BoolWitness {
+    entry: "src/v4/test/claim/extdeps/spice_rc_modelica_claims.dag",
+    function: rc_spice_r1_is_resistor
+  }
+}
+
+data unified_claim_rc_spice_c1_is_capacitor: UnifiedTestClaim = BoolWitnessClaim {
+  witness: BoolWitness {
+    entry: "src/v4/test/claim/extdeps/spice_rc_modelica_claims.dag",
+    function: rc_spice_c1_is_capacitor
+  }
+}
+
+data unified_claim_rc_spice_v1_is_voltage_source: UnifiedTestClaim = BoolWitnessClaim {
+  witness: BoolWitness {
+    entry: "src/v4/test/claim/extdeps/spice_rc_modelica_claims.dag",
+    function: rc_spice_v1_is_voltage_source
+  }
+}
+
+data unified_claim_rc_modelica_r1_is_resistor: UnifiedTestClaim = BoolWitnessClaim {
+  witness: BoolWitness {
+    entry: "src/v4/test/claim/extdeps/spice_rc_modelica_claims.dag",
+    function: rc_modelica_r1_is_resistor
+  }
+}
+
+data unified_claim_rc_modelica_c1_is_capacitor: UnifiedTestClaim = BoolWitnessClaim {
+  witness: BoolWitness {
+    entry: "src/v4/test/claim/extdeps/spice_rc_modelica_claims.dag",
+    function: rc_modelica_c1_is_capacitor
+  }
+}
+
+data unified_claim_rc_modelica_v1_is_voltage_source: UnifiedTestClaim = BoolWitnessClaim {
+  witness: BoolWitness {
+    entry: "src/v4/test/claim/extdeps/spice_rc_modelica_claims.dag",
+    function: rc_modelica_v1_is_voltage_source
+  }
+}
+
+data unified_claim_rc_cross_paradigm_r1_resistance_equal: UnifiedTestClaim = BoolWitnessClaim {
+  witness: BoolWitness {
+    entry: "src/v4/test/claim/extdeps/spice_rc_modelica_claims.dag",
+    function: rc_cross_paradigm_r1_resistance_equal
+  }
+}
+
+data unified_claim_rc_cross_paradigm_c1_capacitance_equal: UnifiedTestClaim = BoolWitnessClaim {
+  witness: BoolWitness {
+    entry: "src/v4/test/claim/extdeps/spice_rc_modelica_claims.dag",
+    function: rc_cross_paradigm_c1_capacitance_equal
+  }
+}
+
+data unified_claim_rc_cross_paradigm_v1_voltage_equal: UnifiedTestClaim = BoolWitnessClaim {
+  witness: BoolWitness {
+    entry: "src/v4/test/claim/extdeps/spice_rc_modelica_claims.dag",
+    function: rc_cross_paradigm_v1_voltage_equal
+  }
+}

src/v4/test/claim/workflow/claim_witness_corpus_ci_runner.dag

@@ -511,6 +511,73 @@ data corpus_ci_gate_row_spice_rc_passive_deck_authority: ClaimWitnessCorpusClaim
   expected: ExpectPass
 }
 
+// SP-M3 dual-emission witnesses — T-4.10 paradigm-falsification gate.
+// Groups A+B: structural coproduct checks (SPICE causal, Modelica acausal).
+// Group C: cross-paradigm discriminating — same value lexeme in both projections.
+
+data corpus_ci_gate_row_rc_spice_r1_is_resistor: ClaimWitnessCorpusClaimRunRow = ClaimWitnessCorpusClaimRunRow {
+  label: "SP-M3 RC fixture: SPICE R1 is Resistor variant",
+  entry: "src/v4/test/claim/extdeps/spice_rc_modelica_claims.dag",
+  function: "rc_spice_r1_is_resistor",
+  expected: ExpectPass
+}
+
+data corpus_ci_gate_row_rc_spice_c1_is_capacitor: ClaimWitnessCorpusClaimRunRow = ClaimWitnessCorpusClaimRunRow {
+  label: "SP-M3 RC fixture: SPICE C1 is Capacitor variant",
+  entry: "src/v4/test/claim/extdeps/spice_rc_modelica_claims.dag",
+  function: "rc_spice_c1_is_capacitor",
+  expected: ExpectPass
+}
+
+data corpus_ci_gate_row_rc_spice_v1_is_voltage_source: ClaimWitnessCorpusClaimRunRow = ClaimWitnessCorpusClaimRunRow {
+  label: "SP-M3 RC fixture: SPICE V1 is VoltageSource variant",
+  entry: "src/v4/test/claim/extdeps/spice_rc_modelica_claims.dag",
+  function: "rc_spice_v1_is_voltage_source",
+  expected: ExpectPass
+}
+
+data corpus_ci_gate_row_rc_modelica_r1_is_resistor: ClaimWitnessCorpusClaimRunRow = ClaimWitnessCorpusClaimRunRow {
+  label: "SP-M3 RC fixture: Modelica R1 is ModelicaResistor variant",
+  entry: "src/v4/test/claim/extdeps/spice_rc_modelica_claims.dag",
+  function: "rc_modelica_r1_is_resistor",
+  expected: ExpectPass
+}
+
+data corpus_ci_gate_row_rc_modelica_c1_is_capacitor: ClaimWitnessCorpusClaimRunRow = ClaimWitnessCorpusClaimRunRow {
+  label: "SP-M3 RC fixture: Modelica C1 is ModelicaCapacitor variant",
+  entry: "src/v4/test/claim/extdeps/spice_rc_modelica_claims.dag",
+  function: "rc_modelica_c1_is_capacitor",
+  expected: ExpectPass
+}
+
+data corpus_ci_gate_row_rc_modelica_v1_is_voltage_source: ClaimWitnessCorpusClaimRunRow = ClaimWitnessCorpusClaimRunRow {
+  label: "SP-M3 RC fixture: Modelica V1 is ModelicaConstantVoltage variant",
+  entry: "src/v4/test/claim/extdeps/spice_rc_modelica_claims.dag",
+  function: "rc_modelica_v1_is_voltage_source",
+  expected: ExpectPass
+}
+
+data corpus_ci_gate_row_rc_cross_paradigm_r1_resistance_equal: ClaimWitnessCorpusClaimRunRow = ClaimWitnessCorpusClaimRunRow {
+  label: "SP-M3 dual-emission: R1 resistance lexeme equal across SPICE and Modelica",
+  entry: "src/v4/test/claim/extdeps/spice_rc_modelica_claims.dag",
+  function: "rc_cross_paradigm_r1_resistance_equal",
+  expected: ExpectPass
+}
+
+data corpus_ci_gate_row_rc_cross_paradigm_c1_capacitance_equal: ClaimWitnessCorpusClaimRunRow = ClaimWitnessCorpusClaimRunRow {
+  label: "SP-M3 dual-emission: C1 capacitance lexeme equal across SPICE and Modelica",
+  entry: "src/v4/test/claim/extdeps/spice_rc_modelica_claims.dag",
+  function: "rc_cross_paradigm_c1_capacitance_equal",
+  expected: ExpectPass
+}
+
+data corpus_ci_gate_row_rc_cross_paradigm_v1_voltage_equal: ClaimWitnessCorpusClaimRunRow = ClaimWitnessCorpusClaimRunRow {
+  label: "SP-M3 dual-emission: V1 supply voltage lexeme equal across SPICE and Modelica",
+  entry: "src/v4/test/claim/extdeps/spice_rc_modelica_claims.dag",
+  function: "rc_cross_paradigm_v1_voltage_equal",
+  expected: ExpectPass
+}
+
 // Sharded enrollment: two parallel CI jobs (~12–13 rows each). Wave A partition rows
 // co-locate with COMPREP emit shard-a (shared entry fixture cost); closure witnesses on shard-b.
 data claim_witness_corpus_shard_a_rows: List<ClaimWitnessCorpusClaimRunRow> = [
@@ -578,5 +645,14 @@ data claim_witness_corpus_shard_b_rows: List<ClaimWitnessCorpusClaimRunRow> = [
   corpus_ci_gate_row_self_host_stage_emission_equality_violates,
   corpus_ci_gate_row_spice_rc_ngspice_op,
   corpus_ci_gate_row_spice_rc_ngspice_nonempty,
-  corpus_ci_gate_row_spice_rc_passive_deck_authority
+  corpus_ci_gate_row_spice_rc_passive_deck_authority,
+  corpus_ci_gate_row_rc_spice_r1_is_resistor,
+  corpus_ci_gate_row_rc_spice_c1_is_capacitor,
+  corpus_ci_gate_row_rc_spice_v1_is_voltage_source,
+  corpus_ci_gate_row_rc_modelica_r1_is_resistor,
+  corpus_ci_gate_row_rc_modelica_c1_is_capacitor,
+  corpus_ci_gate_row_rc_modelica_v1_is_voltage_source,
+  corpus_ci_gate_row_rc_cross_paradigm_r1_resistance_equal,
+  corpus_ci_gate_row_rc_cross_paradigm_c1_capacitance_equal,
+  corpus_ci_gate_row_rc_cross_paradigm_v1_voltage_equal
 ]