Arena/aspect weave - #89
Merged
Merged
Conversation
Owner decision 2026-09-24: aspects are implemented once, in the canonical Zig gateway. The twin could not compile (rand 0.10 API drift; CI red on main) and duplicated every cross-cutting concern. Drops: src/api/rust/, root Cargo workspace, rust-ci.yml, .gitlab-ci.yml cargo stages, MIGRATION.adoc, mise/.tool-versions rust pins, and rust entries in manifests/docs. Estate law unchanged: ABI = Idris2, FFI/API = Zig. Future Rust, if any, must be Creusot-verified. Co-authored-by: arena-agent <297053741+arena-agent@users.noreply.github.com>
The gateway could not build publicly: libzig_api came from developer-ecosystem (hardcoded /var/mnt/eclipse paths), whose own build needs libproven_ffi from the private verification-ecosystem repo. Implement the uapi surface in-repo (estate law: FFI = Zig), declared ABI-first in src/abi/Gnosis.idr and asserted against zig_api.h in tests. GnosisRequestV2 is the aerie extension that carries the query string and headers — v1 strips both, so the deployed policy gate never saw X-Api-Key and resolvers never saw ?target= params. Verified: zig build ReleaseSafe + zig build test green; gateway serves /api/v1/health, degrades gracefully with probes down, clean shutdown. Co-authored-by: arena-agent <297053741+arena-agent@users.noreply.github.com>
Design accepted (docs/design/forensic-stack.adoc): the Zig relational engine is outside the trust boundary — it emits candidate attack paths as RawStep derivations; the Idris2 kernel checks each against the evidence (de Bruijn criterion). A solver bug can only lose answers. src/abi/Forensics.idr: Retention (echo-types thin poset, port-and- reprove), evidence-indexed Lateral/Reach, checkReach signature, CertificateCheck + non-factive Warrant (epistemic-types surfaces). ffi/zig/src/kanren.zig: evidence table, depth-bounded search over the kanren_* C ABI; budgeted no-answer is distinct from no-answer-exists (tropical budget seam). Agda/Lean repos cited as authority. Not yet type-checked in Idris2 (no toolchain here; CI is the witness). Co-authored-by: arena-agent <297053741+arena-agent@users.noreply.github.com>
The weave's skeleton: kyaml.zig (strict KEP-5295 subset, rule Y-3), config.zig (defaults < KYAML < env; only getenv reader), ctx.zig (per-request context, globals and the shared static buffer gone), errors.zig (one statusOf), router.zig (THE route table: paths, verbs, modules, resolvers; boundary-guarded), respond.zig (single write path). main.zig: 756 inline lines -> lifecycle + the V2 handler. GnosisRequestV2 gains resp_scratch: per-connection response storage owned by the server. The weave exposed a real lifetime bug — bodies must outlive the handler call (the socket write happens after return); the old code survived only via the never-freed static. Verified: ?target= params work (dead since single-port), real 400s, verb enforcement, deterministic across runs. Co-authored-by: arena-agent <297053741+arena-agent@users.noreply.github.com>
Contributor
|
Navigate logical layers of code changes, visualize relationships, and explore their blast radius. Note Currently processing new changes in this PR. This may take a few minutes, please wait... ⚙️ Run configurationConfiguration used: Organization UI Review profile: ASSERTIVE Plan: Advanced Run ID: ⛔ Files ignored due to path filters (1)
📒 Files selected for processing (49)
✨ Finishing Touches📝 Generate docstrings
Thanks for using CodeRabbit! It's free for OSS, and your support helps us grow. If you like it, consider giving us a shout-out. Comment |
![github-advanced-security[bot]](https://avatars.githubusercontent.com/in/57789?s=60&v=4){kind=small}
| @@ -0,0 +1,311 @@ | |||
| // SPDX-License-Identifier: MPL-2.0 | |||
| @@ -0,0 +1,572 @@ | |||
| // SPDX-License-Identifier: MPL-2.0 | |||
| @@ -0,0 +1,79 @@ | |||
| // SPDX-License-Identifier: MPL-2.0 | |||
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
Changes
RSR Quality Checklist
Required
just testor equivalent)just fmtor equivalent)unsafeblocks without// SAFETY:commentsbelieve_me,unsafeCoerce,Obj.magic,Admitted,sorry).envfiles includedAs Applicable
.machine_readable/descriptiles/STATE.a2mlupdated (if project state changed).machine_readable/descriptiles/ECOSYSTEM.a2mlupdated (if integrations changed).machine_readable/descriptiles/META.a2mlupdated (if architectural decisions changed)TOPOLOGY.mdupdated (if architecture changed)CHANGELOGor release notes updatedsrc/interface/abi/andsrc/interface/ffi/consistent)Testing
Screenshots