Wave B.4 — VirtualFs trio in C: vfs_tulis/vfs_baca/vfs_padam compile, gated and quota'd as the interpreter - #87
Draft
ib823 wants to merge 4 commits into
Draft
Wave B.4 — VirtualFs trio in C: vfs_tulis/vfs_baca/vfs_padam compile, gated and quota'd as the interpreter#87ib823 wants to merge 4 commits into
ib823 wants to merge 4 commits into
Conversation
…mpile, gated and quota'd as the interpreter
THE GAP. `vfs_tulis`/`vfs_baca`/`vfs_padam` were the last interpreter-only
family with a stated reason: the interpreter runs `riina-os::vfs::VirtualFs`
(the Rust port of Coq domains/VerifiedFileSystem.v) and emitted C had no
in-memory filesystem, so `lower.rs` refused to route the trio rather than stub
it into something that ignores the quota. `vfs_mula` was routed but accepted
its byte-limit argument and IGNORED it, by its own comment.
THE PORT. `emit.rs` now carries the C half of `VirtualFs`, emitted beside the
file gate it already had (same `riina_perm_t`, same shared access context):
- a node table separate from the host-FS gate's — in the interpreter
`HostGate` and `VfsState` are two tables sharing ONE context, and that is
reproduced, not merged;
- `vfs_tulis`: unknown path → `can_allocate_inode` (used < limit), then
first-touch ownership by the current uid/gid at mode 0644, one inode
charged; then `can_write`; then the byte quota on GROWTH only
(`can_allocate_bytes(new - old)` with the overflow guard Rust's
`checked_add` gives), shrinking refunds;
- `vfs_baca`: not found → can_read → the bytes;
- `vfs_padam`: not found → can_write → both quotas released;
- `vfs_mula(limit)`: resets the table and honours the limit (inode limit
4096, the interpreter's DEFAULT_INODE_LIMIT); before it, u64::MAX.
Every check precedes every mutation, and each refusal carries the
interpreter's wording — `vfs: not found` / `vfs: permission denied` /
`vfs: quota exceeded` — and exits non-zero. Byte counts use the string's byte
length, not strlen, as the interpreter charges `data.as_bytes().len()`.
ONE SPECIFICATION, TWO IMPLEMENTATIONS, held together by a differential.
`vfs_differential.rs` runs the same `.rii` program under `riinac run` and as a
native binary and requires the two to agree line-for-line on stdout AND, for
the cases the model refuses, to both exit non-zero with the same `vfs:`
reason with nothing after the refused operation running. Ten cases, each
with the control that shows the gate decided: cross-user write denied vs
cross-user read allowed (mode 0644); growth over the limit refused vs the
same bytes at the limit accepted vs shrink-then-regrow (refund); the byte
quota counted across files; delete gated by can_write; delete-then-create
releasing the inode and reassigning ownership; unknown path not found on
read and on delete; a quota-refused growth leaving the accounting untouched.
NEGATIVE CONTROL: deleting the C growth-quota check makes exactly the two
quota cases fail and the other eight pass — the differential pins the C
semantics, not a coincidence. `file_gate_parity.rs` (the compiled backend
must never bypass the verified file gate) still passes.
Registry re-derived from the compiler (REGEN_STDLIB_DOC): the trio moves
`interp-only` → `native-only`; on this branch 347 of 373 compile,
`interp-only` 24 → 18 (the `jaring_tls_*` 16 and `csrf_generate` 2 remain,
each with its stated reason). WASM still fails closed on `vfs_*`.
`pkg_build.rs::package_using_interpreter_only_builtin_fails_at_codegen` used
`vfs_baca` as its boundary example and its own comment predicted this day;
it now uses `jaring_tls_jabat`, which sits on the boundary by DECISION
(REQ-70) rather than by backlog.
VERIFIED: 3334 Rust tests / 0 failed with the WASM/C differentials live;
clippy clean under -D warnings; corpus ratchet holds 97/172.
Master plan: REQ-70 row (the VirtualFs reason → PORTED, status cell) and the
Gate C status paragraph re-derived. This row is also edited by PR #86
(Wave B.3); whichever merges second resolves the one-line conflict.
Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01Uu28z8CdRQ1SLzTv8yszth
verify --full PASS written by the pre-push gate for the Wave B.4 push (3334 Rust tests, 331 .vo, Transpiler Staleness OK), staged after the commit it describes had landed — committed here so the record travels with the branch. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Uu28z8CdRQ1SLzTv8yszth
Both Wave B branches were cut from main, as agreed, and both re-derive the
registry and touch the one-line REQ-70 row, so the merge conflicted on
exactly the regenerable surface plus that row:
- 46 metrics-banner docs, docs/api/STDLIB.md, website/public/metrics.json,
VERIFICATION_MANIFEST.md: main's versions taken, then REGENERATED with the
repo's tooling on the merged tree (REGEN_STDLIB_DOC, generate-metrics.sh,
sync-metrics.sh) — never merged by hand.
- RIINA_MASTER_PLAN.md: main's version (carrying Wave B.3's REQ-48/REQ-70
text) with Wave B.4's three edits re-applied on top — the VirtualFs
reason → PORTED, the REQ-70 status cell naming both items done, and the
Gate C paragraph with the numbers re-derived on the MERGED tree:
348 of 374 compile, interp-only 32 → 26, typed-only 0 (the jaring_tls_*
16, csrf_generate 2 and the 8 crypto-agility handles remain, each with
its stated reason).
On the merged tree: vfs_differential 10/10, kripto_runtime 7/7, kripto unit
11/11, pkg_build 8/8, file_gate_parity 1/1; clippy clean under -D warnings;
audit-docs PASSED; metrics re-derived on the merged tree: 3352 tests (full cargo
test). The pre-push gate's verify --full is the full record.
Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01Uu28z8CdRQ1SLzTv8yszth
verify --full PASS written by the pre-push gate for the main-into-#87 merge (3352 Rust tests, 331 .vo, Transpiler Staleness OK), staged after the commit it describes had landed — committed here so the record travels with the branch. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Uu28z8CdRQ1SLzTv8yszth
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.
Wave B.4.
vfs_tulis/vfs_baca/vfs_padamwere the last interpreter-only family with a stated reason — "needs an in-memory FS + quota in C" — because the interpreter runsriina-os::vfs::VirtualFs(the Rust port of Coqdomains/VerifiedFileSystem.v) and emitted C had no in-memory filesystem, solower.rsrefused to route the trio rather than stub it into something that ignores the quota.vfs_mulawas routed but, by its own comment, ignored its byte-limit argument. This ports the model.The port
emit.rsnow carries the C half ofVirtualFs, emitted beside the file gate it already had (sameriina_perm_t, same shared access context), mirrored operation by operation:vfs_tulis(path, data)can_allocate_inode(used < limit) → first-touch ownership by the current uid/gid at mode 0644, one inode charged; thencan_write; then the byte quota on growth only (can_allocate_bytes(new − old), with the overflow guard Rust'schecked_addgives); shrinking refundsvfs_baca(path)can_read→ the bytesvfs_padam(path)can_write→ both quotas releasedvfs_mula(limit)u64::MAXbefore itEvery check precedes every mutation. Each refusal carries the interpreter's wording —
vfs: not found/vfs: permission denied/vfs: quota exceeded— and exits non-zero. The node table is separate from the host-FS gate's: in the interpreterHostGate(fail_*) andVfsState(vfs_*) are two tables sharing one access context, and that is reproduced, not merged.One specification, two implementations — held together by a differential
vfs_differential.rsruns the same.riiprogram underriinac runand as a native binary and requires the two to agree line-for-line on stdout and, for the cases the model refuses, to both exit non-zero with the samevfs:reason with nothing after the refused operation running. Ten cases, each with the control that shows the gate decided:Negative control: deleting the C growth-quota check makes exactly the two quota cases fail and the other eight pass, so the differential pins the C semantics rather than a coincidence.
file_gate_parity.rs(the compiled backend must never bypass the verified file gate) still passes.One existing test moved with the boundary:
pkg_build.rs::package_using_interpreter_only_builtin_fails_at_codegenusedvfs_bacaas its interpreter-only example and its own comment predicted this day. It now usesjaring_tls_jabat, which sits on the boundary by decision (REQ-70: a C TLS that is not reallyriina-tlswould be worse than a build error) rather than by backlog.Verification
-D warnings; corpus ratchet holds 97/172REGEN_STDLIB_DOC=1): the trio movesinterp-only→native-only. On the merged tree: 348 of 374 compile, interp-only 26, typed-only 0 — thejaring_tls_*16,csrf_generate2 and the 8 crypto-agility handles remain, each with its stated reason. WASM still fails closed onvfs_*Merged with
mainafter #86 landed. The conflict was exactly the regenerable surface (46 metrics-banner docs,STDLIB.md,metrics.json, the manifest) plus the one-line REQ-70 row and the Gate C paragraph. The regenerable files were taken frommainand regenerated with the repo's tooling on the merged tree; the two plan spots were hand-merged so both Wave B.3's and B.4's records stand, with the numbers re-derived on the merged tree.🤖 Generated with Claude Code
https://claude.ai/code/session_01Uu28z8CdRQ1SLzTv8yszth