66
77#### A kernel-level finite-state machine with formally bounded withdrawal latency.
88
9- <!-- ─── CI / Build ──────────────────────────────────────────────────── -->
10-
119[ ![ CI] ( https://github.com/AxonOS-org/axonos-consent/actions/workflows/ci.yml/badge.svg?branch=main )] ( https://github.com/AxonOS-org/axonos-consent/actions/workflows/ci.yml )
12- [ ![ Format] ( https://img.shields.io/badge/rustfmt-clean-success?logo=rust )] ( https://github.com/AxonOS-org/axonos-consent/actions/workflows/ci.yml )
13- [ ![ Clippy] ( https://img.shields.io/badge/clippy-passing-success?logo=rust )] ( https://github.com/AxonOS-org/axonos-consent/actions/workflows/ci.yml )
14- [ ![ no_std] ( https://img.shields.io/badge/no__std-thumbv7em--none--eabihf-blueviolet?logo=rust )] ( https://github.com/AxonOS-org/axonos-consent/actions/workflows/ci.yml )
15-
16- <!-- ─── Crate / Docs ────────────────────────────────────────────────── -->
17-
18- [ ![ Crate] ( https://img.shields.io/badge/crate-v0.3.0-orange?logo=rust )] ( ./Cargo.toml )
19- [ ![ Docs] ( https://img.shields.io/badge/docs-rustdoc-blue?logo=docsdotrs )] ( https://docs.rs/axonos-consent )
20- [ ![ Spec] ( https://img.shields.io/badge/spec-v0.3.0-blue )] ( ./SPEC.md )
21- [ ![ MSRV] ( https://img.shields.io/badge/rustc-1.75%2B-lightgrey?logo=rust )] ( ./Cargo.toml )
22-
23- <!-- ─── Quality / Safety ────────────────────────────────────────────── -->
10+ [ ![ Crate] ( https://img.shields.io/badge/Crate-v0.5.0-0a4a8f?style=flat-square )] ( https://github.com/AxonOS-org/axonos-consent/releases/tag/v0.5.0 )
11+ [ ![ Spec] ( https://img.shields.io/badge/Spec-v0.5.0-0a4a8f?style=flat-square )] ( ./SPEC.md )
12+ [ ![ Standard] ( https://img.shields.io/badge/Standard-v1.0.0-0a4a8f?style=flat-square )] ( https://github.com/AxonOS-org/axonos-standard )
13+ [ ![ Rust] ( https://img.shields.io/badge/Rust-no__std-CE422B?style=flat-square&logo=rust&logoColor=white )] ( https://www.rust-lang.org/ )
2414
25- [ ![ Unsafe forbidden ] ( https://img.shields.io/badge/unsafe-forbidden-success?logo=rust )] ( ./src/lib.rs )
26- [ ![ Verified: Kani BMC ] ( https://img.shields.io/badge/verified-Kani%20BMC-success )] ( ./kani/ )
27- [ ![ Allocations ] ( https://img.shields.io/badge/critical %20path-0%20alloc-success )] ( ./SPEC.md#4-timing-bounds )
28- [ ![ WCRT] ( https://img.shields.io/badge/WCRT-%E2%89%A4%201648%20cycles-success )] ( ./SPEC.md#4-timing-bounds )
15+ [ ![ Verified ] ( https://img.shields.io/badge/Verified-Kani%20BMC%20%C3%975-0d7a5f?style=flat-square )] ( ./kani/ )
16+ [ ![ Unsafe ] ( https://img.shields.io/badge/Unsafe-forbidden-0d7a5f?style=flat-square )] ( ./src/lib.rs )
17+ [ ![ Critical path ] ( https://img.shields.io/badge/Critical %20path-0%20alloc-0d7a5f?style=flat-square )] ( ./SPEC.md#4-timing-bounds )
18+ [ ![ WCRT] ( https://img.shields.io/badge/WCRT-%E2%89%A4%201648%20cycles-0d7a5f?style=flat-square )] ( ./SPEC.md#4-timing-bounds )
2919
30- <!-- ─── License ─────────────────────────────────────────────────────── -->
31-
32- [ ![ License: Apache-2.0 OR MIT (code)] ( https://img.shields.io/badge/license--code-Apache--2.0%20OR%20MIT-blue.svg )] ( ./LICENSE )
33- [ ![ License: CC-BY-SA-4.0 (spec)] ( https://img.shields.io/badge/license--spec-CC--BY--SA--4.0-lightgrey.svg )] ( ./LICENSE-CC-BY-SA )
34- [ ![ License: CC0-1.0 (vectors)] ( https://img.shields.io/badge/license--vectors-CC0--1.0-lightgrey.svg )] ( ./vectors/LICENSE )
20+ [ ![ License (code)] ( https://img.shields.io/badge/License%20code-Apache--2.0%20OR%20MIT-475569?style=flat-square )] ( ./LICENSE )
21+ [ ![ License (spec)] ( https://img.shields.io/badge/License%20spec-CC--BY--SA--4.0-475569?style=flat-square )] ( ./LICENSE-CC-BY-SA )
22+ [ ![ MSRV] ( https://img.shields.io/badge/MSRV-1.75-475569?style=flat-square )] ( ./Cargo.toml )
3523
3624---
3725
@@ -90,7 +78,7 @@ This is a **standalone subsystem of the AxonOS Project**. No external co-authors
9078| Critical-path allocations | 0 | static analysis |
9179| Source lines (` src/ ` ) | 594 | — |
9280| Unsafe blocks | 0 | ` #![forbid(unsafe_code)] ` |
93- | Kani harnesses | 4 | passing at v0.3 .0 |
81+ | Kani harnesses | 5 | passing at v0.5 .0 |
9482
9583All measurements remain within the L1 bound. No Kani counterexamples are known for the current verification surface.
9684
@@ -121,7 +109,7 @@ A red X on any job blocks the merge. The aggregate `CI` job is what the branch-p
121109axonos-consent/
122110├── SPEC.md ← canonical specification (this is the source of truth)
123111├── README.md ← this file
124- ├── CHANGELOG.md ← version history; v0.4 .0 is the current verification release
112+ ├── CHANGELOG.md ← version history; v0.5 .0 is the current release
125113├── Cargo.toml ← crate manifest; MSRV 1.75
126114├── LICENSE ← Apache-2.0 OR MIT dispatcher for code
127115├── LICENSE-APACHE ← Apache-2.0 full text
@@ -130,19 +118,21 @@ axonos-consent/
130118├── rustfmt.toml ← formatting configuration
131119├── rust-toolchain.toml ← pins stable + rustfmt + clippy + thumbv7em
132120│
133- ├── src/ ← reference Rust implementation (#![no_std], 594 LOC )
121+ ├── src/ ← reference Rust implementation (#![no_std])
134122│ ├── lib.rs ← crate root, exports, doctest
135123│ ├── state.rs ← consent FSM with AtomicU8
136124│ ├── wire.rs ← 16-byte little-endian wire format
137125│ ├── crypto.rs ← constant-time signature verification
138126│ ├── error.rs ← typed error taxonomy
139- │ └── interlock.rs ← ObservationGate trait for kernel IPC integration
127+ │ ├── interlock.rs ← ObservationGate trait for kernel IPC integration
128+ │ └── dual_control.rs ← multi-party (guardian) co-authorisation (v0.5.0)
140129│
141130├── kani/ ← Bounded-model-checking harnesses (L1 evidence)
142131│ ├── handle_withdraw_terminates.rs
143132│ ├── fsm_no_invalid_transitions.rs
144133│ ├── cbor_decoder_bounded.rs
145- │ └── signature_verification_constant_time.rs
134+ │ ├── signature_verification_constant_time.rs
135+ │ └── co_authorisation_requires_two_parties.rs
146136│
147137├── tests/ ← unit + integration + property tests
148138│ ├── integration.rs ← full FSM lifecycle
@@ -152,7 +142,8 @@ axonos-consent/
152142│ └── withdrawal_latency.rs
153143│
154144├── examples/ ← worked usage examples
155- │ └── basic_usage.rs ← (requires the `std` feature)
145+ │ ├── basic_usage.rs ← (requires the `std` feature)
146+ │ └── dual_control.rs ← guardian co-authorisation walkthrough
156147│
157148├── vectors/ ← conformance test vectors (CC0-1.0; public domain)
158149│ ├── README.md
@@ -206,7 +197,7 @@ A worked example covering the full FSM lifecycle is in [`examples/basic_usage.rs
206197cargo install --locked kani-verifier
207198cargo kani setup
208199
209- # Run all four harnesses
200+ # Run all five harnesses
210201cargo kani --harness handle_withdraw_terminates
211202cargo kani --harness fsm_no_invalid_transitions
212203cargo kani --harness cbor_decoder_bounded
@@ -265,7 +256,42 @@ For implementations in languages other than Rust, the vectors are exported in ca
265256
266257A v1.0.0 crate release will accompany the second independent implementation. Until then, the crate remains ` 0.y.z ` to reflect that the implementation surface is not yet locked.
267258
268- The ** specification protocol** is stable as of v0.3.0 and unchanged in v0.4.0; the v0.4.0 bump records added validation evidence (SPEC §10.3), not a protocol change. The * crate* may iterate at the patch level for bug fixes and ergonomic improvements without modifying the protocol.
259+ The single-party ** specification protocol** is stable as of v0.3.0 and unchanged through v0.5.0. v0.4.0 recorded added validation evidence (SPEC §10.3); v0.5.0 adds the optional multi-party (guardian) co-authorisation profile (SPEC §12) without altering the single-party baseline. An implementation conformant with the v0.4.0 protocol is conformant with the v0.5.0 baseline profile without modification.
260+
261+ ---
262+
263+ ## Multi-party (guardian) co-authorisation (v0.5.0)
264+
265+ For clinical deployments — the ALS rehabilitation pilot in the canonical
266+ Standard's roadmap is the motivating case — a guardian can co-authorise consent
267+ changes together with the patient. This is the optional [ ` dual_control ` ] ( ./src/dual_control.rs )
268+ layer, specified normatively in [ SPEC §12] ( ./SPEC.md#12-multi-party-guardian-co-authorisation ) .
269+
270+ It follows the ** safe-direction principle** :
271+
272+ - ** Either party** may reduce neural-data exposure (` Suspended ` , ` Withdrawn ` )
273+ ** unilaterally** . The flow can always be stopped by one signature.
274+ - ** Resuming** the flow (` Suspended → Granted ` ) requires ** both** parties to
275+ authorise the same transition within a bounded window. No sequence of
276+ signatures from one party can resume it — a property proven by the Kani
277+ harness ` co_authorisation_requires_two_parties ` .
278+
279+ The single-party ` ConsentMachine ` is unchanged; multi-party is opt-in by using
280+ ` DualControlMachine ` instead. See [ ` examples/dual_control.rs ` ] ( ./examples/dual_control.rs ) .
281+
282+ ---
283+
284+ ## Position in the AxonOS stack
285+
286+ | Layer | Repository | Role |
287+ | ---| ---| ---|
288+ | Canonical standard | [ ` axonos-standard ` ] ( https://github.com/AxonOS-org/axonos-standard ) | Architecture manual, conformance criteria, validation taxonomy |
289+ | Engineering RFCs | [ ` axonos-rfcs ` ] ( https://github.com/AxonOS-org/axonos-rfcs ) | Numbered design proposals; normative once finalised |
290+ | Kernel substrate | [ ` axonos-kernel ` ] ( https://github.com/AxonOS-org/axonos-kernel ) | EDF scheduling, SPSC IPC, capability gate, monotonic time |
291+ | Application boundary | [ ` axonos-sdk ` ] ( https://github.com/AxonOS-org/axonos-sdk ) | Typed intents, manifests, ABI-compatible integration |
292+ | ** Consent layer** | ** ` axonos-consent ` ** | Deterministic consent FSM + optional multi-party co-authorisation (this repository) |
293+ | Mesh coordination | [ ` axonos-swarm ` ] ( https://github.com/AxonOS-org/axonos-swarm ) | Distributed timing, co-availability, peer health monitoring |
294+ | Acquisition gateway | [ ` axon-bci-gateway ` ] ( https://github.com/AxonOS-org/axon-bci-gateway ) | OpenBCI GUI integration fork for EEG input |
269295
270296---
271297
@@ -277,7 +303,7 @@ This repository is authored solely by **Denis Yermakou** — AxonOS Project, Sin
277303- Reference implementation: same author, same project.
278304- No external co-authors. No external coupling-protocol dependencies.
279305
280- Inquiries: [ info @axonos.org] ( mailto:info @axonos.org ) · Security: [ security@axonos.org ] ( mailto:security@axonos.org ) .
306+ Inquiries: [ connect @axonos.org] ( mailto:connect @axonos.org ) · Security: [ security@axonos.org ] ( mailto:security@axonos.org ) .
281307
282308---
283309
@@ -295,7 +321,7 @@ The test vectors are CC0 specifically so any independent implementation — in a
295321
296322<div align =" center " >
297323
298- ** axonos-consent · v0.4 .0 · verification release **
324+ ** axonos-consent · v0.5 .0 · multi-party co-authorisation **
299325
300326Singapore · Zurich · Berlin · Milano · San Mateo
301327
0 commit comments