Skip to content

Commit 8dd32d7

Browse files
hyperpolymathclaude
andcommitted
chore(floor-raise): add integration files (Phase 2)
Add proven, verisimdb, feedback-o-tron, and vexometer integration manifests as part of Floor Raise campaign Phase 2. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
1 parent 9db6e32 commit 8dd32d7

8 files changed

Lines changed: 1416 additions & 367 deletions

File tree

README.adoc

Lines changed: 216 additions & 23 deletions
Original file line numberDiff line numberDiff line change
@@ -1,45 +1,238 @@
11
// SPDX-License-Identifier: PMPL-1.0-or-later
22
// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
3-
= A2mliser
3+
= a2mliser — Cryptographic Attestation for Any Markup or Configuration
44
Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
55
:toc: left
6+
:toclevels: 3
67
:icons: font
8+
:source-highlighter: rouge
79

8-
== What Is This?
10+
== What Is a2mliser?
911

10-
A2MLiser adds **cryptographic attestation and verification** to any markup,
11-
configuration, or manifest file — proving authenticity and integrity.
12+
a2mliser wraps any markup, configuration, or manifest file in an
13+
**A2ML (Attestable Markup Language) envelope** — adding cryptographic signatures,
14+
provenance chains, and tamper detection without altering the original content.
1215

13-
A2ML (Attested Markup Language) embeds attestation chains in documents.
14-
A2MLiser wraps existing files in A2ML attestation envelopes.
16+
Where most signing tools operate on opaque blobs, a2mliser understands
17+
structure. It parses TOML, YAML, JSON, XML, and INI files, then generates
18+
attestation wrappers that cover both the content and its schema. A consumer can
19+
verify not only that a file has not been tampered with, but that its structure
20+
conforms to the attested schema at the moment of signing.
1521

16-
== How It Works
22+
a2mliser is part of the
23+
https://github.com/hyperpolymath/iseriser[-iser acceleration family] — tools
24+
that wrap existing code in a target language's capabilities via manifest-driven
25+
code generation.
1726

18-
Configure attestation in `a2mliser.toml`. A2MLiser:
27+
== Key Value Proposition
1928

20-
1. Analyses existing markup files (YAML, TOML, JSON, XML, Markdown)
21-
2. Generates A2ML attestation envelopes with cryptographic signatures
22-
3. Embeds provenance metadata (who created, when, from what source)
23-
4. Provides verification: any consumer can check authenticity
24-
5. Supports attestation chains (A attests B attests C)
29+
* **Any file can be attested** — configs, manifests, CI definitions, lock files,
30+
even other A2ML documents.
31+
* **Cryptographic proof** of authenticity and integrity (SHA-256, BLAKE3).
32+
* **Provenance chains** — trace any artifact back through its chain of custody.
33+
A attests B attests C, forming a directed acyclic graph of trust.
34+
* **Structure-aware signing** — unlike GPG detached signatures, a2mliser
35+
understands the file format and signs individual fields or sections.
36+
* **Supply chain security** — verify that CI configs, dependency manifests, and
37+
deployment descriptors have not been altered since the authorised signer
38+
produced them.
39+
* **Format-preserving** — the original file remains readable; attestation
40+
metadata is carried in a sidecar `.a2ml` envelope or embedded as comments.
2541

26-
== Key Value
42+
== Architecture
2743

28-
* **Any file can be attested** — not just code, any artifact
29-
* **Cryptographic proof** of authenticity and integrity
30-
* **Provenance chains** — trace any artifact back to its origin
31-
* **Supply chain security** — verify configs haven't been tampered with
44+
a2mliser follows the hyperpolymath ABI-FFI-codegen architecture:
3245

