diff --git a/README.adoc b/README.adoc index 5f8c6a0..80c4cf6 100644 --- a/README.adoc +++ b/README.adoc @@ -96,6 +96,8 @@ The repository is organised around a simulation-first safety boundary: See link:TOPOLOGY.md[TOPOLOGY.md] for the architecture map and completion dashboard. +The research programme is documented in link:docs/programme-plan.adoc[docs/programme-plan.adoc]. Mathematical extensions and their proof ladder are tracked in link:docs/mathematical-agenda.adoc[docs/mathematical-agenda.adoc]. External reports are received through link:docs/incoming-reports.adoc[docs/incoming-reports.adoc]. The educational BFT/type comparator is described in link:docs/bft-type-comparator.adoc[docs/bft-type-comparator.adoc]. + == Technology Stack [cols="1,2,2"] diff --git a/docs/bft-type-comparator.adoc b/docs/bft-type-comparator.adoc new file mode 100644 index 0000000..fd89825 --- /dev/null +++ b/docs/bft-type-comparator.adoc @@ -0,0 +1,32 @@ += BFT and Type-Augmented Design Comparator +:toc: + +== Purpose + +`www/index.html` is an educational visualisation prompted by a comparison between Byzantine Fault Tolerance (BFT) and ideas associated with epistemic types, proof transport, echo types, choreographies, and tropical grading. + +It is deliberately a *comparator*, not a claim of equivalence. BFT and typed evidence answer different questions: + +* BFT: can non-faulty replicas agree despite a specified class of faults, network model, and quorum assumptions? +* Typed evidence: which states can a component accept, and what machine-checkable evidence accompanies them? + +A signature authenticates origin; it does not authenticate truth. A proof term proves only the proposition actually formalised, under the soundness assumptions of its checker, axioms, specifications, and data sources. Typed boundaries therefore complement BFT; they do not remove quorum intersection, liveness, membership, recovery, or a threat model. + +== What is grounded here + +The repository contains Idris2 ABI declarations, Rust ECM code and tests, and SPARK safety modules. The immediately actionable synthesis is evidence-aware safety boundaries: distinguish measured, inferred, stale, degraded, and rejected inputs, and make unsafe actuator commands unrepresentable or rejected. + +The names `epistemic-types`, `echo-types`, `choreographic`, `tropical`, `residual evidence`, `Januskey`, and `Absolute Zero` should be treated as proposed research modules until their repositories expose formal definitions, semantics, soundness claims, and executable tests. The visualisation labels their useful hypotheses without presenting them as established results. + +== Suggested progression + +. State faults explicitly: crash, omission, equivocation, stale data, malicious sensor, compromised runtime, and unsafe FFI. +. Define one invariant, for example: `unsafe actuator command => no valid evidence path`. +. Build a minimal 3f+1 trace and a typed admission trace, including counterexamples. +. Prove/check the boundary with Idris2, Rust, and SPARK where appropriate. +. Measure latency, memory, proof-check cost, false rejection, and recovery behaviour. +. Add named extensions only when each has an operational semantics and a testable contract. + +== Limitations + +Echo-like witnesses can preserve structured provenance of loss but cannot recover information never received. A choreography can constrain protocol shape but cannot make a compromised runtime honest. Quantitative path costs can make budgets explicit but do not themselves establish safety. These distinctions are the central teaching point. diff --git a/docs/incoming-reports.adoc b/docs/incoming-reports.adoc new file mode 100644 index 0000000..f0e4b2a --- /dev/null +++ b/docs/incoming-reports.adoc @@ -0,0 +1,58 @@ += Incoming Research Reports +:toc: + +This is the receiving surface for results from related repositories. Copy the compact hand-off from each project here, then verify every referenced theorem, test, file, and assumption locally before using it in Robodog design. + +== Intake rules + +. Preserve the submitting repository, revision, date, and exact status. +. Separate formal proof, executable test, documentation, and speculation. +. Do not upgrade a result when importing it. +. Record counterexamples and retractions beside positive results. +. Link the result to a Robodog issue or experiment. +. A result is not an implementation requirement until its safety and scope review is complete. + +== Required report + +[source,yaml] +---- +repository: hyperpolymath/example +revision: "commit or tag" +status: PROVEN | PARTIALLY PROVEN | NOT PROVEN | NOT APPLICABLE +claim: "one precise claim" +formal_objects: + - "definitions or types" +proof_or_test_evidence: + - file: "path" + theorem_or_test: "name" + command: "command, if applicable" +assumptions: + - "checker soundness" + - "fault/timing/physical model" +limits: + - "what is not established" +robodog_relevance: direct | indirect | speculative | none +robodog_integration_proposal: + - "concrete type, invariant, test, or experiment" +robodog_hand_off: "short summary" +verification: + checked_by: "name or handle" + checked_on: "YYYY-MM-DD" + result: pending | accepted | rejected | needs clarification + robodog_issue: "link or identifier" +---- + +== Current intake queue + +No external research result has yet been accepted into the Robodog safety case. The visual comparator in link:bft-type-comparator.adoc[bft-type-comparator.adoc] is explanatory material, not evidence of a BFT or type-theoretic theorem. + +== Standing distinctions + +* BFT agreement is not physical truth. +* Authentication is not correctness. +* A proof term proves only its declared proposition under its assumptions. +* An information residue does not recover information never received. +* A choreography constrains protocol shape; it does not make a runtime honest. +* A resource bound is not a safety proof. +* Inverse metadata is not unconditional reversibility. +* Rejection with no actuator effect is not necessarily total observational nullity. diff --git a/docs/mathematical-agenda.adoc b/docs/mathematical-agenda.adoc new file mode 100644 index 0000000..38bfb16 --- /dev/null +++ b/docs/mathematical-agenda.adoc @@ -0,0 +1,40 @@ += Mathematical Agenda + +== Highest-value proof ladder + +=== 1. Evidence refinement + +Define `e₁ ⊑ e₂` when `e₂` is at least as informative as `e₁`. Prove that valid refinement cannot introduce unsupported certainty. This is the common spine for epistemic, residual, and safety-state work. + +=== 2. Compatible worlds + +Represent an observation by the set of system worlds compatible with it. Prove monotonicity under genuine evidence refinement and exhibit a two-world counterexample where telemetry does not justify a unique action. + +=== 3. Agreement versus truth + +Keep separate predicates for `AgreesOn(replicas, digest)` and `TrueInWorld(world, claim)`. Document the additional sensor, environment, and model assumptions required to connect them. + +=== 4. Typed safety gate + +Make actuator admission depend on explicit evidence predicates, not a single trust flag. Test every transition with stale, degraded, conflicting, forged, and missing evidence. + +=== 5. Quantitative bounds + +Add latency, rounds, trust crossings, evidence-check cost, and recovery cost as separate grades. Prove composition and budget failure without treating a grade as a safety theorem. + +=== 6. Null-effect and trace properties + +For rejected or quarantined inputs, prove no protected actuator-state change, then enumerate allowed audit, timing, queue, cache, and metrics traces. This is a realistic route into noninterference. + +== Why this order + +The first four steps clarify semantics and safety before introducing more machinery. They are small enough to produce counterexamples quickly and strong enough to expose whether later Echo, tropical, choreography, residual-evidence, or epistemic claims genuinely apply. + +== Minimum artefacts per step + +* one definition; +* one positive theorem or explicit counterexample; +* one executable test; +* one named assumption; +* one statement of what remains unproved; +* one Robodog integration note. diff --git a/docs/programme-plan.adoc b/docs/programme-plan.adoc new file mode 100644 index 0000000..62ace24 --- /dev/null +++ b/docs/programme-plan.adoc @@ -0,0 +1,69 @@ += Robodog Defensive Systems Lab: Programme Plan +:toc: + +== Mission + +Build a simulation-first, defensible safety case for resilient autonomous coordination. The project should make unsafe state transitions difficult to express, easy to reject, and auditable after the fact. It is not an operational ECM, surveillance, weapons, or field-deployment programme. + +== Programme questions + +. Can a component distinguish observation, inference, agreement, and physical truth? +. Can degraded or conflicting telemetry cross a safety boundary without being silently upgraded? +. Can safe-state decisions be checked across Rust, Idris2, SPARK, and FFI boundaries? +. Can every claimed guarantee state its model, assumptions, evidence, and limits? +. Can resource, latency, provenance, and recovery budgets fail loudly and locally? + +== Workstreams + +[cols="1,2,2,2",options="header"] +|=== +| Workstream | Near-term deliverable | Mathematical question | Primary evidence + +| Safety state | Explicit evidence-state algebra and gate | Is admission monotone in valid evidence? | Rust tests + SPARK proof obligations +| Proof boundary | Claim meanings, receipts, and transport records | What proposition is actually proved? | Idris2 types + checked examples +| Residual evidence | Compatible-world model for ambiguous telemetry | Does added evidence reduce alternatives? | finite model + Agda hand-off +| Information residue | Degradation/truncation witness | What loss is known, and what is unrecoverable? | Echo-style finite examples +| Agreement | Small 3f+1 trace model | Do replicas agree under the declared fault model? | executable fault traces +| Resource grades | Latency/round/boundary budget | Are worst-case bounds compositional? | benchmark + formal grade +| Recovery | Evidence-backed rollback and audit states | What is required for reversal? | property tests and crash cases +| Noninterference | Rejected/quarantined path | What state and trace effects remain? | SPARK/Absolute-Zero style model +|=== + +== Phase gates + +=== Gate 0: vocabulary and threat model + +Define crash, omission, equivocation, stale input, malicious input, compromised runtime, unsafe FFI, and physical-model error. No security claim may proceed without naming its fault model. + +=== Gate 1: executable baseline + +Implement explicit states: `Measured`, `Inferred`, `Verified`, `Stale`, `Degraded`, `Conflicting`, `Rejected`, and `UnknownProvenance`. Add positive, negative, and fault-injection tests. + +=== Gate 2: one cross-language invariant + +Select and state one invariant: + +[source] +---- +unsafe actuator command => no valid evidence path exists +---- + +Map the invariant across Rust, Idris2, SPARK, and the FFI. Record which layer proves which part. + +=== Gate 3: mathematical extensions + +Only after Gate 2, add residual-world ordering, Echo residues, tropical grades, choreography, reversibility, or non-disclosure. Each extension needs definitions, a theorem or counterexample, an executable test, and a Robodog adapter note. + +=== Gate 4: integrated safety case + +Produce a traceable argument from input to decision to safe-state outcome, including degraded communication, contradictory evidence, timeout, crash, and recovery. + +== Definition of done for a research claim + +A claim is `PROVEN` only when a formal checker or complete stated argument establishes it under named assumptions. `PARTIALLY PROVEN` means some lemmas or cases are established. `NOT PROVEN` is a valid result when a counterexample or missing assumption is identified. “Implemented”, “tested”, and “plausible” are not synonyms for proven. + +Every imported result must be recorded in link:incoming-reports.adoc[incoming-reports.adoc]. + +== Safety and publication boundary + +All experiments remain synthetic, defensive, and non-operational. No real RF captures, field deployment guidance, target tracking, intrusion, jamming, or offensive autonomy should be added. See link:../DEFENSIVE-USE.adoc[DEFENSIVE-USE.adoc] and link:../EXPORT-CONTROL.adoc[EXPORT-CONTROL.adoc]. diff --git a/www/index.html b/www/index.html new file mode 100644 index 0000000..8aa225d --- /dev/null +++ b/www/index.html @@ -0,0 +1,28 @@ + + + + +Robodog · BFT / Type-augmented comparator + + +
+
Robodog defensive systems lab · explanatory prototype
+

