Architecture & Scale
AstroMesh Round 2 — Challenge #518, Constraint Awareness: Completion Signal
1. The shape of it
┌──────────────────────────────────────────┐
│ CONSTRAINT ENGINE │
│ dev/constraints/engine.js │
│ │
rulebook ─────────► │ rulebook + context → completion signal │
context ─────────► │ │
│ COMPLETE · PARTIAL · BLOCKED · │
│ UNRESOLVED │
│ │
│ Knows nothing about satellites. │
└──────────────┬───────────────────────────┘
│
┌──────────────────┬───────────┴───────────┬────────────────────┐
▼ ▼ ▼ ▼
┌───────────┐ ┌─────────────┐ ┌──────────────┐ ┌──────────────┐
│ maneuver │ │ re-entry │ │ authored │ │ release │
│ rulebook │ │ rulebook │ │ (English → │ │ gate │
│ 19 rules │ │ 9 rules │ │ verified) │ │ 10 rules │
└───────────┘ └─────────────┘ └──────────────┘ └──────────────┘
│ │ NOT SPACE —
│ │ the portability
▼ ▼ proof
┌──────────────────────────────────────────────────────────────┐
│ vote gate (409) · deterministic poll · propellant ledger │
└──────────────────────────────────────────────────────────────┘
The engine is the product. The rulebooks are data. That separation is what makes the capability theme-independent, and it is verified by a test that runs a software release gate through the same code path.
2. Where the inputs come from
| Layer | Source | Live? | Feeds |
|---|---|---|---|
| Catalogue | Space-Track, ~31k objects, 3×/day | yes | FR-00, FR-03, FR-22 |
| Conjunctions | our own SGP4 screening | computed | FR-01, FR-10, FR-12 |
| CDMs | 19th SDS via Space-Track | yes | FR-11 |
| Operator ephemeris | SpaceX Starlink Space Safety | operator-gated (403) | FR-11 — reports UNEVALUATED without access |
| Space weather | NOAA SWPC, no API key | yes, 5 min | FR-19, FR-20, FR-21 |
| Solar X-ray | NOAA GOES XRS, two bands | yes, 2 min | FR-19 predictive deadline |
| Ground consequence | GeoNames + OpenFlights + Natural Earth | static, 4.4 MB | FR-17a, FR-17b, FR-23 |
| Maritime | not loaded | no | FR-24 → UNEVALUATED, never "clear water" |
| Models | trained offline, shipped as JSON | n/a | FR-07, FR-10, FR-13 |
Every absent source degrades to UNEVALUATED. Nothing defaults, nothing imputes, nothing assumes a quiet Sun or an empty ocean.
3. Scale
What it handles today
| Quantity | Measured |
|---|---|
| Catalogue screened | 31,572 objects |
| Conjunction screening | apogee/perigee sieve → coarse → fine TCA refine |
| Ground raster | 259,200 cells, 100% characterised, 4.4 MB |
| Monte Carlo footprint | 20,000 samples per deorbit, deterministic |
| Constraint evaluation | 28 rules × N events, pure arithmetic, no I/O |
| Refresh cadence | 8 h catalogue · 5 min space weather · 2 min X-ray |
| Consensus | 4 nodes, quorum 3, sub-second failover |
| Formal verification | 148,163 states exhaustively checked |
How each part scales
The constraint engine is the easy part. It is stateless and linear in
rules × events with no I/O — 28 rules over 38 events is roughly a thousand comparisons.
100,000 events would still be milliseconds. It is not, and will not become, the bottleneck.
Conjunction screening is the real cost. All-pairs over a catalogue is O(n²) — for 31,572 objects that is half a billion pairs. The sieve is what makes it tractable:
apogee/perigee filter O(n²) pair rejection on scalars, no propagation
↓ ~99% rejected
coarse screen 300 s steps over a 24 h window
↓
fine TCA refinement only for candidates inside the gate
Naming the ceiling. At ~31k objects a full screening pass takes 1–2 minutes on one core. At 100k it becomes the bottleneck — which is precisely where a GNN pre-filter earns its place (published work reports 100,000 objects in 920 ms at 90.3% recall). The architecture for that is already the one we use elsewhere: the model proposes, the physics disposes, and anything flagged-but-unverified sits at UNRESOLVED rather than being silently trusted.
Consensus. Quorum is ⌈n/2⌉+1; nothing assumes four nodes. Forty operators works with the
same protocol and the same TLA+ model, re-checked with a larger Nodes constant.
The demo path has no scaling risk at all. SNAPSHOT=1 serves 13.9 MB of frozen real data,
and FR-00 still audits its age.
4. Failure behaviour
This is the part worth reading twice, because it is the product.
| Failure | What happens |
|---|---|
| Space-Track stale | FR-00 BLOCKS the whole system. It audits our own evidence first |
| NOAA down | FR-19/FR-21 → UNEVALUATED → UNRESOLVED. Never "conditions are fine" |
| GOES X-ray down | FR-19 loses its predictive deadline, keeps its current-state check |
| Operator feed gated | FR-11 → UNEVALUATED. We never label screening-grade data operator-grade |
| Model artefact absent | The rule it feeds reports UNEVALUATED. No default, no imputation |
| Model artefact mismatched | REFUSED at load. Better no model than one fed the wrong columns |
| A rule evaluator throws | That rule becomes UNEVALUATED, never SATISFIED |
| Sources disagree | UNRESOLVED. We do not average two disagreeing measurements |
| Verifier unreachable | An authored rule is refused, not admitted unverified |
| Snapshot goes stale | FR-00 blocks, exactly as with live data |
There is no path in this system where absence becomes permission.
5. Verification
| What | How | Result |
|---|---|---|
| Engine semantics | node dev/constraints/engine.test.js |
65/65, offline, <1 s |
| Vote determinism | same event × 200 polls | 1 distinct outcome |
| Formal safety | tlc -config ConstraintGate.cfg |
148,163 states, 0 violations |
| The old bug | tlc -config ConstraintGateBug.cfg |
2-state counterexample |
| Propagator | vs ESA dSGP4, 800 propagations | 0.000 m |
| Classifier | real catalogue rows | ISS→CREWED, STARLINK→AUTOMATED_COLA, DEB→NONMANEUVERABLE |
| Portability | release-gate rulebook | 4/4 states, 0 engine changes |
6. Honest limitations
Stated here rather than waiting to be asked.
- Population is settlement-based (GeoNames ≥15,000), not gridded. Rural exposure is undercounted, so our casualty numbers are optimistic. GHSL at 100 m is the upgrade.
- Maritime exposure is not modelled. FR-24 reports UNEVALUATED.
- Debris casualty area is taken from published survivability data, not modelled. Fragment ablation is a research programme.
- The classifier's MANEUVERABLE precision is 0.52. Weak supervision from names; the objects it exists for are the ones we cannot score.
- The maneuver detector separates active from inert by only 3.2% vs 2.0%. A robust z-score adapts to each object, so a constellation that manoeuvres constantly gets a wide baseline and its own burns stop looking anomalous. Most useful on objects that manoeuvre rarely.
- The flare forecast projects the peak of a flare already beginning. It does not predict onset from a quiet Sun.
- Propellant state is operator-declared and simulated here; no public feed exists. Flagged
simulated: truein every payload. Consumption is real; the starting balance is declared. - APPROVED is a coordination decision, not a command to hardware.