33-
== Architecture
46+
[source]
47+
----
48+
a2mliser.toml (user manifest)
49+
|
50+
v
51+
+------------------------+
52+
| Manifest Parser (Rust) | <-- reads user intent
53+
+------------------------+
54+
|
55+
+-------------+-------------+
56+
| |
57+
v v
58+
+---------------------+ +-----------------------+
59+
| Idris2 ABI Proofs | | Format Handlers |
60+
| (signature correct- | | (TOML, YAML, JSON, |
61+
| ness, non-repudia- | | XML, INI parsers) |
62+
| tion, chain valid- | +-----------------------+
63+
| ity) | |
64+
+---------------------+ v
65+
| +-----------------------+
66+
v | Attestation Engine |
67+
+---------------------+ | (hash, sign, embed) |
68+
| Zig FFI Bridge | +-----------------------+
69+
| (crypto primitives: | |
70+
| BLAKE3, Ed25519, | v
71+
| SHA-256) | +-----------------------+
72+
+---------------------+ | Codegen (A2ML wrapper |
73+
| | generation) |
74+
v +-----------------------+
75+
+---------------------+ |
76+
| C Headers (generated| v
77+
| from ABI) | attested output files
78+
+---------------------+ (.a2ml envelopes)
79+
----
80+
81+
=== Layer Responsibilities
82+
83+
Manifest Parser (Rust)::
84+
Reads `a2mliser.toml`, validates user intent, dispatches to format handlers
85+
and the attestation engine.
86+
87+
Idris2 ABI (`src/interface/abi/`)::
88+
Formally proves that signature operations are correct: signing a document and
89+
verifying the same document always agree; provenance chains form a valid DAG;
90+
attestation envelopes are non-repudiable.
91+
92+
Zig FFI (`src/interface/ffi/`)::
93+
Implements the actual cryptographic primitives (BLAKE3 hashing, Ed25519
94+
signing, SHA-256 digests) as a C-compatible shared library. Zero runtime
95+
overhead from the proof layer — Idris2 proofs are erased at compile time.
96+
97+
Format Handlers (`src/codegen/`)::
98+
Parse each supported format while preserving structure, identify attestable
99+
regions, and generate the A2ML envelope that wraps the original content.
100+
101+
== Supported Formats
102+
103+
[cols="1,3"]
104+
|===
105+
| Format | Notes
106+
107+
| TOML
108+
| Full structural attestation. Individual tables and key-value pairs can be
109+
signed independently.
110+
111+
| YAML
112+
| Document and sub-document attestation. Anchors and aliases are resolved
113+
before signing.
114+
115+
| JSON
116+
| Object-level and array-level attestation. JSON Schema can be co-attested.
117+
118+
| XML
119+
| Element-level signing with XPath selectors. Namespace-aware.
120+
121+
| INI
122+
| Section-level attestation. Comments are preserved but excluded from
123+
signatures by default.
124+
125+
| Custom
126+
| Plugin system (Phase 3+) for arbitrary formats via a trait-based handler
127+
interface.
128+
|===
129+
130+
== CLI Commands
131+
132+
[source,bash]
133+
----
134+
# Create a new a2mliser.toml in the current directory
135+
a2mliser init
136+
137+
# Validate an existing manifest
138+
a2mliser validate --manifest a2mliser.toml
139+
140+
# Generate A2ML attestation envelopes for all declared files
141+
a2mliser generate --manifest a2mliser.toml --output attested/
142+
143+
# Build the generated artifacts (compile Zig FFI, link)
144+
a2mliser build --manifest a2mliser.toml [--release]
145+
146+
# Run the attestation workload end-to-end
147+
a2mliser run --manifest a2mliser.toml
34148
35-
Follows the hyperpolymath -iser pattern:
36-
manifest -> Idris2 ABI proof -> Zig FFI bridge -> target language codegen.
37-
Part of the https://github.com/hyperpolymath/iseriser[-iser family].
149+
# Show manifest information and attestation summary
150+
a2mliser info --manifest a2mliser.toml
151+
----
152+
153+
== Example Manifest
154+
155+
An `a2mliser.toml` that attests a Cargo.toml and a CI workflow:
156+
157+
[source,toml]
158+
----
159+
# a2mliser manifest — declare which files to attest
160+
[workload]
161+
name = "my-project-attestation"
162+
entry = "Cargo.toml"
163+
strategy = "structure-aware"
164+
165+
[data]
166+
input-type = "toml"
167+
output-type = "a2ml-envelope"
168+
169+
[options]
170+
flags = ["sign-sections", "provenance-chain"]
171+
172+
# Files to attest
173+
[[targets]]
174+
path = "Cargo.toml"
175+
format = "toml"
176+
granularity = "table" # sign each [section] independently
177+
178+
[[targets]]
179+
path = ".github/workflows/ci.yml"
180+
format = "yaml"
181+
granularity = "document" # sign the entire document
182+
183+
[signing]
184+
algorithm = "ed25519"
185+
hash = "blake3"
186+
key-source = "env:A2ML_SIGNING_KEY" # or "file:keys/signing.pem"
187+
----
188+
189+
== Integration With Other -isers
190+
191+
k9iser::
192+
Contract validation. k9iser validates that configuration files satisfy K9
193+
contracts; a2mliser then attests the validated result, proving that the file
194+
both conforms to its contract and has not been modified since validation.
195+
196+
typedqliser::
197+
Query attestation. When typedqliser generates type-safe query wrappers,
198+
a2mliser can attest the generated code, proving it was produced by a specific
199+
version of typedqliser from a specific schema.
200+
201+
verisimiser::
202+
Database augmentation. Attestation records (who signed what, when) can be
203+
stored in VeriSimDB octads via verisimiser, providing a tamper-evident
204+
audit trail.
205+
206+
== Build and Test
207+
208+
[source,bash]
209+
----
210+
# Build
211+
cargo build --release
212+
213+
# Test
214+
cargo test
215+
216+
# Full quality check (format, lint, test)
217+
just quality
218+
219+
# Pre-commit scan
220+
just assail
221+
----
38222