Agreement is not the same as knowledge.

+

A side-by-side map of classical Byzantine Fault Tolerance and a type-augmented design. Toggle stages, failure overlays, and claims. This is a teaching comparator—not a claim that dependent types replace a network protocol.

+
+
+

Classical BFT

runtime protocolquorumpartial synchrony
A
honest
→
X
faulty
→
B
honest

1 · Propose

A value is broadcast. X may equivocate, omit, or lie.

2 · Vote / prepare

Replicas exchange protocol messages and collect votes. Safety depends on quorum intersection and the fault model.

3 · Commit

With a valid quorum, replicas decide. Liveness may wait for synchrony; BFT does not prove the value is true.

Guarantee: agreement (under stated assumptions). Not guaranteed: factual correctness of an authenticated sender’s claim.

+

Type-augmented path

static + runtime evidenceproof-carrying datalocal rejection
A
claim
→
Γ
checker
→
B
consumer

1 · Construct

A value travels with an evidence object, e.g. Verified origin timestamp; a type can require the witness.

2 · Check

The boundary validates the evidence and its scope. An attacker can still send a signed lie unless the predicate captures the relevant truth.

3 · Admit or reject

Invalid evidence is rejected locally—or retained as an explicit Unverified / Echo value. This complements, rather than magically replaces, consensus.

