feat: v0.1 foundation — five-language defensive ECM platform

Implement the v0.1 foundation for Robodog ECM with a five-language
architecture: Rust (core), SPARK (safety proofs), Idris2 (ABI),
Zig (FFI bridge), V-lang (API layer).

Rust core:
- ECM signal analysis (synthetic signals, FFT spectrum, interference detection)
- PQ crypto protocols (Kyber1024, Dilithium5, SPHINCS+ with round-trip tests)
- Formation control (5 shapes, separation checks, geometry computation)
- Defensive autonomy (collision avoidance, safe-state, comms loss handling)

SPARK safety:
- ecm_safety (frequency band bounds, power limits with postconditions)
- formation_safety (separation distance proofs via squared distance)
- autonomy_safety (comms timeout, speed bounds, safe-state selection)

Idris2 ABI:
- Types.idr (core type universe — no offensive action constructors)
- ECM.idr (power bounds, spectrum snapshots)
- Crypto.idr (key sizes with dependent type proofs)
- Formation.idr (integer-mm coordinates, separation proof witnesses)
- Foreign.idr (Zig FFI declarations)

Zig FFI:
- C-ABI signal classification, distance computation, formation positions
- Generated C header (robodog_ffi.h)
- Unit + integration tests

V-lang API:
- Full type mirror of core types
- Signal classification + defensive recommendation
- ABI verification types (round-trip proofs)

Infrastructure:
- Trustfile.a2ml: 780-line comprehensive trust contract (18 checks)
- EXPORT-CONTROL.md: ITAR/EAR/Wassenaar compliance framework
- run-checks.sh: executable Trustfile verification
- Fix SPDX typos (PLMP→PMPL) in 3 contractile files
- Fix LICENSE (MPL-2.0→PMPL-1.0-or-later as root)
- Replace old Haskell Trustfile with A2ML format
- Updated TOPOLOGY.md, STATE.a2ml, README.adoc, justfile, .gitignore

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

Author: hyperpolymath

.gitignore

@@ -24,7 +24,8 @@ Thumbs.db
 /.elixir_ls/
 
 # Rust
-# Cargo.lock  # Keep for binaries
+src/rust/target/
+# Cargo.lock  # Keep for reproducible builds
 
 # Elixir
 /cover/
@@ -50,6 +51,16 @@ __pycache__/
 *.ali
 /obj/
 /bin/
+src/spark/obj/
+src/spark/proof/
+
+# Zig
+ffi/zig/.zig-cache/
+ffi/zig/zig-out/
+
+# Idris2
+src/abi/build/
+src/abi/**/*.ibc
 
 # Haskell
 /.stack-work/

.machine_readable/STATE.a2ml

@@ -1,14 +1,44 @@
 # SPDX-License-Identifier: PMPL-1.0-or-later
 # STATE.a2ml — Project state checkpoint
-# Converted from STATE.scm on 2026-03-15
+# Updated: 2026-03-16
 
 [metadata]
 project = "robodog-ecm"
 version = "0.1.0"
-last-updated = "2026-03-15"
+last-updated = "2026-03-16"
 status = "active"
 
 [project-context]
 name = "robodog-ecm"
-completion-percentage = 0
-phase = "In development"
+completion-percentage = 40
+phase = "v0.1 Foundation"
+description = "Electronic Countermeasures & Defensive Technologies research platform"
+
+[technology-stack]
+core = "Rust"
+safety = "Ada/SPARK"
+abi = "Idris2"
+ffi = "Zig"
+api = "V-lang"
+
+[v0.1-progress]
+ecm-signal-analysis = "implemented — signals, detection, FFT spectrum"
+crypto-protocols = "implemented — Kyber1024, Dilithium5, SPHINCS+ round-trips"
+formation-control = "implemented — 5 shapes, separation checks, geometry"
+defensive-autonomy = "implemented — collision avoidance, safe-state, comms loss"
+spark-proofs = "specified — ecm_safety, formation_safety, autonomy_safety"
+idris2-abi = "implemented — Types, ECM, Crypto, Formation, Foreign"
+zig-ffi = "implemented — classify, distance, formation, C header"
+v-api = "implemented — full type mirror, classify, recommend"
+trustfile = "complete — 780 lines, 18 operational checks"
+export-control = "complete — ITAR/EAR/Wassenaar framework"
+
+[blockers]
+none = "No blockers for v0.1 completion"
+
+[next-actions]
+1 = "Run cargo test to verify Rust builds"
+2 = "Run zig build test to verify FFI"
+3 = "Run gnatprove to verify SPARK proofs"
+4 = "Run idris2 --check to verify ABI"
+5 = "Commit, push, mirror"

