Skip to content

EXPLAINME.adoc

Latest commit

 

History

History
115 lines (81 loc) · 3.81 KB

EXPLAINME.adoc

File metadata and controls

115 lines (81 loc) · 3.81 KB
Raw

robodog-defensive-systems-lab — Evidence for Public Claims

Table of Contents

This file maps the README framing to repository artifacts. It is intentionally limited to non-operational research claims: synthetic simulation, communications resilience, secure coordination, autonomy-safety, and formal interface boundaries.

Core Claims and Evidence

Claim 1: Post-Quantum Cryptographic Families Are Represented

The README describes research involving:

ML-KEM, ML-DSA, and SLH-DSA, the NIST-standardised post-quantum cryptographic families derived from the Kyber, Dilithium, and SPHINCS+ submissions.

Evidence: src/rust/src/lib.rs, src/abi/Crypto.idr, and the Rust test suites exercise post-quantum protocol interfaces and round-trip behaviour.

Caveat: cryptographic completeness should be evaluated from the current source and tests. This repository should not be read as claiming independently proven cryptographic implementations.

Claim 2: Formal and Interface Safety Boundaries Exist

The README describes an Idris2 ABI layer, a Zig FFI layer, and Ada/SPARK safety specifications.

Evidence:

  • src/abi/ contains Idris2 interface definitions for typed signal, cryptographic, formation, and foreign-function boundaries.

  • ffi/zig/src/main.zig contains the Zig FFI bridge.

  • src/spark/src/ contains SPARK specifications for bounded safety behaviour.

Caveat: these are boundary and specification artifacts. They do not make every Rust implementation mechanically verified unless the relevant proof and test coverage is present.

Claim 3: Publication Safety and Compliance Boundaries Are Documented

The README states that the public repository is non-operational and limited to defensive research.

Evidence:

  • README.adoc defines the safety and publication boundary.

  • DEFENSIVE-USE.md defines the repository use policy.

  • EXPORT-CONTROL.md records compliance and export-control review context.

  • contractiles/trust/Trustfile.a2ml records provenance, safety-boundary, and compliance metadata checks.

Caveat: these policy files do not replace legal advice and do not authorise any restricted activity. Contributors and users remain responsible for applicable laws and institutional policies.

File Map

Path Contents and Purpose

src/rust/src/ecm/

Synthetic spectrum-awareness and interference-classification logic. Public examples should use synthetic data only.

src/rust/src/crypto/

Post-quantum secure-communication protocol experiments and wrappers.

src/rust/src/formation/

Formation geometry, separation checks, and coordination primitives for bounded simulation.

src/rust/src/autonomy/

Safe-state, communication-loss, and collision-avoidance behaviour.

src/abi/

Idris2 interface contracts for typed boundaries and foreign interfaces.

ffi/zig/

Zig FFI bridge and C-ABI-facing interface experiments.

src/spark/

Ada/SPARK safety specifications for selected safety boundaries.

TEST-NEEDS.md

Test coverage report for synthetic, bounded research scenarios.

EXPORT-CONTROL.md

Export-control and publication-safety notice.

DEFENSIVE-USE.md

Defensive-use policy and out-of-scope list.

contractiles/trust/Trustfile.a2ml

Trust-boundary metadata and repository checks.

Relationship to Other Work

This repository shares the hyperpolymath pattern of formal boundaries with a Rust implementation core and explicit FFI surfaces. The public positioning here is narrower: synthetic simulation, resilience, secure coordination, safety cases, and formal/interface boundaries.

Questions

Open an issue or reach out at j.d.a.jewell@open.ac.uk for questions about the research boundary, formal interface model, or compliance documentation.