Skip to content

Commit 087eefe

Browse files
hyperpolymathclaude
hyperpolymath
and
claude
committed
docs: bespoke architecture, roadmap, topology, and ABI definitions for dafniser
Replace all template placeholders with dafniser-specific content: - README.adoc: Dafny verification pipeline (specs -> Z3 -> target compilation), use cases (crypto, consensus, financial, sorting), Dafny constructs - ROADMAP.adoc: Phase 0-6 (scaffold, spec parser, Dafny codegen, Z3 verification, multi-target compilation, Idris2 meta-proofs, ecosystem) - TOPOLOGY.md: module topology, data flow diagram, verification pipeline - Types.idr: Precondition, Postcondition, LoopInvariant, GhostVariable, Lemma, VerificationResult, DafnyTarget, FunctionSpec, SpecTree - Layout.idr: memory layouts for all Dafniser ABI types - Foreign.idr: FFI for spec loading, Dafny generation, Z3 verification, target compilation - main.zig: Dafniser FFI implementation with pipeline stubs - build.zig, integration_test.zig: dafniser-specific - 0-AI-MANIFEST.a2ml: dafniser description, invariants, structure - 6a2/*.a2ml: STATE, META, ECOSYSTEM, AGENTIC, NEUROSYM, PLAYBOOK — all bespoke Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
1 parent 04f4275 commit 087eefe

16 files changed

Lines changed: 1192 additions & 463 deletions

File tree

‎.machine_readable/6a2/AGENTIC.a2ml‎

Lines changed: 4 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,12 +1,12 @@
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>
33
#
4-
# AGENTIC.a2ml — AI agent constraints and capabilities
4+
# AGENTIC.a2ml — AI agent constraints and capabilities for dafniser
55
# Defines what AI agents can and cannot do in this repository.
66

77
[metadata]
88
version = "0.1.0"
9-
last-updated = "{{CURRENT_DATE}}"
9+
last-updated = "2026-03-21"
1010

1111
[agent-permissions]
1212
can-edit-source = true
@@ -22,6 +22,8 @@ can-create-files = true
2222
# - Never use banned languages (TypeScript, Python, Go, etc.)
2323
# - Never place state files in repository root (must be in .machine_readable/)
2424
# - Never use AGPL license (use PMPL-1.0-or-later)
25+
# - Never write Dafny by hand — dafniser generates all Dafny from TOML specs
26+
# - Never bypass Z3 verification — all generated Dafny must pass verification
2527

2628
[maintenance-integrity]
2729
fail-closed = true

‎.machine_readable/6a2/ECOSYSTEM.a2ml‎

Lines changed: 10 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -6,12 +6,13 @@
66
(version "0.1.0")
77
(name "dafniser")
88
(type "tool")
9-
(purpose "Generate correct-by-construction code using Dafny")
9+
(purpose "Generate correct-by-construction code for critical functions using Dafny verification and Z3 SMT solving — sorting, searching, crypto, consensus, financial algorithms")
1010

1111
(position-in-ecosystem
1212
(family "-iser acceleration frameworks")
1313
(meta-framework "iseriser")
1414
(relationship "sibling")
15+
(niche "Formal verification via Dafny/Z3 — proves code satisfies pre/postconditions, loop invariants, and termination")
1516
(top-3 ("typedqliser" "chapeliser" "verisimiser")))
1617

1718
(related-projects
@@ -32,7 +33,13 @@
3233
(description "Database recovery via constraint propagation"))
3334
(project "proven"
3435
(relationship "dependency")
35-
(description "Shared Idris2 verified library"))
36+
(description "Shared Idris2 verified library — dafniser may use proven lemmas"))
3637
(project "typell"
3738
(relationship "dependency")
38-
(description "Type theory engine"))))
39+
(description "Type theory engine — potential source of type-level spec validation"))
40+
(project "halideiser"
41+
(relationship "sibling")
42+
(description "Halide image processing acceleration — shares -iser architecture"))
43+
(project "futharkiser"
44+
(relationship "sibling")
45+
(description "Futhark GPU acceleration — shares -iser architecture"))))

‎.machine_readable/6a2/META.a2ml‎

Lines changed: 30 additions & 15 deletions
Original file line numberDiff line numberDiff line change
@@ -4,38 +4,53 @@
44

55
(meta
66
(version "0.1.0")
7-
(last-updated "2026-03-20")
7+
(last-updated "2026-03-21")
88

99
(architecture-decisions
1010
(adr "001-iser-pattern"
1111
(status "accepted")
12-
(context "Need to make powerful languages accessible without steep learning curves")
13-
(decision "Use manifest-driven code generation: user describes WHAT, tool generates HOW")
14-
(consequences "Users write zero target language code; all complexity in the -iser"))
12+
(context "Need to make Dafny verification accessible without requiring users to learn Dafny syntax")
13+
(decision "Use manifest-driven code generation: user describes WHAT (pre/postconditions), dafniser generates HOW (Dafny source with verification annotations)")
14+
(consequences "Users write zero Dafny; all complexity in the -iser; specs are TOML, not Dafny"))
1515

1616
(adr "002-abi-ffi-standard"
1717
(status "accepted")
18-
(context "Need verified interop between Rust CLI, target language, and user code")
19-
(decision "Idris2 ABI for formal proofs, Zig FFI for C-ABI bridge")
20-
(consequences "Compile-time correctness guarantees; zero runtime overhead from proofs"))
18+
(context "Need verified interop between Rust CLI, Dafny compiler, Z3, and user code")
19+
(decision "Idris2 ABI for formal proofs of spec consistency; Zig FFI for C-ABI bridge to Dafny compilation and verification pipeline")
20+
(consequences "Compile-time correctness guarantees for specs; zero runtime overhead from proofs"))
2121

22-
(adr "003-rsr-template"
22+
(adr "003-dafny-verification-pipeline"
23+
(status "accepted")
24+
(context "Dafny uses Z3 SMT solver for automatic verification of requires/ensures/invariant/decreases")
25+
(decision "Pipeline: parse TOML -> Idris2 meta-proofs -> generate .dfy -> invoke Dafny+Z3 -> parse results -> compile target")
26+
(consequences "Verification failures map back to TOML locations; counterexamples shown in user terms, not Dafny terms"))
27+
28+
(adr "004-multi-target-compilation"
29+
(status "accepted")
30+
(context "Dafny compiles to C#, Java, Go, Python, JavaScript — users want verified code in their ecosystem")
31+
(decision "Support all 5 Dafny targets; Zig FFI bridge wraps compiled output for C-ABI integration")
32+
(consequences "One spec, five verified outputs; FFI bridge needed per target runtime"))
33+
34+
(adr "005-rsr-template"
2335
(status "accepted")
2436
(context "Need consistent project structure across 29+ -iser repos")
2537
(decision "All repos cloned from rsr-template-repo with full CI/CD and governance")
2638
(consequences "17 workflows, SECURITY.md, CONTRIBUTING, bot directives from day one")))
2739

2840
(development-practices
29-
(language "Rust" (purpose "CLI and orchestration"))
30-
(language "Idris2" (purpose "ABI formal proofs"))
31-
(language "Zig" (purpose "FFI C-ABI bridge"))
41+
(language "Rust" (purpose "CLI, manifest parsing, orchestration"))
42+
(language "Idris2" (purpose "ABI formal proofs — spec consistency, termination, ghost scoping"))
43+
(language "Zig" (purpose "FFI C-ABI bridge to Dafny compiler and Z3"))
44+
(language "Dafny" (purpose "Generated verification-aware code (never hand-written)"))
3245
(build-tool "cargo")
3346
(ci "GitHub Actions (17 workflows)"))
3447

3548
(design-rationale
3649
(principle "Manifest-driven"
37-
(explanation "User intent captured in TOML; all generation is deterministic and reproducible"))
50+
(explanation "User intent captured in TOML — pre/postconditions, invariants, ghost variables, lemma hints; all generation is deterministic and reproducible"))
3851
(principle "Formally verified bridges"
39-
(explanation "Idris2 dependent types prove interface correctness at compile time"))
40-
(principle "Zero target language exposure"
41-
(explanation "Users never write Chapel/Julia/Futhark/etc. — the -iser handles everything"))))
52+
(explanation "Idris2 dependent types prove spec consistency at compile time — no contradictory requires/ensures, well-founded decreases, ghost variables stay ghost"))
53+
(principle "Zero Dafny exposure"
54+
(explanation "Users never write or read Dafny — the -iser handles all Dafny syntax, Z3 interaction, and target compilation"))
55+
(principle "Counterexample-driven feedback"
56+
(explanation "When Z3 finds a violation, dafniser maps the counterexample back to the TOML spec location with a concrete witness value"))))

‎.machine_readable/6a2/NEUROSYM.a2ml‎

Lines changed: 7 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,20 +1,24 @@
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>
33
#
4-
# NEUROSYM.a2ml — Neurosymbolic integration metadata
4+
# NEUROSYM.a2ml — Neurosymbolic integration metadata for dafniser
55
# Configuration for Hypatia scanning and symbolic reasoning.
66

77
[metadata]
88
version = "0.1.0"
9-
last-updated = "{{CURRENT_DATE}}"
9+
last-updated = "2026-03-21"
1010

1111
[hypatia-config]
1212
scan-enabled = true
1313
scan-depth = "standard" # quick | standard | deep
1414
report-format = "logtalk"
1515

1616
[symbolic-rules]
17-
# Custom symbolic rules for this project
17+
# Custom symbolic rules for dafniser:
18+
# - Ensure generated Dafny always has requires/ensures on every method
19+
# - Ensure decreases annotations on all recursive functions and loops
20+
# - Ensure ghost variables never leak into runtime code paths
21+
# - Ensure lemma dependency graph is acyclic (DAG)
1822
# - { name = "no-unsafe-ffi", pattern = "believe_me|unsafeCoerce", severity = "critical" }
1923

2024
[neural-config]

‎.machine_readable/6a2/PLAYBOOK.a2ml‎

Lines changed: 7 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -1,25 +1,26 @@
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>
33
#
4-
# PLAYBOOK.a2ml — Operational playbook
4+
# PLAYBOOK.a2ml — Operational playbook for dafniser
55
# Runbooks, incident response, deployment procedures.
66

77
[metadata]
88
version = "0.1.0"
9-
last-updated = "{{CURRENT_DATE}}"
9+
last-updated = "2026-03-21"
1010

1111
[deployment]
12-
# method = "gitops" # gitops | manual | ci-triggered
13-
# target = "container" # container | binary | library | wasm
12+
method = "ci-triggered"
13+
target = "binary" # Rust CLI binary; Zig FFI shared library
1414

1515
[incident-response]
16-
# 1. Check .machine_readable/STATE.a2ml for current status
16+
# 1. Check .machine_readable/6a2/STATE.a2ml for current status
1717
# 2. Review recent commits and CI results
1818
# 3. Run `just validate` to check compliance
1919
# 4. Run `just security` to audit for vulnerabilities
20+
# 5. If Dafny verification is failing, check Z3 version compatibility
2021

2122
[release-process]
22-
# 1. Update version in STATE.a2ml, META.a2ml, Justfile
23+
# 1. Update version in STATE.a2ml, META.a2ml, Cargo.toml, Justfile
2324
# 2. Run `just release-preflight` (validate + quality + security + maint-hard-pass)
2425
# 3. Optional local permission hardening: `just perms-snapshot && just perms-lock`
2526
# 4. Tag and push

‎.machine_readable/6a2/STATE.a2ml‎

Lines changed: 16 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -5,31 +5,34 @@
55
(state
66
(metadata
77
(version "0.1.0")
8-
(last-updated "2026-03-20")
8+
(last-updated "2026-03-21")
99
(author "Jonathan D.A. Jewell"))
1010

1111
(project-context
1212
(name "dafniser")
13-
(description "Generate correct-by-construction code using Dafny")
13+
(description "Generate correct-by-construction code for critical functions using Dafny verification and Z3 SMT solving")
1414
(status "scaffold")
1515
(priority "—")
1616
(ecosystem "-iser family (https://github.com/hyperpolymath/iseriser)"))
1717

1818
(current-position
19-
(phase "initial-scaffold")
20-
(completion-percentage 5)
21-
(milestone "Architecture defined, CLI scaffolded, RSR template complete"))
19+
(phase "scaffold-complete")
20+
(completion-percentage 10)
21+
(milestone "Architecture defined, CLI scaffolded, bespoke Idris2 ABI types (Precondition, Postcondition, LoopInvariant, GhostVariable, Lemma, VerificationResult, SpecTree), Zig FFI with Dafny pipeline stubs, TOPOLOGY documented"))
2222

2323
(route-to-mvp
24-
(step 1 "Replace codegen stubs with target-language-specific generation")
25-
(step 2 "Implement Idris2 ABI proofs for core invariants")
26-
(step 3 "Build Zig FFI bridge")
27-
(step 4 "Integration tests with real-world examples")
28-
(step 5 "Documentation and examples"))
24+
(step 1 "Define dafniser.toml schema for function specs with requires/ensures/invariant/decreases/ghost")
25+
(step 2 "Implement spec parser in Rust (manifest/ module)")
26+
(step 3 "Generate Dafny source with verification annotations (codegen/ module)")
27+
(step 4 "Integrate Z3 verification — invoke dafny verify, parse results, map failures to TOML locations")
28+
(step 5 "Multi-target compilation — Dafny to C#/Java/Go/Python/JavaScript")
29+
(step 6 "Idris2 meta-proofs: spec consistency, termination, ghost scoping, lemma DAG")
30+
(step 7 "First working end-to-end example: verified sorting algorithm"))
2931

3032
(blockers-and-issues
31-
(none "Project is in scaffold phase — no blockers yet"))
33+
(none "Project is in scaffold phase with bespoke architecture — no blockers yet"))
3234

3335
(critical-next-actions
34-
(action "Implement codegen for primary use case")
35-
(action "Write first working example end-to-end")))
36+
(action "Define dafniser.toml manifest schema with Dafny-specific fields")
37+
(action "Implement spec parser for requires/ensures/invariant/decreases clauses")
38+
(action "Write first Dafny codegen template for a sorting algorithm")))

‎0-AI-MANIFEST.a2ml‎

Lines changed: 58 additions & 40 deletions
Original file line numberDiff line numberDiff line change
@@ -1,19 +1,29 @@
1-
# ⚠️ STOP - CRITICAL READING REQUIRED
1+
# SPDX-License-Identifier: PMPL-1.0-or-later
2+
# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
3+
#
4+
# 0-AI-MANIFEST.a2ml — Universal AI agent entry point for dafniser
5+
6+
# STOP - CRITICAL READING REQUIRED
27

38
**THIS FILE MUST BE READ FIRST BY ALL AI AGENTS**
49

510
## WHAT IS THIS?
611

7-
This is the AI manifest for **[YOUR-REPO-NAME]**. It declares:
8-
- Canonical file locations (where things MUST be, and nowhere else)
9-
- Critical invariants (rules that must NEVER be violated)
10-
- Repository structure and organization
12+
This is the AI manifest for **dafniser** — a tool that generates
13+
correct-by-construction code for critical functions using Dafny.
14+
15+
Dafniser takes function specifications (pre/postconditions, loop invariants,
16+
ghost variables, lemma hints) from a TOML manifest, generates Dafny source
17+
with `requires`/`ensures`/`invariant`/`decreases` annotations, verifies
18+
them via Z3, and compiles to C#, Java, Go, Python, or JavaScript.
19+
20+
Part of the hyperpolymath -iser family (https://github.com/hyperpolymath/iseriser).
1121

1222
## CANONICAL LOCATIONS (UNIVERSAL RULE)
1323

1424
### Machine-Readable Metadata: `.machine_readable/` ONLY
1525

16-
These 6 a2ml files MUST exist in `.machine_readable/` directory ONLY:
26+
These 6 a2ml files MUST exist in `.machine_readable/6a2/` directory ONLY:
1727
1. **STATE.a2ml** - Project state, progress, blockers
1828
2. **META.a2ml** - Architecture decisions, governance
1929
3. **ECOSYSTEM.a2ml** - Position in ecosystem, relationships
@@ -55,7 +65,7 @@ Policy enforcement contracts (k9, dust, lust, must, trust).
5565
### AI Configuration & Guides: `.machine_readable/ai/` ONLY
5666

5767
- `AI.a2ml` - Language-specific or LLM-specific patterns
58-
- `PLACEHOLDERS.md` - Bootstrap guide
68+
- `PLACEHOLDERS.adoc` - Bootstrap guide
5969

6070
### Community & Forge Metadata: `.github/` ONLY
6171

@@ -70,6 +80,40 @@ Policy enforcement contracts (k9, dust, lust, must, trust).
7080

7181
- `0-AI-MANIFEST.a2ml` - THIS FILE (universal entry point)
7282

83+
## REPOSITORY STRUCTURE
84+
85+
```
86+
dafniser/
87+
├── 0-AI-MANIFEST.a2ml # THIS FILE (start here)
88+
├── README.adoc # What dafniser does and why
89+
├── ROADMAP.adoc # Phase 0-6 roadmap
90+
├── CONTRIBUTING.adoc # Human contribution guide
91+
├── Justfile # Task runner
92+
├── Containerfile # OCI build (Chainguard base)
93+
├── Cargo.toml # Rust CLI dependencies
94+
├── LICENSE # PMPL-1.0-or-later
95+
├── src/
96+
│ ├── main.rs # CLI entry point (init/validate/generate/build/run/info)
97+
│ ├── lib.rs # Library API
98+
│ ├── manifest/ # TOML manifest parser and spec extraction
99+
│ ├── codegen/ # Dafny source generation with verification annotations
100+
│ └── interface/ # Verified Interface Seams
101+
│ ├── abi/ # Idris2 ABI (Types, Layout, Foreign)
102+
│ │ ├── Types.idr # Precondition, Postcondition, LoopInvariant,
103+
│ │ │ # GhostVariable, Lemma, VerificationResult, SpecTree
104+
│ │ ├── Layout.idr # Memory layout proofs for ABI types
105+
│ │ └── Foreign.idr # FFI declarations (Dafny compile, Z3 verify, target compile)
106+
│ ├── ffi/ # Zig FFI (The Bridge)
107+
│ │ ├── build.zig # Build config (shared + static libs)
108+
│ │ ├── src/main.zig # C-ABI implementation of Foreign.idr
109+
│ │ └── test/ # Integration tests
110+
│ └── generated/ # C Headers (auto-generated from Idris2 ABI)
111+
├── docs/
112+
│ └── architecture/
113+
│ └── TOPOLOGY.md # Module topology and data flow diagram
114+
└── .machine_readable/ # ALL machine-readable metadata (6a2/ subdirectory)
115+
```
116+
73117
## CORE INVARIANTS
74118

75119
1. **No state file duplication** - Root must NOT contain STATE.a2ml, META.a2ml, etc.
@@ -80,42 +124,16 @@ Policy enforcement contracts (k9, dust, lust, must, trust).
80124
6. **Container images** - MUST use Chainguard base (`cgr.dev/chainguard/wolfi-base:latest` or `cgr.dev/chainguard/static:latest`)
81125
7. **Container runtime** - Podman, never Docker. Files are `Containerfile`, never `Dockerfile`
82126
8. **Container orchestration** - `selur-compose`, never `docker-compose`
83-
84-
## REPOSITORY STRUCTURE
85-
86-
This repo follows the **Dual-Track** architecture:
87-
88-
```
89-
[YOUR-REPO-NAME]/
90-
├── 0-AI-MANIFEST.a2ml # THIS FILE (start here)
91-
├── README.adoc # High-level orientation (Rich Human)
92-
├── ROADMAP.adoc # Future direction
93-
├── CONTRIBUTING.adoc # Human contribution guide
94-
├── GOVERNANCE.adoc # Decision-making model
95-
├── Justfile # Task runner
96-
├── Containerfile # OCI build
97-
├── LICENSE # Primary license
98-
├── src/ # Source code
99-
│ └── interface/ # Verified Interface Seams
100-
│ ├── abi/ # Idris2 ABI (The Spec)
101-
│ ├── ffi/ # Zig FFI (The Bridge)
102-
│ └── generated/ # C Headers (The Result)
103-
├── container/ # Stapeln container ecosystem
104-
├── docs/ # Technical depths
105-
│ ├── attribution/ # Citations, owners, maintainers (adoc)
106-
│ ├── architecture/ # Topology, diagrams
107-
│ ├── theory/ # Domain theory
108-
│ └── practice/ # Manuals
109-
├── docs/legal/ # Legal exhibits and full texts
110-
└── .machine_readable/ # ALL machine-readable metadata
111-
```
127+
9. **Dafny pipeline order** - Always: parse spec -> meta-prove (Idris2) -> generate .dfy -> verify (Z3) -> compile target
128+
10. **No manual Dafny** - Users never write Dafny; dafniser generates everything from TOML specs
112129

113130
## SESSION STARTUP CHECKLIST
114131

115-
✅ Read THIS file (0-AI-MANIFEST.a2ml) first
116-
✅ Understand canonical location: `.machine_readable/`
117-
✅ State understanding of canonical locations
132+
1. Read THIS file (0-AI-MANIFEST.a2ml) first
133+
2. Understand canonical location: `.machine_readable/`
134+
3. Read `.machine_readable/6a2/STATE.a2ml` for current project state
135+
4. State understanding of canonical locations
118136

119137
## ATTESTATION PROOF
120138

121-
**"I have read the AI manifest. All machine-readable content (state files, anchors, policies, bot directives, contractiles, AI guides) is located in `.machine_readable/` ONLY, and community metadata is in `.github/`. I will not create duplicate files in the root directory."**
139+
**"I have read the AI manifest for dafniser. All machine-readable content (state files, anchors, policies, bot directives, contractiles, AI guides) is located in `.machine_readable/` ONLY, and community metadata is in `.github/`. I will not create duplicate files in the root directory."**

0 commit comments

Comments
 (0)