Flow the design-consistency pass (#12) from integration/phase-3 into develop

Makefile

@@ -3,9 +3,10 @@ PILOT ?= build/pilot-validator/validate-sysml
 PILOT_BATCH ?= build/pilot-sysml-validator/validate-sysml-batch
 OPENSYSML_LIBRARIES ?= build/opensysml-src/internal/workspace/libs/stdlib/OpenSysML Libraries
 MODEL := $(sort $(wildcard model/*.sysml model/*.kerml))
-# The standalone pilot reads .sysml only (docs/findings/WP-G.md F-G01); the KerML library is
-# gated by the strict OpenSysML validate and by the batch pilot.
+# The standalone pilot wrapper reads .sysml only (docs/findings/WP-G.md F-G01), so the
+# mission-tier .kerml files go through the pinned batch oracle against the standard library alone.
 MODEL_SYSML := $(sort $(wildcard model/*.sysml))
+MODEL_KERML := $(sort $(wildcard model/*.kerml))
 
 # Tool tier: files that reference an OpenSysML library package (the packages shipped under
 # "OpenSysML Libraries"). The pilot resolves them only when that directory is loaded as an
@@ -14,6 +15,7 @@ MODEL_SYSML := $(sort $(wildcard model/*.sysml))
 OPENSYSML_PACKAGES := $(shell ls "$(OPENSYSML_LIBRARIES)" | grep -E '\.(sysml|kerml)$$' | sed 's/\..*//' | paste -sd '|')
 MODEL_TOOL := $(sort $(shell grep -lwE '$(OPENSYSML_PACKAGES)' $(MODEL)))
 MODEL_MISSION := $(filter-out $(MODEL_TOOL),$(MODEL_SYSML))
+MODEL_MISSION_KERML := $(filter-out $(MODEL_TOOL),$(MODEL_KERML))
 
 .PHONY: tools check validate pilot pilot-mission pilot-all house-rules runs runs-check tiers
 
@@ -29,12 +31,13 @@ pilot: pilot-mission pilot-all
 
 pilot-mission:
 	$(PILOT) $(MODEL_MISSION)
+	$(PILOT_BATCH) --root $(CURDIR) $(addprefix $(CURDIR)/,$(MODEL_MISSION_KERML))
 
 pilot-all:
 	$(PILOT_BATCH) --extension-library "$(OPENSYSML_LIBRARIES)" --root $(CURDIR) $(addprefix $(CURDIR)/,$(MODEL))
 
 tiers:
-	@echo "mission tier: $(MODEL_MISSION)"
+	@echo "mission tier: $(MODEL_MISSION) $(MODEL_MISSION_KERML)"
 	@echo "tool tier:    $(MODEL_TOOL)"
 
 house-rules:

docs/coverage/WP-B.md

@@ -35,18 +35,18 @@ Result legend: ✓ satisfied · ◐ construct in the model, tool result wrong or
 | SE-090 could | — | — | ○ |
 | SE-121 must | 32 : `MassBudget` (`dryEstimate`, `dryWithContingency`, `dryAllocation`, `launchMass`, `launcherCapability`, `dryCloses`, `launchCloses`), `requirement <'TS-121'>` | `wpb-tug-dry-mass` = 3725.5 kg; `wpb-tug-dry-mass-allocated` = 4300.9 kg; `wpb-mass-budget` = 12624 kg; `wpb-budgets-satisfy` | ✓ dry margin 30 %, launch margin 36 % |
 | SE-122 should | — | — | ○ |
-| SE-123 must | 31 : `Unit::operatingPower/standbyPower/operatingModes/standbyModes/poweredShare`, `PowerInMode`, `UnitsPowerInMode`; 32 : `TugPowerInMode`, `PowerBudget.demand<Mode>` for the eight flight modes, `<'TS-123'>` | `wpb-unit-power-safe` = 42 W, `wpb-unit-power-thrusting` = 24.75 kW (right); `wpb-power-budget-safe` = 0 W (wrong) | ◐ F-B01: per-set values are right, the rollup inside `powerBudget` evaluates to 0 W, so `powerBudgetCloses` "holds" vacuously |
-| SE-124 must | 32 : `calc def ArrayPower`, `PowerBudget.arrayAtAphelionEol` from `TethysEnvironment::SolarFlux(amaranth.orbit.aphelionAu)` and `arrayWings.endOfLifeFactor` | `wpb-budgets-satisfy` (`thrustingCloses`) | ◐ capability 39.76 kW right; demand side F-B01 |
-| SE-125 must | 32 : `EnergyBudget` (DRO eclipse 4 h, launch to arrays 1.5 h, `maximumDepthOfDischarge`), `<'TS-125'>` | `wpb-budgets-satisfy` | ◐ usable 8640 W·h right; demand side F-B01; static budget, no state-machine SOC run |
+| SE-123 must | 31 : `Unit::operatingPower/standbyPower/operatingModes/standbyModes/poweredShare`, `PowerInMode`, `UnitsPowerInMode`; 32 : `TugPowerInMode`, `PowerBudget.demand<Mode>` for the eight flight modes, `<'TS-123'>` | `wpb-unit-power-safe` = 42 W, `wpb-unit-power-thrusting` = 24.75 kW (right); `wpb-power-budget-safe` = 0 W (wrong) | ◐ on the pinned build F-B01 zeroes the rollup so `powerBudgetCloses` "holds" vacuously; on the F-B01-fixed build `demandThrusting` = 35 518 W against `arrayAtAphelionEol` = 39 757 W is `thrustingMargin` = 0.119 < the 0.15 policy — **power while thrusting does not close**; which attribute closes it (array rating, string draw or margin policy) is the pending maintainer decision |
+| SE-124 must | 32 : `calc def ArrayPower`, `PowerBudget.arrayAtAphelionEol` from `TethysEnvironment::SolarFlux(amaranth.orbit.aphelionAu)` and `arrayWings.endOfLifeFactor` | `wpb-budgets-satisfy` (`thrustingCloses`) | ◐ capability 39.76 kW right; the demand it is checked against closes in every mode but `thrust` (SE-123) |
+| SE-125 must | 32 : `EnergyBudget` (DRO eclipse 4 h, launch to arrays 1.5 h, `maximumDepthOfDischarge`), `<'TS-125'>` | `wpb-budgets-satisfy` | ◐ usable 8640 W·h right; on the F-B01-fixed build `eclipseEnergy` = 3 588 W·h closes; `droEclipse = 4 h` is asserted, not derived (SE-264 open); static budget, no state-machine SOC run |
 | SE-126 must | 32 : `InspectorEnergyBudget`, `<'TS-126'>` | `wpb-budgets-satisfy` | ✓ 55 W·h of 108 W·h usable |
 | SE-127 must | 32 : `DataBudget` (`generatingRate`, `dailyGenerated`, `dailyDownlink`, `storageDemand`), `<'TS-127'>` | `wpb-data-daily` = 70.6 Gbit; `wpb-budgets-satisfy` | ✓ against 90 Gbit/day and 4 TB |
-| SE-128 must | — | — | — link budget is WP-D's |
-| SE-129 must | — | — | — relay link is WP-D's |
-| SE-130 must | 32 : `deltaVOutbound/Rendezvous/Return/Insertion`, `missedThrustMargin`, `XenonForMission` (four arcs on the running mass with the case's body attached), `PropellantBudget.thrustAtAphelion` via `TethysEnvironment::SepThrust`, `<'TS-130'>` | `wpb-xenon-large`; `wpb-sep-thrust-aphelion` = 1.73 N; `wpb-thrusting-time-large` | ✓ SEP string closed power → thrust → mass flow → thrusting time |
+| SE-128 must | — | — | — link budget is WP-D's; its 60 × 10⁶ km maximum range is asserted, not derived from the trajectory (domain list O7) |
+| SE-129 must | — | — | — relay link is WP-D's; same asserted range envelope as SE-128 |
+| SE-130 must | 32 : `deltaVOutbound/Rendezvous/Return/Insertion`, `missedThrustMargin`, `XenonForMission` (four arcs on the running mass with the case's body attached), `PropellantBudget.thrustAtAphelion` via `TethysEnvironment::SepThrust`, `<'TS-130'>` | `wpb-xenon-large`; `wpb-sep-thrust-aphelion` = 1.73 N; `wpb-thrusting-time-large` | ✓ SEP string closed power → thrust → mass flow → thrusting time; `70:LowThrustTransferAnalysis` reads the same `transferBook`, so the budget and the analysis book agree that every design case returns |
 | SE-131 must | 32 : `PropellantBudget` (xenon per case, residuals, `tankCapacity`, `throughputLife`), `HydrazineBudget` (`DespinPropellant` per case, proximity Δv, stack control), `<'TS-130'>`, `<'TS-131'>` | `wpb-xenon-large`, `wpb-hydrazine-large` = 290 kg of 388 kg usable; `wpb-budgets-satisfy` | ✓ |
 | SE-132 must | 32 : `RootSumSquareDegrees`, `PointingBudget.antennaPointingErrorDegrees` vs `antennaAllocation`, `<'TS-132'>` | `wpb-pointing-antenna` = 0.0232° (allocation 0.05°) | ✓ |
 | SE-133 should | 32 : `PointingBudget.thrustVectorErrorDegrees` (centre-of-mass knowledge, thruster alignment, gimbal) | `wpb-budgets-satisfy` | ✓ 0.229° of 0.5° |
-| SE-134 must | 31 : `min/maxOperatingTemperature`, `predictedHot/ColdTemperature` on every unit; 32 : `RadiatorRejection`, `ThermalBudget` (hot case, cold-case heaters, `forAll` limits), `<'TS-134'>` | `wpb-radiator-capacity` = 7480 W; `wpb-budgets-satisfy` | ◐ limits and capacity right; `hotCaseHeat` demand side F-B01 |
+| SE-134 must | 31 : `min/maxOperatingTemperature`, `predictedHot/ColdTemperature` on every unit; 32 : `RadiatorRejection`, `ThermalBudget` (hot case, cold-case heaters, `forAll` limits), `<'TS-134'>` | `wpb-radiator-capacity` = 7480 W; `wpb-budgets-satisfy` | ◐ limits and capacity right; on the F-B01-fixed build `hotCaseHeat` = 5 737 W closes against 7 480 W; pinned run still vacuous (F-B01) |
 | SE-135 must | 32 : `CaptureLoadBudget` (contact force of the heavy case, cinch preload, thrust load vs `bag.cinchLoadCapacity`), `<'TS-135'>` — the small-body reading of the entry-loads rows | `wpb-budgets-satisfy` | ✓ 14.4 kN of 20 kN |
 | SE-136 must | as SE-135 | | ✓ |
 | SE-137 should | 31 : `Unit::doseRating : AbsorbedDoseValue`; 32 : `RadiationBudget` (150 Gy × RDM 2, `forAll`), `<'TS-137'>` | `wpb-budgets-satisfy` | ✓ |
@@ -57,15 +57,15 @@ Result legend: ✓ satisfied · ◐ construct in the model, tool result wrong or
 | SE-142 should | 31 : `FlightComputer.processorCapacityMips/LoadMips/memoryCapacity/memoryAllocated`; 32 : `ProcessorBudget`, `<'TS-142'>` | `wpb-budgets-satisfy` | ✓ 50 % reserve |
 | SE-143 should | — | — | — WP-D |
 | SE-144 could | — | — | ○ |
-| SE-145 must | 30 : `attribute def MarginPolicyRow`, `srrPolicy`/`pdrPolicy`/`cdrPolicy`/`acceptancePolicy`, `activePolicy`, `ContingencyFor`, `WithContingency`, `MarginFraction`, `constraint def ClosesWithMargin`/`WithinLimit`/`ReserveNotNegative`; every `assert constraint … : ClosesWithMargin { … in policy = activePolicy; }` in 32 | `wpb-margin-policy-alone` = 0.1 (right, file alone); `wpb-margin-policy` = 0.2 (wrong, whole model), 120.0, 0.2, holds | ◐ policy complete and referenced by every budget; enum equality in the whole model is F-B01 |
+| SE-145 must | 30 : `attribute def MarginPolicyRow`, `srrPolicy`/`pdrPolicy`/`cdrPolicy`/`acceptancePolicy`, `activePolicy`, `ContingencyFor`, `WithContingency`, `MarginFraction`, `constraint def ClosesWithMargin`/`WithinLimit`/`ReserveNotNegative`; every `assert constraint … : ClosesWithMargin { … in policy = activePolicy; }` in 32 | `wpb-margin-policy-alone` = 0.1 (right, file alone); `wpb-margin-policy` = 0.2 (wrong, whole model), 120.0, 0.2, holds | ◐ policy complete and referenced by every budget; on the F-B01-fixed build mass, xenon, energy and thermal close under `pdrPolicy`, power while thrusting does not (SE-123); pinned run still vacuous (F-B01) |
 | SE-146 should | — | — | ○ tool tier (`DocumentQueries`); candidate `model/33-budget-report-tooling.sysml` |
 
 ## LANG rows
 
 | Row | File : element | Proving command | Result |
 | --- | --- | --- | --- |
 | LANG-506–510 attributes | 31 : `attribute def` — ; `Unit` attributes `mass : MassValue`, `operatingPower : PowerValue`, …; 30 : `attribute def MarginPolicyRow`, 32 : `attribute def TargetCase` | `make validate`, `make pilot` | ✓ |
-| LANG-511–518 enumerations | 31 : `enum def TugMode` (nine literals); 30 : `enum def Maturity`, `enum def ReviewGate`; enum-valued attributes and sequences (`allFlightModes : TugMode[*]`) | `make validate`, `make pilot`; `wpb-margin-policy` | ✓ (membership evaluation: F-B01) |
+| LANG-511–518 enumerations | 31 : `enum def TugMode` (sixteen literals, the one mode vocabulary); 30 : `enum def Maturity`, `enum def ReviewGate`; enum-valued attributes and sequences (`allFlightModes : TugMode[*]`) | `make validate`, `make pilot`; `wpb-margin-policy` | ✓ (membership evaluation: F-B01) |
 | LANG-547–551 parts | 31 : 60 `part def`s (`Unit`, `PassiveUnit`, `ElectronicUnit`, `Assembly`, ten subsystems, every unit type), `part argentDesign : ArgentTug` with redefinitions `part :>> sep : ArgentPropulsion`, sequences `part :>> units = (…)` | `instantiate-system` run | ✓ |
 | LANG-742–751 calculations | 31 : `PowerInMode`, `HeatInMode`, `UnitsPowerInMode`, `UnitsHeatInMode`; 30 : `ContingencyFor`, `WithContingency`, `MarginFraction`; 32 : `ArrayPower`, `ExpNeg`, `PropellantFor`, `MassFlowRate`, `RootSumSquareDegrees`, `Survival`, `SetReliability` (body items + `return`), `XenonForMission`, `DespinPropellant`, `RadiatorRejection`, `TugPowerInMode`, `TugHeatInMode`, `UnitsDataRate` | `wpb-*` runs | ✓ |
 | quantities and units | every physical quantity ISQ-typed with an SI literal: `[kg]`, `[W]`, `[K]`, `[Gy]`, `['W⋅h']`, `['bit/s']`, `['A⋅m²']`, `['°']`, `[N]`, `[Pa]`, `[Hz]`, `['m²']`, `[d]`, `[h]`; `[GHz]`/`[MPa]`/`[GB]` are not SI library literals, so `32.0e9 [Hz]`, `12.0e6 [Pa]`, `4.0e12 [B]` | `make validate`, `make pilot` | ✓ |

docs/coverage/WP-C.md

@@ -8,9 +8,11 @@ Files: `model/40-inspector.sysml` (`TethysInspectorDetail`), `model/41-capture-s
 `sysml -validate -strict -warnings-as-errors` and by the pilot validator.
 
 Target uncertainty: every target-dependent number is carried over the cases of
-`TethysCaptureSystem::CaptureTargetCase` (small 181 t, nominal 362 t, large 1 010 t, fast-spin
-120 s, tumbling) — the envelope is asserted to hold for the first two and asserted *not* to hold
-for the other three (`runs/wpc-envelope-cases.txt`), and the despin propellant, angular momentum
+`TethysTarget::CaptureTargetCase` (small 213 t, nominal 362 t, large 506 t, densest 576 t, largest 987 t, fast-spin
+120 s, tumbling) — the mechanism's envelope is asserted to hold for the small, nominal, large and
+densest bodies and asserted *not* to hold for the largest (100 s spin), fast-spin and tumbling
+ones (`runs/wpc-envelope-cases.txt`); the densest body is refused at commit by the return
+envelope (`TethysBudgets::captureCommitEnvelope`) instead, and the despin propellant, angular momentum
 and surface speed are computed per case (`runs/wpc-target-cases.txt`).
 
 ## SE rows (reading per `docs/small-body-domain-list.md` §8)

docs/coverage/WP-D.md

@@ -16,7 +16,7 @@ recorded with OpenSysML built from `develop` at `0a5fa2d94` (`v0.10.1-2054-g0a5f
 | SE-102 | must | `51 : PacketPort` (`out item telemetry`, `in item command`), `~PacketPort` end of `PacketInterface`; `50 : ProductPort`; every ICD `end` typed by a backbone port def or its conjugate | `make validate`; `make house-rules` (`portUsageIsTyped` over 3 647 elements) | satisfied — 0 violations (`runs/house-rules.txt`) |
 | SE-103 | must | `51 : TugInspectorIcd <'TI-001'>` (electrical + umbilical telemetry, `bind`/`binding` of keep-alive voltage and power), `InspectorDispenserIcd <'TI-007'>` (mechanical: preload, ejection speed), `InspectorThermalIcd <'TI-008'>` (thermal), `InspectorRelayIcd <'TI-004'>` (RF, after release); `IcdFlightSegment::dispenser` connects the backbone structure ports | `make validate`, `make pilot` | satisfied for the four disciplines; `InspectorDispenserIcd` and `InspectorThermalIcd` specialise the backbone `InspectorDispenserInterface` and `InspectorThermalInterface` and connect `ThermalControl::inspectorThermal` to `Inspector::stowedThermal` |
 | SE-104 | must | `51 : LaunchIcd <'TI-002'>` — adapter and fairing envelope, `axialQuasiStatic`, `lateralQuasiStatic`, `sineVibration`, `shockResponse` (`AccelerationValue`), `acousticLevelDb`, stack mass and CoM limits, `separationSpeed`, `tipOffRate`, injection C3 tolerance, umbilical; `bind` of the load and `separable` across both ends | `make validate`, `make pilot` | satisfied |
-| SE-105 | must | `51 : SpaceGroundIcd <'TI-003'>` — uplink/X/Ka frequencies, modulation and coding enums, rate envelope (`BinaryDigitRateValue`), ranging tone, packet protocol, `bind` of the carrier frequency, RF `flow`s both ways; `52 : xDownlinkAtMaximumRange`, `xUplinkAtMaximumRange`, `kaDownlinkAtTargetRange`, `xDownlinkInDro` | `run wpd-link-margins` = `-calc "TethysLinkBudgets::MarginReport(TethysLinkBudgets::xDownlinkAtMaximumRange)" …`; `run wpd-link-satisfy` = `-satisfy=TethysLinkBudgets` | satisfied — margins 10.7 dB (X down, 1 Mbit/s, 60e6 km), 46.3 dB (X up), 10.0 dB (Ka, 4 Mbit/s, 45e6 km), 46.6 dB (DRO, 4 Mbit/s); TG-001…TG-004 hold |
+| SE-105 | must | `51 : SpaceGroundIcd <'TI-003'>` — uplink/X/Ka frequencies, modulation and coding enums, rate envelope (`BinaryDigitRateValue`), ranging tone, packet protocol, `bind` of the carrier frequency, RF `flow`s both ways; `52 : xDownlinkAtMaximumRange`, `xUplinkAtMaximumRange`, `kaDownlinkAtTargetRange`, `xDownlinkInDro` | `run wpd-link-margins` = `-calc "TethysLinkBudgets::MarginReport(TethysLinkBudgets::xDownlinkAtMaximumRange)" …`; `run wpd-link-satisfy` = `-satisfy=TethysLinkBudgets` | satisfied for the asserted ranges — the 60e6 / 45e6 km sizing cases are not yet derived from the trajectory (domain list O7, SE-128), so the margins hold against an assumption; margins 10.7 dB (X down, 1 Mbit/s, 60e6 km), 46.3 dB (X up), 10.0 dB (Ka, 4 Mbit/s, 45e6 km), 46.6 dB (DRO, 4 Mbit/s); TG-001…TG-004 hold |
 | SE-106 | must | `51 : InspectorRelayIcd <'TI-004'>` (frequencies, GMSK, rate, 50 m–5 km window, off-boresight, daily window); `52 : proximityReturnLink`, `CharacterisationDataVolume`, `RelayDaysRequired`, `RelayLoadByTarget` (small 4 m / nominal 6.8 m / large 9.5 m variants), `TG-006` | `run wpd-relay-load` = `-calc "TethysLinkBudgets::CharacterisationDataVolume(4.0, 0.005, 40.0, 12.0)" … -calc "TethysLinkBudgets::RelayDaysRequired(5443751750.14, 1.0e6, 3240.0)"`; `run wpd-link-margins`; `run wpd-link-satisfy` | satisfied — 0.97 / 2.79 / 5.44 Gbit to relay for the three target cases, 0.30 / 0.86 / 1.68 contact days against the 30-day allowance; proximity margin 40.8 dB at 5 km; TG-005, TG-006 hold |
 | SE-107 | must | `51 : PowerIcd <'TI-011'>`, `HighVoltagePowerIcd <'TI-012'>`, `DataBusIcd <'TI-013'>`, `ThermalIcd <'TI-014'>`, `PropellantFeedIcd <'TI-009'>` with `flow`s typed `ElectricalPower`, `Telemetry`/`Telecommand`, `Heat`, `Propellant`; `PropellantLoading` connects both fill ports | `make validate`, `make pilot` | satisfied for the ICD classes; the backbone's eight `PowerInterface` usages in `Tug` stay typed by the backbone def (retyping them needs an edit to `05-tug.sysml`) |
 | SE-108 | should | `51 : metadata def InterfaceControl { authority; document; revision; status : IcdStatus }`, `@InterfaceControl` on every one of the 14 ICD interface defs | `make validate` | satisfied |