From 785c1961d3a86072ae28b16d1caf9b5baf43f9ab Mon Sep 17 00:00:00 2001 From: Claude Date: Fri, 5 Jun 2026 14:23:55 +0000 Subject: [PATCH] docs(machine_readable): refresh 6a2 + ANCHOR (proofs, FFI, reconciliation) Replace the March .scm-converted stubs with current content: STATE (proven surface, proof-campaign milestones, blockers, 2026-06-05 reconciliation), META (architecture + decisions D1/D2/D3 + totality practices), NEUROSYM (discharged/open proof obligations + honest bounds), ECOSYSTEM (related projects + declared integrations), AGENTIC (proof-escape constraints + agent workflow), PLAYBOOK (build/verify/release runbooks). ANCHOR gains a realignment record for the convergence + combiner generalization. https://claude.ai/code/session_011z2t8zAxfcCNLJzU7YdpBQ --- .machine_readable/6a2/AGENTIC.a2ml | 17 ++++-- .machine_readable/6a2/ECOSYSTEM.a2ml | 22 +++++++- .machine_readable/6a2/META.a2ml | 30 +++++++++-- .machine_readable/6a2/NEUROSYM.a2ml | 27 +++++++++- .machine_readable/6a2/PLAYBOOK.a2ml | 29 ++++++----- .machine_readable/6a2/STATE.a2ml | 74 ++++++++++++++++++++++++--- .machine_readable/anchors/ANCHOR.a2ml | 13 +++++ 7 files changed, 181 insertions(+), 31 deletions(-) diff --git a/.machine_readable/6a2/AGENTIC.a2ml b/.machine_readable/6a2/AGENTIC.a2ml index 9931a7a..f028180 100644 --- a/.machine_readable/6a2/AGENTIC.a2ml +++ b/.machine_readable/6a2/AGENTIC.a2ml @@ -3,10 +3,9 @@ # # AGENTIC.a2ml — AI agent constraints and capabilities # Defines what AI agents can and cannot do in this repository. - [metadata] version = "0.1.0" -last-updated = "2026-03-16" +last-updated = "2026-06-05" [agent-permissions] can-edit-source = true @@ -17,8 +16,16 @@ can-create-files = true [agent-constraints] # What AI agents must NOT do: -# - Never use banned language patterns (believe_me, unsafeCoerce, etc.) +# - Never use banned proof escapes (believe_me, assert_total, postulate, unsafePerformIO, holes) on proof symbols +# - Never weaken %default total, nor introduce `covering` / `partial` on verification code # - Never commit secrets or credentials # - Never use banned languages (TypeScript, Python, Go, etc.) -# - Never place state files in repository root (must be in .machine_readable/) -# - Never use AGPL license (use MPL-2.0) +# - Never place state/meta files in repository root (must live under .machine_readable/) +# - Never use AGPL (license is MPL-2.0) + +[agent-workflow] +# How AI agents should work here: +proof-campaign = "resume from docs/PROOFS.adoc — the authoritative, dependency-sorted plan; it survives context compaction" +post-migration = "on return from the svalinn → Ephapax track, follow docs/AFTER-MIGRATION.adoc before resuming" +verification-gate = "idris2 --build ochrance.ipkg must stay clean and fully total" +model-guidance = "Opus for proof discovery / structural walls; Sonnet for mechanisation, refactors, tests; Haiku for grunt sweeps" diff --git a/.machine_readable/6a2/ECOSYSTEM.a2ml b/.machine_readable/6a2/ECOSYSTEM.a2ml index 329af2c..0616b01 100644 --- a/.machine_readable/6a2/ECOSYSTEM.a2ml +++ b/.machine_readable/6a2/ECOSYSTEM.a2ml @@ -1,10 +1,28 @@ # SPDX-License-Identifier: MPL-2.0 +# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +# # ECOSYSTEM.a2ml — Ecosystem position -# Converted from ECOSYSTEM.scm on 2026-03-15 - [metadata] project = "ochrance" ecosystem = "hyperpolymath" +last-updated = "2026-06-05" [position] type = "component" +role = """Neurosymbolic filesystem-integrity verifier — the receipt/attestation layer for accountable state transitions.""" + +[related-projects] +projects = [ + "echidna — Rust/Julia neurosymbolic prover (provides libechidna.so); Ochránce adds Idris2 as a backend", + "idris2-echidna — Idris2 prover abstraction layer", + "proven — Idris2 formally verified library", + "ochrance-framework — architecture + docs; its duplicate core is retired (D1)", + "svalinn — estate sibling, edge verification gateway; migrating ReScript → Ephapax (D3)", + "valence-shell — consumes Ochránce receipts for accountable state transitions (see integrations/valence-shell-bridge.a2ml)", + "echo-types — semantics of the residue/loss those transitions expose", + "boj-server — SSG/build host (casket engine); ANCHOR parent (see anchors/ANCHOR.a2ml)", +] + +[integrations] +# detail in .machine_readable/integrations/*.a2ml +declared = [ "proven", "valence-shell-bridge", "verisimdb", "vexometer", "feedback-o-tron" ] diff --git a/.machine_readable/6a2/META.a2ml b/.machine_readable/6a2/META.a2ml index 3210aa0..af5ec3d 100644 --- a/.machine_readable/6a2/META.a2ml +++ b/.machine_readable/6a2/META.a2ml @@ -1,9 +1,33 @@ # SPDX-License-Identifier: MPL-2.0 -# META.a2ml — Project meta-information -# Converted from META.scm on 2026-03-15 - +# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +# +# META.a2ml — Architecture decisions & development practices [metadata] project = "ochrance" author = "Jonathan D.A. Jewell " license = "MPL-2.0" standard = "RSR 2026" +last-updated = "2026-06-05" + +[architecture] +summary = """6-layer trust pyramid (L0 hardware root → L5 TUI/telemetry). Framework-first: a VerifiedSubsystem interface with pluggable modules; the filesystem is the reference subsystem. A2ML is the attestation/audit markup. A verified Merkle tree carries a combiner-generic soundness theorem. Crypto is provided by a thin Zig FFI over std.crypto.""" +core = "ochrance-core (Idris2) — single source of proof truth" +ffi = "ffi/zig (BLAKE3 / SHA-256 / SHA3-256 / Ed25519); thin C NVMe syscall shims (L1)" +languages = "Idris2 (proofs), Zig (FFI), C (syscall shims), Rust + Julia (ECHIDNA, future)" + +[decisions] +# architecture decisions on record (proof-side rationale in docs/PROOFS.adoc) +records = [ + "D1 — single core: ochrance-core is the source of truth; ochrance-framework's duplicate core is retired, its mode-indexed VerifiedSubsystem Interface harvested.", + "D2 — crypto binding as a typed interface: collision resistance modelled as an Idris hypothesis (CollisionResistant h); the binding theorem is discharged against it, not left as prose.", + "D3 — svalinn migrates ReScript → Ephapax before proof (migrate-then-prove).", + "Combiner generalization: Merkle construction/verification/soundness are parameterised over the hash combiner; XOR and BLAKE3 are instances of one universally-quantified theorem; cryptographic binding is the separate trust assumption.", +] + +[practices] +totality = "every module carries %default total; structural recursion only; no believe_me / assert_* / postulate / unsafePerformIO / holes on proof symbols" +idris = "Idris2 0.8.0+" +progressive-strictness = "verification supports Lax / Checked / Attested modes" +error-taxonomy = "q/ query · p/ proof · z/ zone" +ci = "type-check + totality gate, A2ML/property/integration/e2e suites, Zig FFI build+test, CodeQL, secret scans, RSR antipattern / SPDX / workflow linters" +docs = "AsciiDoc (.adoc) except GitHub-required files; the proof campaign is tracked in docs/PROOFS.adoc" diff --git a/.machine_readable/6a2/NEUROSYM.a2ml b/.machine_readable/6a2/NEUROSYM.a2ml index 767d7dd..4ae988d 100644 --- a/.machine_readable/6a2/NEUROSYM.a2ml +++ b/.machine_readable/6a2/NEUROSYM.a2ml @@ -3,12 +3,35 @@ # # NEUROSYM.a2ml — Neurosymbolic integration metadata # Configuration for Hypatia scanning and symbolic reasoning. - [metadata] version = "0.1.0" -last-updated = "2026-03-16" +last-updated = "2026-06-05" [hypatia-config] scan-enabled = true scan-depth = "standard" report-format = "logtalk" + +[symbolic] +prover = "Idris2 (dependent types)" +neural-backend = "ECHIDNA (Rust/Julia) — FFI stubbed, integration pending" +abstraction = "idris2-echidna prover layer (planned 13th ECHIDNA backend)" + +[proof-obligations] +# discharged — machine-checked, axiom-free +discharged = [ + "merkleCorrectWith — combiner-generic inclusion soundness", + "verifyProofReconstructsWith — verify ≡ root == reconstruct", + "roundtripManifest — grammar invertibility over the reference token codec", + "progressive assurance (SatisfiesMinimum / attestedSatisfiesLax)", +] +# open — see docs/PROOFS.adoc Stages 1–4 +open = [ + "buildMerkleTree correctness + IO↔pure bridge to the production crypto path", + "CollisionResistant h + merkleBinding (D2)", + "Verify / Validator soundness; repair correctness (L3 linear); Merkle completeness", +] + +[honest-bounds] +# boundaries by design — documented, never faked +notes = """The production parse∘lex∘serialize round-trip rests on primitive String operations (pack/unpack/parseInteger) with no equational theory; the honest guarantee is roundtripManifest over a reference token codec, complemented by a runtime round-trip property. The residual root==root Bool step in merkleCorrect is propositional digest equality — the strongest honest statement without an unsafe reflexivity axiom.""" diff --git a/.machine_readable/6a2/PLAYBOOK.a2ml b/.machine_readable/6a2/PLAYBOOK.a2ml index a961250..7b9dc04 100644 --- a/.machine_readable/6a2/PLAYBOOK.a2ml +++ b/.machine_readable/6a2/PLAYBOOK.a2ml @@ -2,22 +2,27 @@ # Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) # # PLAYBOOK.a2ml — Operational playbook -# Runbooks, incident response, deployment procedures. - +# Runbooks, build/verify procedures, incident response. [metadata] version = "0.1.0" -last-updated = "2026-03-16" +last-updated = "2026-06-05" -[deployment] -# method = "gitops" -# target = "container" +[build-and-verify] +typecheck = "idris2 --build ochrance.ipkg # must be clean and fully total" +single-file = "idris2 --check ochrance-core/Ochrance/A2ML/Lexer.idr" +ffi = "cd ffi/zig && zig build && zig build test # BLAKE3 / SHA-256 / SHA3-256 / Ed25519 KATs (Zig 0.11.0)" +suites = "A2ML parser, property, integration, and tests/e2e_test.sh" [incident-response] -# 1. Check .machine_readable/STATE.a2ml for current status -# 2. Review recent commits and CI results -# 3. Run just validate to check compliance +steps = [ + "Check .machine_readable/6a2/STATE.a2ml for current status, blockers, and next actions", + "Review recent commits and CI results on main", + "Re-run the proof build (idris2 --build ochrance.ipkg) and the affected suite", +] [release-process] -# 1. Update version in STATE.a2ml, META.a2ml -# 2. Run just quality (format, lint, test) -# 3. Tag and push +steps = [ + "Update version + last-updated in STATE.a2ml and META.a2ml", + "Ensure CI is green (totality gate, suites, Zig FFI build+test, CodeQL, RSR linters)", + "Tag and push", +] diff --git a/.machine_readable/6a2/STATE.a2ml b/.machine_readable/6a2/STATE.a2ml index bad2b8f..ef1b1a0 100644 --- a/.machine_readable/6a2/STATE.a2ml +++ b/.machine_readable/6a2/STATE.a2ml @@ -1,14 +1,74 @@ # SPDX-License-Identifier: MPL-2.0 -# STATE.a2ml — Project state checkpoint -# Converted from STATE.scm on 2026-03-15 - +# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +# +# STATE.a2ml — Ochránce project state checkpoint [metadata] project = "ochrance" version = "0.1.0" -last-updated = "2026-03-15" +last-updated = "2026-06-05" status = "active" +session = "machine-readable checkpoint — 2026-06-05" [project-context] -name = "ochrance" -completion-percentage = 0 -phase = "In development" +name = "Ochránce" +purpose = """Neurosymbolic filesystem verification framework in Idris2 dependent types: a pluggable VerifiedSubsystem interface, A2ML attestation/audit markup, a verified Merkle tree with a combiner-generic soundness theorem, and ECHIDNA integration.""" +completion-percentage = 40 + +[position] +phase = "implementation" # design | implementation | testing | maintenance | archived +maturity = "experimental" # experimental | alpha | beta | production | lts + +[proven-surface] +# machine-checked, axiom-free (no believe_me / assert_* / postulate / holes on proof symbols) +theorems = [ + "merkleCorrect / merkleCorrectWith — inclusion-proof soundness, generic over the hash combiner (XOR & BLAKE3 are instances)", + "verifyProofReconstructs(With) — verify ≡ (root == reconstruct leaf prf)", + "roundtripManifest (+ algoRT/modeRT/refsRT/mpolRT codecs) — decodeManifest (encodeManifest m) = Just m", + "SatisfiesMinimum / attestedSatisfiesLax — progressive-assurance threshold witness", + "ABI Handle / createHandle — So (ptr /= 0) non-null invariant", + "supporting lemmas: reconstructAppendWith, powerTwoSucc, justInj", +] + +[route-to-mvp] +# the proof campaign — docs/PROOFS.adoc is the authoritative, dependency-sorted plan +milestones = [ + "Stage 1 — Merkle closure (buildMerkleTree correctness, IO↔pure bridge) + crypto-binding interface (CollisionResistant)", + "Stage 2 — Verify + Validator soundness; hex codec round-trip", + "Stage 3 — Repair correctness (L3 linear types); harvest framework's mode-indexed Interface", + "Stage 4 — Merkle completeness, binding discharge, progressive monotonicity, write-up", +] + +[blockers-and-issues] +issues = [ + "No cryptographic-integrity claim yet: Idris stub fallbacks (hashPairStub / blake3Stub / ed25519VerifyStub in FFI/Crypto.idr) remain in the verification flow; libochrance.so not yet built + linked in", + "Repair (L3) idempotence is property-tested only, not yet proven", + "ECHIDNA FFI is stubbed (echidnaProve returns 'FFI not yet implemented')", + "Production round-trip (parse∘lex∘serialize) is honestly bounded by primitive String ops — see docs/PROOFS.adoc", +] + +[critical-next-actions] +actions = [ + "Stage 1 (Opus): buildMerkleTree index/root-fold laws; bridge verifyProofIO/rootHashBytesIO to the …With spec", + "Introduce CollisionResistant h + merkleBinding interface (D2)", + "Remove Idris-side crypto stubs and build + link libochrance.so into the flow (unblocks the crypto-integrity claim)", + "Sync .machine_readable scaffold to rsr-template (ai/, compliance/, configs/, policies/, scripts/, 0.1-AI-MANIFEST, ENSAID_CONFIG, root README, root-allow) — pending template access", +] + +[recent-history] +# 2026-06-05 reconciliation: main is now the single trunk +merged = [ + "#31 — Zig crypto FFI (BLAKE3/SHA-256/SHA3-256/Ed25519) + zig-ffi.yml CI + Valence-Shell bridge docs", + "#32 — A2ML parser totality + correctness, Merkle combiner generalization, proof ledger, post-migration re-entry runbook", + "#33 — nixpkgs flake.lock bump", + "#34 — CodeQL cron weekly→monthly", +] +decisions = [ + "D1 — converge on ochrance-core (ochrance-framework duplicate core retired; mode-indexed VerifiedSubsystem Interface harvested)", + "D2 — crypto binding modelled as a typed CollisionResistant hypothesis, discharged not asserted", + "D3 — svalinn migrates ReScript → Ephapax (migrate-then-prove)", +] + +[maintenance-status] +last-run-utc = "2026-06-05T14:08:00Z" +last-result = "pass" # unknown | pass | warn | fail +notes = "CI green on main; core builds fully total. A2ML parser 16/16, property 47/47, e2e 22/22; integration suite and Zig FFI build+test green." diff --git a/.machine_readable/anchors/ANCHOR.a2ml b/.machine_readable/anchors/ANCHOR.a2ml index 7205c5b..b33ef32 100644 --- a/.machine_readable/anchors/ANCHOR.a2ml +++ b/.machine_readable/anchors/ANCHOR.a2ml @@ -16,3 +16,16 @@ ssg: # Relationships parents: - "org.hyperpolymath.boj-server" + +# Realignments — significant repository realignments on record +realignments: + - date: "2026-06-05" + kind: "convergence + proof-campaign" + summary: > + Converged on ochrance-core as the single source of proof truth (D1); + retired the ochrance-framework duplicate core and harvested its + mode-indexed VerifiedSubsystem interface. Generalised Merkle + construction / verification / soundness over the hash combiner + (XOR and BLAKE3 as instances of one theorem). Implemented the Zig + crypto FFI. Reconciled all open branches into a single main. + authority: "docs/PROOFS.adoc"