Guarantee: no unchecked claim crosses a typed boundary (if the implementation and specification are sound). Not guaranteed: that the sensor or predicate is truthful.

+
+
What the red overlay means: A faulty sender can equivocate. BFT contains this through quorum rules; types reject only what their predicates can detect. Authentication proves who spoke, not that they spoke truth.
+

Claim audit

Informal proposalAccurate readingVerdict
“ProofTransport replaces BFT.”Proof-carrying interfaces constrain admissible states. They do not solve agreement, membership, equivocation, timing, or recovery.Complement
“A factive proof term makes a message true.”Only if the proof checker, predicate, axioms, data source, and refinement model are sound. A proof of “sensor reported X” is not a proof that X is physically true.Overclaim
“Echo types retain packet loss exactly.”A typed loss witness can preserve structured provenance/shape of an observed transformation. It cannot recover information that was never received.Useful, bounded
“Choreography makes deviation impossible.”Projection can rule out protocol-shape deviations in a verified endpoint; crashes, compromised runtimes, unsafe FFI, and hostile peers still need containment.Conditional
+

Where this repo fits

This checkout is a Robodog ECM/safety lab with Idris ABI declarations, Rust implementation/tests, and SPARK safety modules. The strongest immediate connection is evidence at safety boundaries: make detection, formation, and autonomy outputs distinguish measured, inferred, stale, degraded, and rejected.

Idris2 model evidence/indexed states and protocol shape. Rust enforce explicit enums and rejection paths. SPARK prove safety properties of the boundary—not physical truth.

Next experiments

  1. Write a small threat model: crash, omission, equivocation, stale sensor, malicious sensor.
  2. Define one end-to-end invariant: unsafe actuator command ⇒ no valid evidence path.
  3. Model a 3f+1 quorum trace beside the typed trace; inject counterexamples.
  4. Measure cost: latency, memory, proof/check overhead, false rejection.
  5. Only then connect Echo, epistemic, tropical, choreography, residual evidence, Januskey, or Absolute Zero as named modules with operational semantics and tests.
+

Reading guide: BFT answers “can non-faulty replicas agree despite faults?” Typed evidence answers “what states may this component accept, and why?” Those are orthogonal questions. Keep the distinction visible.

+