39223
== Status
40224

41-
**Pre-alpha.** Architecture defined, scaffolding in place, codegen pending.
225+
**Pre-alpha (Phase 0 complete).**
226+
227+
The CLI skeleton, manifest parser, and ABI/FFI scaffolding are in place.
228+
Codegen stubs exist but do not yet produce real attestation envelopes.
229+
230+
See link:ROADMAP.adoc[ROADMAP.adoc] for the full development plan.
231+
232+
See link:TOPOLOGY.md[TOPOLOGY.md] for the repository structure map.
42233

43234
== License
44235

45236
SPDX-License-Identifier: PMPL-1.0-or-later
237+
238+
Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath)

ROADMAP.adoc

Lines changed: 87 additions & 27 deletions
Original file line numberDiff line numberDiff line change
@@ -1,32 +1,92 @@
11
// SPDX-License-Identifier: PMPL-1.0-or-later
2+
// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
23
= a2mliser Roadmap
3-
:toc:
4+
:toc: left
45
:icons: font
56

6-
== Phase 0: Scaffold (COMPLETE)
7-
* [x] RSR template with full CI/CD
8-
* [x] CLI with subcommands
9-
* [x] Manifest parser
10-
* [x] Codegen stubs
11-
* [x] ABI module stubs
12-
* [x] README with architecture
13-
14-
== Phase 1: Core Implementation
15-
* [ ] Implement target-language-specific code generation
16-
* [ ] Write Idris2 ABI proofs for core invariants
17-
* [ ] Build Zig FFI bridge
18-
* [ ] First working end-to-end example
19-
* [ ] Integration tests
20-
21-
== Phase 2: Polish
22-
* [ ] Error messages and diagnostics
7+
== Phase 0: Scaffold [COMPLETE]
8+
9+
* [x] RSR template with 17 CI/CD workflows
10+
* [x] Rust CLI with `init`, `validate`, `generate`, `build`, `run`, `info` subcommands
11+
* [x] Manifest parser (`a2mliser.toml` — TOML-based workload description)
12+
* [x] Codegen module stubs
13+
* [x] ABI module stubs (Rust side)
14+
* [x] Idris2 ABI type definitions (Types.idr, Layout.idr, Foreign.idr) — template placeholders
15+
* [x] Zig FFI scaffold (build.zig, main.zig, integration tests)
16+
* [x] README with architecture overview
17+
* [x] Machine-readable state files (STATE.a2ml, META.a2ml, ECOSYSTEM.a2ml)
18+
* [x] Contractile system (K9, Must, Trust, Dust, Lust)
19+
* [x] Bot directives for gitbot-fleet
20+
21+
== Phase 1: Core Attestation Engine
22+
23+
The minimum viable attestation pipeline: hash a file, sign the hash, embed
24+
the signature in an A2ML envelope.
25+
26+
* [ ] Implement SHA-256 and BLAKE3 digest computation in Zig FFI
27+
* [ ] Implement Ed25519 signing and verification in Zig FFI
28+
* [ ] Define `AttestationEnvelope` structure (hash algorithm, signature bytes,
29+
signer identity, timestamp, target file path, target file digest)
30+
* [ ] Wire Rust CLI `generate` command to call Zig FFI via C headers
31+
* [ ] Produce `.a2ml` sidecar files containing the attestation envelope
32+
* [ ] Implement `validate` command: read `.a2ml` envelope, recompute digest,
33+
verify signature
34+
* [ ] First end-to-end test: attest a TOML file, verify the attestation
35+
* [ ] Replace Idris2 ABI template placeholders with attestation-specific types
36+
37+
== Phase 2: Format Handlers
38+
39+
Structure-aware parsing so that attestation can target individual sections
40+
of a document rather than treating it as an opaque blob.
41+
42+
* [ ] TOML handler: parse into tables, attest individual `[section]` blocks
43+
* [ ] YAML handler: parse documents, resolve anchors/aliases before signing
44+
* [ ] JSON handler: object-level and array-level attestation
45+
* [ ] XML handler: element-level signing with XPath selectors
46+
* [ ] INI handler: section-level attestation, comment preservation
47+
* [ ] Granularity control in `a2mliser.toml`: `document`, `section`, `field`
48+
* [ ] Envelope embedding modes: sidecar (`.a2ml` file) vs inline (comments)
49+
* [ ] Schema co-attestation: sign both the data and its expected schema
50+
51+
== Phase 3: Provenance Chains
52+
53+
Chain-of-custody tracking — an attestation can reference a previous
54+
attestation, forming a directed acyclic graph of trust.
55+
56+
* [ ] `ProvenanceChain` data structure: ordered list of attestation records
57+
* [ ] Parent reference: each envelope can cite the hash of its predecessor
58+
* [ ] Timestamp authority integration (RFC 3161 or custom TSA)
59+
* [ ] Chain validation: verify the full chain from leaf to root
60+
* [ ] Merge detection: identify when two chains diverge and re-converge
61+
* [ ] Export: provenance chain as Graphviz DOT for visualisation
62+
* [ ] Key rotation: support multiple signing keys with validity periods
63+
64+
== Phase 4: Idris2 Formal Proofs
65+
66+
Replace the template ABI with attestation-specific formal verification.
67+
68+
* [ ] `SignatureAlgorithm` type with exhaustive case coverage
69+
* [ ] Proof: `sign(key, data) |> verify(pubkey, data)` always succeeds for
70+
matching key pairs
71+
* [ ] Proof: provenance chains form a valid DAG (no cycles)
72+
* [ ] Proof: attestation envelopes are non-repudiable (signature binds signer
73+
identity to content)
74+
* [ ] Proof: hash collision resistance properties (type-level bounds)
75+
* [ ] Memory layout proofs for all FFI-crossing structs
76+
* [ ] Platform-specific ABI compliance verification (Linux, macOS, Windows, WASM)
77+
78+
== Phase 5: Ecosystem Integration
79+
80+
Packaging, distribution, and integration with the broader hyperpolymath
81+
toolchain.
82+
83+
* [ ] BoJ-server cartridge: expose a2mliser as an MCP tool
84+
* [ ] PanLL panel: visual attestation status dashboard
85+
* [ ] CI/CD action: GitHub Action that runs `a2mliser validate` on PRs
86+
* [ ] VeriSimDB storage: persist attestation records in octad database
87+
* [ ] k9iser bridge: attest files after K9 contract validation passes
88+
* [ ] typedqliser bridge: attest generated query wrappers
89+
* [ ] Plugin system: trait-based handler interface for custom formats
90+
* [ ] crates.io publication
2391
* [ ] Shell completions (bash, zsh, fish)
24-
* [ ] CI/CD for the generated artifacts
25-
* [ ] Performance benchmarks
26-
* [ ] Additional examples
27-
28-
== Phase 3: Ecosystem
29-
* [ ] PanLL panel integration
30-
* [ ] BoJ-server cartridge
31-
* [ ] VeriSimDB backing store for results
32-
* [ ] Publish to crates.io
92+
* [ ] Performance benchmarks and optimisation pass

0 commit comments

Comments
 (0)