EXPORT-CONTROL.md

@@ -0,0 +1,118 @@
+<!-- SPDX-License-Identifier: PMPL-1.0-or-later -->
+<!-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk> -->
+
+# Export Control Compliance Framework
+
+## Classification
+
+This repository contains **dual-use defensive technologies** that may be
+subject to export control regulations including:
+
+- **UK Export Control Act 2002** and Strategic Export Control Lists
+- **Wassenaar Arrangement** Category 5 (Information Security) and Category 11 (Military Electronics)
+- **US ITAR** (International Traffic in Arms Regulations) — for reference only; UK law governs
+- **US EAR** (Export Administration Regulations) — for reference only; UK law governs
+
+### Technology Categories Present
+
+| Category | Description | Control Status |
+|----------|-------------|----------------|
+| ECM Signal Analysis | Spectrum analysis, interference detection | Dual-use (Wassenaar Cat 5) |
+| Post-Quantum Cryptography | Kyber, Dilithium, SPHINCS+ protocols | Potentially controlled (Cat 5A2) |
+| Formation Control | Distributed coordination for robotic systems | Dual-use (Cat 11) |
+| Autonomous Navigation | Collision avoidance, threat response | Dual-use (Cat 11) |
+
+## Defensive Use Only Policy
+
+### Permitted Uses
+
+1. **Defensive electronic countermeasures** — protecting communications from interception
+2. **Search and rescue coordination** — multi-robot disaster response
+3. **Secure communications research** — post-quantum protocol design and analysis
+4. **Academic research** — published, peer-reviewed defensive technology studies
+5. **Civilian infrastructure protection** — spectrum monitoring and anomaly detection
+
+### Explicitly Prohibited Uses
+
+1. **Offensive weapons systems** — targeting, kill chains, lethal autonomy
+2. **Mass surveillance** — tracking, profiling, or monitoring individuals
+3. **Offensive signal jamming** — disrupting civilian or emergency communications
+4. **Autonomous lethal decision-making** — any system that decides to use force
+5. **Export to embargoed or sanctioned entities** — per UK/EU/UN sanctions lists
+
+## Contributor Requirements
+
+### Before Contributing
+
+All contributors must:
+
+1. **Acknowledge** this export control policy by including in their first commit message:
+   ```
+   Export-Control-Acknowledged: yes
+   ```
+
+2. **Verify** they are not acting on behalf of any entity on:
+   - UK Consolidated List of Financial Sanctions Targets
+   - EU Consolidated Sanctions List
+   - UN Security Council Sanctions Committees lists
+
+3. **Ensure** their contributions serve exclusively defensive purposes
+
+### Code Review Requirements
+
+All pull requests involving the following must receive explicit export control review:
+
+- New cryptographic algorithm implementations
+- Signal processing or spectrum analysis modules
+- Autonomous decision-making logic
+- Formation control or swarm coordination protocols
+- Any hardware interface code (SDR, sensors, actuators)
+
+## Technical Controls
+
+### Source-Level Annotations
+
+All modules that handle controlled technology must include the annotation:
+
+```rust
+//! DEFENSIVE USE ONLY — Electronic countermeasures for protective applications.
+//! Export control classification: Wassenaar Category [X], UK ML [Y].
+//! See EXPORT-CONTROL.md for compliance requirements.
+```
+
+### Build-Time Verification
+
+The `Trustfile.a2ml` includes checks that:
+
+- No offensive capability markers exist in source code
+- Core modules declare defensive-use-only intent
+- Export control documentation is present and current
+
+### CI/CD Enforcement
+
+The `hypatia-scan` workflow includes export control scanning rules that flag:
+
+- Offensive terminology in code, comments, or documentation
+- Undocumented cryptographic implementations
+- Missing defensive-use annotations on controlled modules
+
+## Licensing Interaction
+
+The PMPL-1.0-or-later license does **not** override export control obligations.
+Even though the source code is publicly available under an open license, users
+remain responsible for compliance with all applicable export control laws in
+their jurisdiction.
+
+## Contact
+
+For export control queries:
+
+- **Author:** Jonathan D.A. Jewell
+- **Email:** j.d.a.jewell@open.ac.uk
+- **Institution:** The Open University
+
+## Document History
+
+| Date | Change |
+|------|--------|
+| 2026-03-16 | Initial export control framework for v0.1 |