⚡ Bolt: Extract Zustand selectors in App.tsx to prevent root re-renders - #190
⚡ Bolt: Extract Zustand selectors in App.tsx to prevent root re-renders#190teerthsharma wants to merge 487 commits into
Conversation
…pu test plan, browser html/dom - Add Aether stdlib: List, Map, StringBuilder, fs I/O - Add Aether build driver (Phase 0 self-hosting) - Add AMD GPU hardware dispatch proof (Stream 13) - Add GPU test harness and OpenCL C shader sources - Rename GPU test plan to generic GPU_TEST_PLAN.md - Add browser HTML parser + DOM (Stream 14) - Add Ubuntu benchmark artifact scaffolding (Stream 8) - Add VM verifier, peephole, trace cache (Stream 3) - Add incremental lexing + error recovery (Stream 1) NO STUBS: removes compile_shaders.py --stubs poison and generated stub binaries. Real shader compilation requires ROCm clang at build time.
Co-authored-by: teerthsharma <78080953+teerthsharma@users.noreply.github.com>
Co-authored-by: teerthsharma <78080953+teerthsharma@users.noreply.github.com>
Co-authored-by: teerthsharma <78080953+teerthsharma@users.noreply.github.com>
…nding test `ipv4::transport_checksum_uses_the_delivered_destination` builds a broadcast datagram to 255.255.255.255, then rebuilds it summed against `local_ip()` and requires the second to be refused. Its guard checked that the two addresses differ. They do, and it proves nothing. The internet checksum adds 16-bit words in one's complement with end-around carry, which makes 0xFFFF an identity: adding it overflows to `x - 1` and the carry adds back to `x`. Adding 0x0000 is an identity too. So 255.255.255.255 and 0.0.0.0 contribute the same amount — nothing — and produce byte-identical checksums. `local_ip()` is 0.0.0.0 until DHCP completes, which it has not at test time, so the mirror datagram carried a checksum that was correct for the address it was actually delivered to. It was accepted, and the assertion failed, at 409/410 in CI on run 31477047356. The mirror address is now 198.51.100.7, and the guard compares the checksum fields of the two segments rather than the addresses. Address inequality does not imply distinguishability under a checksum, which is the same argument commit 916e485 used to prove its source/destination swap an equivalent mutant, applied to the fixture instead of the mutation. Verification: `cargo +nightly clippy --release --target x86_64-unknown-uefi` on this machine, forced by touch, reports 0 errors in both profiles. The assertion's own failure in CI is the control: it accepted a datagram whose checksum was built for a different address, which is exactly what the test exists to forbid, and it could not have detected that with the addresses it was given. The other 409 registered assertions passed on the same run. Limits: QEMU is not installed on this machine, so whether the repaired fixture now discriminates is confirmed by CI rather than here. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
…he shell Commit 8a24f43 gave the shell pipelines and redirection with one stdin consumer, `grep`. A pipeline with one filter in it composes nothing. Seven filters now share one free entry point, `run_filter(input, stdin)`, which holds the whole table: `wc` with `-l`/`-w`/`-c`, `head` and `tail` with `-n`, `sort` with `-r` and `-u`, `uniq` with `-c`, `tr` for single-character translation, `cat` reading stdin when given no argument, and `grep` extended with `-v`, `-i`, `-n` and `-c`. `dispatch` grows two lines: a guard arm for `cat` with an argument, and a `_` arm that consults `run_filter` before reporting an unknown command. No new stage type, no new pipe path, no tokenizer. `grep_lines` is deleted rather than kept. It became a one-line wrapper over `grep_matches("", ...)` with no caller outside tests, and plain clippy flagged it against a zero-warning baseline. Its two call sites now call `grep_matches("", ...)` directly — same call, same assertions. Flags are parsed by a shared `split_flags(cmd, args, allowed)`: leading `-` tokens are flags, letters bundle so `-ru` and `-vc` work, the first non-flag token ends them, and the remainder is returned with its spaces intact so `grep two words` keeps its pattern. An unrecognised letter is refused rather than ignored. A lone `-` and a `-` before a digit are not flags, which makes `head -n -3` report a bad line count rather than an unknown option, and lets `grep -` search for a hyphen. `head -n 0`, a negative or non-numeric count, a missing count and a bare `head 3` are all refused with a message naming the command; none silently falls back to ten lines. `sort` terminates every line it emits whether or not the input ended in one, so a downstream `str::lines` sees the same count, and an empty stream yields an empty string rather than a bare newline. `apps/help.rs` gains the filters, the pipeline syntax and the redirection syntax. A feature the handbook does not mention is half-shipped. Verification: registered in-kernel assertions in this module go from 15 to 25, all passing, with all 15 predecessors unchanged, against 0 passed / 12 failed in the host harness before the change. Twenty mutations were applied and nineteen were killed by the in-kernel registry — the layer CI actually runs — including one, `wc` counting words as lines, that the host harness missed entirely. The surviving mutation feeds filters an empty stdin from inside `dispatch`'s four-line `_` arm, which no registered assertion can reach without mounting AHCI; the host harness catches it. An earlier mutation covering argument splitting was registry-blind for the same reason and was made reachable by moving the split out of `dispatch` into `run_filter`. `cargo +nightly clippy --release --target x86_64-unknown-uefi` on this machine, forced by touch: 0 errors / 0 warnings plain and 0 errors / 79 warnings with `--features test-mode`, both matching baseline, none naming either file. Limits: QEMU is not installed on this machine, so the in-kernel run is CI's alone; the harness pulls both shipped files in by absolute `#[path]` and executes the shipped `register_all()`. `tr` translates one character to one character and refuses ranges and character classes loudly rather than translating the first and dropping the rest. `grep -i` allocates a lowercased copy per line. The inherited limits from 8a24f43 are unchanged: no quoting, so `|`, `<` and `>` are metacharacters everywhere; no exit status, so a filter's error text flows downstream as ordinary bytes; no stderr channel. A pattern beginning with `-` is unreachable except as a lone `-`, and `--` is not implemented. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
`relocation_table` computed `rela_size / rela_ent.max(24)` from `DT_RELASZ` with nothing tying it to the segment the table lives in. The loop is not unbounded — `read_u64` refuses the first offset past the end of `elf_data`, so a `DT_RELASZ` of `u64::MAX` on a 16 KiB file stops after 501 iterations with `Err(TooSmall)`. The defect is narrower and worse than a runaway: reads that leave the table while staying inside the file. A ten-entry relocation table in a segment with `p_filesz = 0x100`, declaring `DT_RELASZ = 0x1000`, made the loader apply 170 relocations. The 160 beyond the table were decoded from `.text`, padding and string data, and the load returned `Ok`. `va_to_file_offset` becomes `va_to_file_range` and returns the containing segment's remaining file-backed length alongside the offset, so the bound costs one comparison and no second scan. A `DT_RELASZ` larger than that length is `InvalidSegment`. Both callers are updated. Three unchecked additions of the same class were found while auditing and are fixed: `read_u16`, `read_u32` and `read_u64` each computed `offset + N`, which wraps silently in release and aborts the kernel under `overflow-checks`; `va_to_file_offset` added `p_offset + (va - p_vaddr)` with `p_offset` unbounded; and the `DT_STRTAB + DT_NEEDED` offset added two raw `u64` values. The five empty-path syscall guards this change was also dispatched for already exist. Commit 1eadfc0 added them at table.rs:1067, :1098, :1475, :1497, :1520 and :1529, all returning EINVAL like their three siblings. `syscall/table.rs` is unmodified here, verified with `git diff --quiet`. An empty path was already EINVAL before that commit, because `Vfs::canonicalize_path` opens with `if !path.starts_with('/') { return None; }`; the guards short-circuit before `check_mac`, `find_mount` and the mount lock rather than changing the answer. No shared resolver exists to hold a single guard: every arm calls `copy_path_from_user` inline and then its own `with_vfs` closure. Verification: registered in-kernel assertions in `elf_loader::` go from 14 to 19, all passing, against 16 passed / 2 failed in the host harness before the fix, where the failures record `writes=170 result=Ok(())` and `writes=501 result=Err(TooSmall)`. After the fix both are `writes=0 result=Err(InvalidSegment)`. The harness is built with `overflow-checks = true` so an unchecked addition panics rather than wrapping silently, and routes every relocation write through a stub that asserts at 10,000 writes. Six mutations were applied and all six killed. Four assertions survived their mutations on the first round, for two different reasons, both fixed. Three survived because the harness ran registered tests outside `catch_unwind`, so an overflow panic killed the process without printing a failure line and a kill was indistinguishable from a survival. The fourth survived for a real reason: the probe placed the huge `p_offset` on the relocation segment with `DT_RELA` at its start, making the delta zero so the addition was never exercised, and `map_load_segments` rejects such a `p_offset` itself before relocations run. The only path reaching that addition is `parse_dynamic_link_info` at elf.rs:127, which runs before `map_load_segments` at :146, so the case was rewritten to drive a `DT_NEEDED` name through it. Every other count and size in the file was checked. `e_phnum` is sound because each iteration needs 56 real bytes through `elf_data.get(start..end)?`, so the file length bounds it before the count does. The `e_phentsize` and `e_phoff` arithmetic already used `checked_mul` and `checked_add`. `DT_STRSZ` feeds `elf_data.get`, which returns `None`. The dynamic-section walk strides over `dyn_bytes.len()` and breaks on a short tail. `p_memsz` is bounded against `phys::free_count()` by commit ea6e899. Section headers, `DT_PLTRELSZ`, `DT_SYMTAB` and `DT_SYMENT` are never read. Limits: QEMU is not installed on this machine, so the in-kernel run is CI's alone. Clippy against the real tree could not reach the baseline while a sibling's edit to `apps/shell.rs` was mid-change, so the smith ran a controlled A/B in an isolated crate copy with `shell.rs` pinned at HEAD: this file at HEAD and this file fixed both give 0 errors / 0 warnings plain and 0 errors / 79 warnings test-mode, a zero delta. That copy initially reported 27 errors and 106 warnings on byte-identical sources, because clippy finds `clippy.toml` (`msrv = "1.85"`) by walking ancestors from the package root and a crate copied outside the repo loses it; any future out-of-tree clippy run on seal-os must carry that file. Re-verified in place after the sibling landed: 0/0 and 0/79. `p_filesz` is still not validated against `elf_data.len()`, so the segment bound can be looser than the file, with the per-entry read still stopping at the real file end. The `rela_file_off + i * rela_ent` addition keeps a plain `+` because entry zero reads at `rela_file_off` first and a saturated value fails that read through the now-checked `read_u64`, so a `checked_add` there would be code no mutation could falsify. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
… contract `--check-doc-claim-contract` asserts that the ManifoldPkg install path calls `verify_signature(&pkg, key)`. Commit 8f0693c replaced that function with `verify_package_signature`, because the old preimage covered neither the manifest description nor its dependencies and carried no length separators between fields. The gate went red on the rename while the property it exists to enforce — that nothing is installed without a signature check — held throughout. The needle becomes `verify_package_signature(&pkg, key)`, which is the live call at `pkg/mod.rs:415`. The check is unchanged in strength: deleting the verification still fails it. Verification: `cargo run -- --check-doc-claim-contract` reports `DOC CLAIM CONTRACT OK` on this machine, against `DOC CLAIM CONTRACT FAIL: ManifoldPkg core missing verify_signature(&pkg, key)` before the change. The gate failed the `cargo test --workspace` job of CI run 31478596463 at its `Check README/doc claim contract` step, with the other 14 jobs green. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
…ding it
`rmdir` walks directory data with `while offset < dir_data.len()` and then does
a `read_unaligned` of an 8-byte `DirEntryHeader` at `offset`. Its siblings
`lookup` at ext2.rs:1393 and `readdir` at :1615 both break when
`offset + size_of::<DirEntryHeader>()` exceeds the length. `rmdir` carried
nothing, so a hostile `rec_len` that lands `offset` at `len - 1` reads seven
bytes past the end of the `Vec`. Miri, on a hand-built image:
error: Undefined Behavior: memory access failed: attempting to access
8 bytes, but got alloc58115+0x3ff which is only 1 byte from the end
of the allocation
--> fs/ext2.rs:1724:17
`add_dir_entry` has the same defect on both of its paths, and the second is
worse than surveyed. At :1291 the name slice panics on a lying `rec_len`, but
the `write_unaligned` at :1285 has already written eight bytes past the
allocation by then — corruption first, abort second, in a kernel built with
`panic = "abort"`.
`free_block` and `free_inode` both wrap when handed a block below
`s_first_data_block` or inode 0. The group-size bound keeps the index inside
the bitmap `Vec`, so the result is a foreign group's bitmap corrupted rather
than a write out of bounds. Both now reject the low end, and both also reject
the high end: `free_inode_blocks` feeds `free_block` every `u32` read out of a
disk indirect block, so `u32::MAX` reaches it and does the same damage from the
other direction, for one extra comparison in the same `if`.
Verification: registered in-kernel assertions in this module go from 23 to 25,
all passing, with all 23 predecessors unchanged. The host harness runs 8
assertions natively and all 8 again under `cargo +nightly miri test` with no
undefined behaviour reported, against a pre-fix state where Miri reported the
read above and plain `cargo test` panicked with
`range end index 1025 out of range for slice of length 1024` and
`range start index 1032 out of range for slice of length 1024`. Ten mutations
were applied and all ten killed. Five delete a guard; the other five tighten
one by a single step, because a guard that cannot be over-tightened is a guard
whose boundary was never tested — turning any of the three `>` comparisons into
`>=` fails a positive-control assertion, as does rejecting the first data block
or the last inode of the volume. The file was sha256-verified identical to the
green state after every mutation. `cargo +nightly clippy --release --target
x86_64-unknown-uefi` on this machine, forced by touch: 0 errors / 0 warnings
plain and 0 errors / 79 warnings with `--features test-mode`, neither naming
`fs/ext2.rs`. The diff is 169 insertions and 0 deletions.
The first mutation run produced bad evidence and was redone. `free_block` and
`free_inode` mutations panicked at ext2.rs:1001 on the host's debug overflow
trap rather than on the assertion, which proves the host caught the wrap and
not that the kernel would; seal-os builds release without `overflow-checks`.
The harness now matches that profile, and the assertions fire on their own.
Limits: QEMU is not installed on this machine, so the in-kernel run is CI's
alone; the harness pulls the shipped file in by absolute `#[path]` and executes
`fs::ext2::tests::register_all()`. `dir_inode.i_size += self.block_size` at
:1303 still wraps `u32` and is left with a note naming the precondition:
reaching it requires `checked_dir_size` to pass first, which needs a volume of
at least 4 GiB, and the line before it allocates a `Vec` of that size in a
kernel with no `#[alloc_error_handler]`, so the allocation aborts before the
wrap. Fixing it needs a 4 GiB image fixture to prove, and an unprovable guard
is not worth shipping. `fs::parity` and `fs::ext2_format` both mark bitmap tail
bits used, so no allocator can hand out a value the new bounds reject, and
`free_block` and `free_inode` have no caller outside this file.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Commit d3a144d introduced `wrong_dst` and a guard proving it produces a different checksum from the delivered destination, then left the mirror datagram still built from `local_ip()`. The guard verified a property of a value the assertion did not use, so the test kept failing for its original reason: `local_ip()` is 0.0.0.0 before DHCP, and 0.0.0.0 and 255.255.255.255 both contribute nothing under one's complement addition with end-around carry. CI run 31479738820 reported 454/455 with the same single failure. The mirror datagram now uses `wrong_dst`. Verification: `cargo +nightly clippy --release --target x86_64-unknown-uefi` on this machine, forced by touch, reports 0 errors and 0 warnings on the plain profile. The test-mode profile could not be compiled here because a sibling agent's in-flight edit to `net/tcp.rs` fails at line 2544 with an unresolved name; that file is untouched by this change. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
…TF-8 `parse_eph` decoded both the file path and the manifest with `String::from_utf8_lossy`, so invalid bytes became U+FFFD rather than being refused. `pkg/mod.rs` compensated downstream by rejecting any path containing the replacement character, a proxy standing in for the check that was missing. The manifest decode is the worse of the two and was not surveyed. Every field it yields — name, version, description and dependencies — feeds `signature_preimage`, so two different wire manifests that differ only in invalid bytes collapsed to the same preimage and one signature covered both. That is a collision in the scheme 8f0693c introduced to remove exactly this class of ambiguity. Both decodes now use `core::str::from_utf8` and return `BadPath` or `BadManifest`. `pub fn verify_signature` is deleted rather than delegated. It had zero callers and built the old preimage — no domain tag, no length separators, and neither description nor dependencies — so leaving it public left the trap that the next person needing a signature check reaches for the name that reads like the obvious one. A delegating wrapper would be an unreferenced interface with one implementation whose only purpose is to be that name. The module doc now records where verification lives and what the deleted preimage omitted. Deleting it left a mutation with nothing to catch it: no gate read `format.rs` at all, so the weak verifier could be reintroduced silently. `check_manifoldpkg_shell_contract` now reads that file and fails on the literal `fn verify_signature`. `test_unsafe_paths_refused` in `pkg/mod.rs` required every hostile path to be refused by the installer with a message beginning `unsafe path`. Refusing invalid UTF-8 at the parser means one of its eleven cases is now rejected a layer earlier, so it accepts `parse error: BadPath` as well. The package is still refused and still installs nothing; only which layer says so moved. The other ten cases are unchanged and still reach the installer. Verification: registered assertions in `pkg::format` go from 7 to 9, all passing, against 7 passed / 2 failed before the fix. Four mutations were applied and three killed: restoring either lossy decode fails its named assertion, and a proxy implementation that decodes lossily and then rejects U+FFFD fails `non_utf8_path_rejected` on the control that a valid UTF-8 path containing a genuine U+FFFD must still parse. The fourth — reinstating the weak verifier — survived, which is what prompted the new gate check; it now fails with `pkg/format.rs reintroduces fn verify_signature`. `--check-doc-claim-contract` reports `DOC CLAIM CONTRACT OK` and `cargo test` in `kernel/seal-mkimage` reports 76 passed, 0 failed. That suite had one failure before this change, introduced by 3f4b352: the needle was updated to `verify_package_signature` while the test's own fixture string at main.rs:6967 kept the old name, so the gate's self-test checked a string the gate no longer looked for. The fixture is corrected here. Limits: QEMU is not installed on this machine, so the in-kernel run is CI's alone; the host harness pulls the shipped file in by absolute `#[path]`. Clippy was measured as an A/B against `git show HEAD:pkg/format.rs` with sibling state held constant, giving a delta of exactly zero in both profiles with no warning naming `pkg/format.rs`; the absolute counts could not be taken because a sibling's uncommitted `net/tcp.rs` fails to compile at line 1019, where `port >= EPHEMERAL_PORT_MAX` compares against that type's maximum and is always true. `docs/CRYPTO_AUDIT.md:160-177` still presents the deleted weak verifier as the live scheme; it documented the weak preimage while `pkg/mod.rs` ran the strong one even before this change, and no gate reads it. The U+FFFD check in `pkg/mod.rs` is kept as defence in depth, though its justification comment now describes a decode that no longer exists. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
…ff the end
`NEXT_TCP_PORT` starts at 40000 and both `socket()` and `poll()` advanced it
with a bare `*p += 1`. Allocation 25,536 is the last that fits; the next
computes `65535 + 1`, which is 0 in release and an abort under
`overflow-checks`. The counter then walks up from zero through the well-known
range, handing 22, 80 and 443 to outgoing connections. It does not wrap to the
floor of the ephemeral range, because nothing named a floor.
The allocation in `poll()` was dead: `TcpSocket::new(new_port)` was immediately
followed by `new_sock.local_port = dst_port`, discarding the port. The counter
moved anyway, once per SYN a remote peer sent, so the overflow was reachable
from the network with no local socket involved. That allocation is deleted,
which is the root-cause half of this change.
Nothing prevented a duplicate either, and that does not need the overflow to
bite. `TCP_SOCKETS` is a plain `Vec` with no uniqueness, `TCP_FLOW_INDEX` keys
on the four-tuple so two sockets on one local port with different peers are two
valid entries, and `TCP_LISTENER_INDEX::insert` overwrites on a repeated
`local_port`, so a second listener silently takes the first one's traffic. The
only code in the file that ever asked whether a port was free was
`packet_fixture_proof`'s own search, and `alloc_ephemeral_port` now uses the
same predicate rather than a second one that could disagree.
Allocation wraps inside `EPHEMERAL_PORT_MIN..=EPHEMERAL_PORT_MAX`, skips ports
a live socket holds, and returns `None` after a full pass rather than looping
or duplicating. Exhaustion returns `TCP_SOCKET_NONE`, which indexes nothing:
every entry point resolves through `get`/`get_mut` and no-ops, and `state()`
reports `Closed`. `drivers/net/http.rs:93` therefore times out and returns
`Err("TCP connect timeout")` rather than writing into a stranger's socket.
Verification: registered in-kernel assertions in this module go from 17 to 21,
all passing, against 17 passed / 4 failed before the fix. Nine mutations were
applied and eight killed, including all four boundary shifts — the assertions
carry literal port numbers rather than the constants, so moving either end of
the range by one fails them. The ninth, shortening the search bound by one
iteration, survives and is not papered over: it differs only when exactly one
port is free and it sits immediately behind the counter, and it fails closed by
refusing one port early rather than handing out a duplicate. Killing it needs
the full-range test that was rejected on cost. Both CI benchmarks hold:
`[BENCH] tcp-packet-demux ok=1 rx_bytes=4` and `[BENCH] tcp-roundtrip
established=8 server_rx=512 result=pass`. `cargo +nightly clippy --release
--target x86_64-unknown-uefi` on this machine, forced by touch: 0 errors / 0
warnings plain and 0 errors / 79 warnings with `--features test-mode`, none
naming `net/tcp.rs`. Clippy rejected the first version of the wrap comparison
as `absurd_extreme_comparisons`, since the ceiling is `u16::MAX`; it was
changed to `==` rather than silenced.
Limits: QEMU is not installed on this machine, so the in-kernel run is CI's
alone; the host harness pulls the shipped file in by absolute `#[path]` and is
built with `overflow-checks = false` to match the seal-os release profile.
Full-range exhaustion is proved only on the host — the in-use test is a linear
scan, so filling 25,536 ports costs its square, 326 million comparisons, which
is 101 ms natively and seconds under QEMU's interpreter. The registered
assertion walks a 512-port run instead and proves the skip lands on the first
free port. `close()` never removes a socket from `TCP_SOCKETS`, so a port is
held for the life of the machine once used; that is what makes exhaustion
reachable after 25,536 opens and is left for its own change. `socket()` would
be better typed `-> Option<usize>` than returning a sentinel — `drivers/net/tcp.rs:20`
already stores an `Option<usize>` and needs one token — but `net/ipv4.rs:656`,
`net/ipv4.rs:752` and `net/ipv6.rs:886` also call it and are outside this scope.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
The shell had no way to name a value. `NAME=value` now assigns, `$NAME` and
`${NAME}` expand in arguments, `export` marks a variable, `unset` removes one,
`env` lists the exported set and bare `set` lists all of them, both sorted by
the `BTreeMap` they live in so two runs print identical lines.
Five decisions shape the result and each is asserted rather than left to fall
out.
Expansion happens after the pipeline split, per stage, so `parse_line` and
`parse_stage` never see a value. A value holding `|`, `<` or `>` arrives after
the only place those read as operators and stays an argument. Expanding first
would make `V=a|b` turn `grep $V` into two stages, and with no quoting there
would be no way to ask for the literal.
An assignment is a whole statement and a trailing command is refused, as is a
value containing whitespace. Without quoting, `A=1 look` cannot be distinguished
from a value with a space in it, and the two readings do opposite things. That
refusal also buys the property the expander relies on: no value holds a space,
so `$NAME` always expands to exactly one argument and expansion can never change
how `dispatch`'s `splitn(3, ' ')` cuts the line.
Redirect targets expand, because `OUT=hits.txt` then `> $OUT` is half the point,
and the expanded string is the same one `deny()` and `abs_path_in` validate and
the filesystem opens. An empty expansion is refused: before this change
`peek note.txt > $GONE` silently created a file named `$GONE`.
Expansion is one pass. Substituted text is copied out and never rescanned, and
an assignment expands its right-hand side once at assignment time, so `A=$B`
with `B=$A` cannot store a live reference. The store caps at 64 variables and
4096 bytes of names and values together, refusing past either rather than
evicting, since a vanished variable would make a later `$NAME` expand to empty
and read as a wrong answer instead of a full store.
`$?` is not invented. This shell has no exit status, and a `$` with no name
after it stays a literal `$`, so `$?`, `$5` and `cost $` come out as themselves.
Verification: registered in-kernel assertions in this module go from 25 to 34,
all passing, with all 25 predecessors unchanged, against 0 passed / 11 failed
in the host harness before the change. Thirty-four mutations were applied and
all thirty-four killed. `cargo +nightly clippy --release --target
x86_64-unknown-uefi` on this machine, forced by touch: 0 errors / 0 warnings
plain and 0 errors / 79 warnings with `--features test-mode`, neither naming
`apps/shell.rs` or `apps/help.rs`.
Three of the new assertions survived their mutations on the first pass and all
three were substring accidents in the handbook checks: `contains("export")` was
satisfied by the word `exported` on the `env` line, `contains("NAME=value")` by
a parenthetical on the `export` line, and the `set` page check only verified
that help existed rather than that it described the listing. Each token now
belongs to exactly one line and the `set` check names what the page must say.
Limits: QEMU is not installed on this machine, so the in-kernel run is CI's
alone; the harness pulls both shipped files in by absolute `#[path]` and
executes the shipped `register_all()`. Four mutations are killed only by the
host harness and not by the registry CI runs: expanding before the split,
treating an assignment as a non-statement, leaving the redirect target
unexpanded, and dropping the `set` listing arm. All four live in
`Shell::run_line` and `Shell::dispatch` behind `&mut self`, which no registered
assertion can construct without mounting AHCI. What the registry proves is the
composition those decisions are built from — that `parse_line` yields two
stages, that `expand_vars` on the second yields `grep a|b`, and that
`expand_required` refuses an empty result — not the wiring itself. Making
`run_line` a free function over its inputs and an output callback would close
that, and is a rewrite of its I/O calls rather than part of this change. The
export mark is a mark and nothing more: no command receives an environment,
because Seal OS commands are `Shell` methods rather than processes, and there
is no address space to fill until `run` or `install` spawns a real task. The
no-whitespace-value rule sits under the quoting ceiling recorded in 8a24f43 and
is documented in the `help variables` page rather than left to be discovered.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
…ee self-caught tests
The README stopped at 379 registered assertions and three fixes. A new section
covers the run to 455 and what moved it: not 91 new tests, but nine test groups
already present in the tree that had never executed, because `kernel/seal-os`
sits in the workspace `exclude` list so `cargo test --workspace` never reaches
it and every `#[test]` inside compiles to nothing. TCP held seventeen of them
and four were broken, which is how their never having run is provable.
The section records the remote defect found while bounding the ephemeral port
allocator: the allocation inside `poll()` was dead, because the port it
computed was overwritten with the packet's destination port on the next line,
but the counter still advanced once per SYN from any peer. It documents that
the wrap lands on zero rather than the floor of the ephemeral range, and that
the counter then walks up through the well-known ports.
Three assertions that the variables agent caught surviving their own mutations
are quoted in full, because all three are substring accidents in handbook
checks — `contains("export")` satisfied by the word `exported` on a different
line, `contains("NAME=value")` by a parenthetical, and a help-page check that
only verified the page was not the not-found string. Two of the three stay
green with the feature deleted from the handbook.
The section closes on the `transport_checksum_uses_the_delivered_destination`
failure and states plainly that the first fix for it was also wrong: it
introduced a distinguishable address and a guard comparing checksums, then left
the mirror datagram built from `local_ip()`, so the guard proved a property of
a value the assertion never used.
The file grows from 6,254 to 6,381 lines, counted with `wc -l` before and after
on this machine. The 455/455 figure is from CI run 31480589284, which reports
`Suite All Registered Tests: 455/455 passed, 0 failed, 0 panicked` followed by
`ALL TESTS PASSED`.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
`docs/CRYPTO_AUDIT.md` described a system that no longer exists in several places and had never described one that did in others. Section 3.2 documented `format::verify_signature` as the package signature scheme. That function was deleted in d86e1c2, and its preimage had never been the installer's — the installer's is at `pkg/mod.rs:297-318`. Section 1 opened by calling the TLS stack PSK-only with no X.509 and no ECDHE, which `tls.rs:173-180`, `tls.rs:216-227` and `x509.rs:593` all contradict; PSK is the fallback at `tls.rs:228-231`. Section 1.3 called the HKDF implementation non-compliant with RFC 5869, but `tls.rs:535-562` implements it and `tls.rs:713-748` carries RFC 4231 and RFC 5869 vectors. Three of the seven limitations in section 4 were superseded by the same three subsystems. The rewrite carries a file and line for every claim, and quotes no Rust at all, because the quoted blocks are what drifted while the citations stayed correct. Section 3.2 now records the real preimage byte by byte — the `EPHSIG1\0` domain tag at `pkg/mod.rs:42`, a `u32be` length before every field, a count before every section — and says why `carrier` and `voronoi_cell` are excluded (`format.rs:167` hardcodes them). A new limit is recorded that nobody had written down: the signature covers parsed fields rather than manifest bytes (`format.rs:152-163`), so two wire manifests that parse identically share one signature. That is inert today and stated anyway. A new section 6 lists what this revision did not verify: no kernel was booted, so the RFC vector tests registered at `testing/runner.rs:61` are present but their result was not observed; dependencies were not audited; key provenance could not be settled from source. Ten code defects were found while reading and none are fixed here, since this is a documentation change. Two are load-bearing. `drivers/net/tls.rs` performs no CertificateVerify — grep finds the term only in test-vector literals — so chain validation at `tls_socket.rs:118-123` proves that a valid chain was shown rather than that the peer holds its key, and a chain is public data. There is no Finished message and no transcript hash either, so a modified ServerHello leaves no trace. Separately, `SEAL_PKG_PUBLIC_KEY` at `pkg/mod.rs:26-29` has no signer anywhere in the tree: the Ed25519 public key of the all-zero seed shares its first sixteen bytes and differs in the last sixteen, and the constant does decompress to a curve point, so `VerifyingKey::from_bytes` succeeds and every verification against it then fails. Registry installs at `pkg/mod.rs:460-477` cannot succeed with any package this repository can produce. The other eight are recorded in the document: empty AAD at `tls.rs:296` and `:321` where RFC 8446 5.2 binds the record header, a `u16` record-length truncation at `tls.rs:381` reachable from `tls_socket.rs:129-136`, `matches_dns` at `x509.rs:507-509` having no production caller because `TlsSocket::connect` takes an `IpAddr`, a rollback floor at `pkg/channel.rs:215` that resets to zero every boot, `EphError::HashMismatch` never being constructed, local `.eph` installs passing no key at `apps/shell.rs:1623`, and a doc comment at `pkg/mod.rs:346-349` that still describes the lossy path decode d86e1c2 replaced. Verification: `--check-doc-claim-contract` reports `DOC CLAIM CONTRACT OK` before and after, and no `.rs` file is touched. Every table row was checked against the line it cites. Limits: line numbers are pinned to 2b113d7 and `apps/shell.rs` is under active change, so that row cites `cmd_install` as well as its number. `certs.rs` fixtures were not re-derived and `cargo audit` was not run. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
The shell could compose commands on one line but could not run a file of them.
`source <path>` and its `.` alias now read a file from the VFS and run each line
through the existing `run_line`, in the current shell, so assignments and
exports a script makes persist after it finishes. `#` starts a comment, blank
lines are skipped, and `echo` is added because a script with no way to print is
a script nobody can debug.
Comments are cut first, at the top of `run_line`, before the assignment test,
before the `|` split, and long before expansion. A `#` opens a comment only
where a word opens — at the start of a line or after whitespace — because with
no quoting, cutting at every `#` would silently shorten `A=v#1` to `A=v` with no
way to ask for the character back. Cutting before expansion means a `#` arriving
from a variable is text rather than a comment that retroactively truncates the
line, which is asserted both through the `strip_comment` → `expand_vars` →
`run_filter` chain and end to end.
`MAX_SOURCE_DEPTH` is 8. The wall is the kernel stack rather than the heap:
each level stacks `run_line` → `run_pipeline` → `dispatch` → `cmd_source` →
`run_script`. `MAX_SCRIPT_BYTES` is `PIPE_CAPACITY`, 65536, since a script is
read whole into the heap exactly as `< file` is, and `MAX_SCRIPT_LINES` is 1024
separately, because a file of blank lines is cheap in bytes and still walks
`run_line` once per line. Exceeding either refuses the whole script rather than
running part of it — half a script is a different script, and the operator
cannot tell which half ran.
A script stops when `run_line` returns `Err`, meaning the line could not run at
all: a syntax error, an unclosed `${`, a name expanding to nothing, a refused
redirect, an over-capacity pipe. It continues when a line ran and printed
something, including `peek: 'x' not found`, because `dispatch` returns a
`String` whether it succeeded or failed and the shell has no way to tell those
apart. Sniffing for the `seal: ` prefix was rejected: `seal: unknown command`
is ordinary `dispatch` output, so that rule would stop on a typo and not on a
real failure. No exit status is invented and no dispatch arm is touched.
Verification: registered in-kernel assertions in this module go from 34 to 41,
all passing, with all 34 predecessors unchanged, against 0 passed / 10 failed
in the host harness before the change. Twenty-three mutations were applied with
the file restored byte-exact between each and all twenty-three killed. Five are
killed only by the host harness, and all five are the `&mut self` parts:
`run_line`'s cut order and blank-line skip, the `.` alias arm in `dispatch`, and
`cmd_source`'s depth bookkeeping, missing-file message and same-shell property.
Everything bounded, parsed, numbered or documented is killed by the registry
that CI runs. `cargo +nightly clippy --release --target x86_64-unknown-uefi` on
this machine, forced by touch: 0 errors in both profiles with no diagnostic
naming `apps/shell.rs` or `apps/help.rs`.
The first draft of the depth assertion compared against `MAX_SOURCE_DEPTH`
symbolically, so changing the constant to 64 would have left it green. It is
pinned to the literal 8 instead, next to the handbook assertion that prints the
same number, so the documented bound cannot drift from the enforced one.
Handbook tokens are checked with
`book.lines().filter(|l| l.contains(token)).count() == 1`, so a token matching
two lines fails — a guard added because three assertions in 3e6ab2f passed on
substrings belonging to a different line, and a mutation here confirms it bites.
Limits: QEMU is not installed on this machine, so the in-kernel run is CI's
alone; the harness pulls both shipped files in by absolute `#[path]`. A script
that sources a script that fails keeps going, because `cmd_source` returns the
stopped script's message as ordinary output through a `dispatch` that returns
`String`; the fix is the exit status `run_line` already names as its ceiling.
Each script is capped but the accumulated output of nested scripts is not, the
same shape as `run_pipeline`'s last stage. Without quoting the shell cannot
write a file containing a literal `#` except by routing the character through a
variable, which is how the harness builds its commented fixture and doubles as
the ordering proof.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
`TCP_SOCKETS` was a `Vec` that only grew. `close()` changed a socket's state
and removed nothing, and `alloc_ephemeral_port` skips any port a socket in that
table holds, so every port used was held for the life of the machine.
The state the item named was not the state that mattered. `TimeWait` was
terminal: its arm carries a comment saying the socket should remain there for
2*MSL and no timer anywhere ever leaves it. An active close goes `FinWait1` to
`TimeWait` and stops, so reaping `Closed` alone would not have touched the path
that leaks. This adds the 2MSL timer — `TIME_WAIT_TICKS` of 60,000 on the
roughly 1 kHz tick counter, an MSL of 30 seconds as BSD and Linux use — and
reaps `TimeWait` only past it. Reaping it on sight was rejected: RFC 793 holds
the four-tuple so a delayed duplicate cannot be read as a new connection, and
collecting it early is a correctness regression rather than a cleanup.
`Closed` alone is also not enough to reap. `socket()` hands out a `Closed`
socket with `remote_port == 0`, so reaping on state alone takes the table entry
out from under a caller standing between `socket()` and `connect()`. And
`abort()` promises the received bytes stay readable, which
`drivers/net/http.rs:117-127` relies on by draining after it observes `Closed`.
A socket is collected only when it is `Closed`, has a peer, and its receive
buffer is empty.
Removing from a `Vec` was not an option. Six classes of holder store an index:
`drivers/net/tcp.rs:10`, five call sites across `net/ipv4.rs` and
`net/ipv6.rs`, both demux indexes, `pending_accept`, and the two benchmark
fixtures that address sockets positionally. `remove` or `swap_remove` repoints
all six. `TCP_SOCKETS` is now a slot map: `SocketSlot { sock: Option<TcpSocket>,
generation }`, where a slot is emptied in place and never moves. The handle
stays a `usize` but stops being an index — the low half is the slot and the
high half the generation, and `resolve` returns a slot only when it is occupied
and the generation matches. A tombstone alone would leave the table growing one
slot per socket ever opened, which is the defect; reuse without a generation
would let a stale handle read whatever took its slot. The generation counter is
global rather than per slot because `cleanup_tcp_fixture` truncates, and a
per-slot counter would be dropped with the slot and could repeat a generation a
live handle still holds.
`free_slot` also removes the socket from both demux indexes. Those key on slot
across 256 buckets, so a leaked entry holds a bucket forever: after 256
finished connections `insert` refuses and a new connection is not demuxed at
all.
Part 2 of the item is superseded rather than done. The handle is no longer a
raw index, `TCP_SOCKET_NONE` is a genuine null key whose slot half exceeds any
table `insert_socket` will mint, and it still fails closed through `resolve`.
Changing four callers to `Option<usize>` would buy no behaviour, so
`net/ipv4.rs`, `net/ipv6.rs` and `drivers/net/tcp.rs` are byte-identical to
HEAD.
Verification: registered in-kernel assertions in this module go from 21 to 26,
all passing, with all 21 predecessors unchanged, against 21 passed / 2 failed
with the new assertions on the old code. Sixteen mutations were applied and all
sixteen killed, including reaping `TimeWait` immediately, never leaving it,
ending the hold one tick early or late, shortening it to 5 ticks, reaping any
`Closed` socket, dropping the receive-buffer guard, reaping without repairing
the indexes, keeping a generation across a free, ignoring the generation in
`resolve`, and reusing a slot without incrementing it. Both CI benchmarks are
unmoved: `[BENCH] tcp-packet-demux ok=1 rx_bytes=4 cleanup=ok` and
`[BENCH] tcp-roundtrip established=8 server_rx=512 cleanup=ok result=pass`.
`cargo +nightly clippy --release --target x86_64-unknown-uefi` on this machine,
forced by touch: 0 errors / 0 warnings plain, 0 errors in test-mode, with no
warning naming `net/tcp.rs`.
One mutation initially survived and the harness was changed rather than the
test: with a zero clock, a `TimeWait` entry that records no timestamp is
indistinguishable from a fresh one. The harness clock now starts at 1,234,567
and the mutation dies.
Limits: QEMU is not installed on this machine, so the in-kernel run is CI's
alone; the harness pulls the shipped file in by absolute `#[path]` with
`overflow-checks = false` in both profiles. The generation wraps after 2^32
sockets on a 64-bit target, roughly 50 days at one per millisecond, after which
a handle that old aliases again. Free slots are found by linear scan, the same
scan the port allocator already performs. The table settles at peak concurrent
sockets and never shrinks. A `SynSent` socket nobody answers still leaks: it
retransmits at the capped RTO forever and holds its port, and
`http::get_http` returns a timeout without closing — the fix is a SYN retry
limit that aborts, after which this sweep collects it. A `Closed` socket with
bytes nobody reads is held until drained or closed, deliberately, since the
alternative is losing an HTTP body. `pending_accept` entries for reaped sockets
stay queued until popped, after which `accept` returns a handle reporting
`Closed`. `drivers/net/tcp.rs` has no `Drop`, so an abandoned value never
closes its handle; adding one would change behaviour for `tls_socket.rs` too.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
`--check-o1-network` requires `lookup_exact_flow_index` and `lookup_listener_index` to validate a candidate socket by direct index rather than by scanning, and enforced it by requiring the literal `.get(idx)` in each body. Commit 36e389f made `TCP_SOCKETS` a slot map, so both bodies now call `slot_sock(sockets, idx)`, which is `sockets.get(slot).and_then(...)` — the same direct index, one call deep. The gate went red on the indirection while the property it exists to enforce held, failing the QEMU UEFI boot smoke test of CI run on 36e389f. Both checks now accept either shape. The indirection is not taken on trust: `slot_sock` is itself checked to contain `sockets.get(slot)` and to contain no `iter()`, `for` or `while`, so a future edit cannot turn the helper every demux lookup validates through into a scan. That is a check the gate did not have before, because before there was nothing between the lookup and the table. Verification: `cargo run -- --check-o1-network` reports `O(1) NETWORK OK` on this machine against `O(1) NETWORK FAIL: lookup_exact_flow_index must use bounded index lookup plus direct socket-index validation` before the change, and `cargo test` in `kernel/seal-mkimage` reports 76 passed, 0 failed. The existing rejection of `sockets.iter()` and `for sock in` in both lookup bodies is unchanged. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
… showed `tls_socket.rs` validated a certificate chain against the embedded trust anchor and set `connected = true`. No CertificateVerify message existed anywhere in either file — grep for the term or handshake type 0x0f finds only the word "transcript" in a doc comment and the byte 0x0f inside an RFC 5869 test vector. A certificate chain is public data, so replaying an observed one passed that check. There was no Finished either, and `tls.rs:247-248` derived the handshake traffic secrets over the client and server randoms alone, so a modified ServerHello left no trace and the ServerHello parser skipped the cipher suite without reading it. A running SHA-256 transcript now covers ClientHello, ServerHello, Certificate, CertificateVerify and Finished. Handshake secrets derive over `Transcript-Hash(ClientHello..ServerHello)` per RFC 8446 7.1 rather than over the randoms, and a ServerHello selecting anything but 0x1301 is refused. `handle_certificate_verify` builds the RFC 8446 4.4.3 content — 64 bytes of 0x20, the context string, a zero byte, the transcript hash — and `handle_finished` verifies the 4.4.4 MAC under `HKDF-Expand-Label(shts, "finished", "", 32)` with a constant-time compare. Only Finished sets `authenticated`, and `encrypt` and `decrypt` refuse until it does. An unknown handshake type inside the authentication window is refused rather than skipped, because skipping desynchronises the transcript silently. CertificateVerify accepts only `ed25519` (0x0807). That is not a simplification: `x509.rs` verifies Ed25519 and nothing else, enforced independently at :321, :347 and :374. A peer offering RSA or ECDSA already fails chain validation for the same reason, so refusing its CertificateVerify loses no reachable peer. The ClientHello now advertises `signature_algorithms` containing only ed25519, so the offer matches what can be verified. `TlsSocket::set_require_peer_auth` and the `require_peer_auth` field are deleted. They had no callers and were the permissive path — a switch that turned authentication off is the defect, not a mitigation for it. Verification: assertions go from 32 to 51, all passing, against 33 passed / 4 failed with the new ones on the old code. Published vectors are used throughout: RFC 8032 7.1 TEST 2 for Ed25519 in both directions, the RFC 8446 4.4.3 content string pinned octet by octet, and the existing RFC 4231 and RFC 5869 vectors still pass. The strongest control is `socket::psk_finished_completes`, where the harness computes the RFC 8446 7.1 schedule and the 4.4.4 MAC with its own independent code, so agreement means the kernel matches the specification rather than matching itself. Ten mutations were applied and all ten killed: deleting the signature check, verifying over a constant, accepting an empty signature, authenticating on CertificateVerify alone, dropping the socket gate, accepting any cipher suite, and omitting each of the three handshake messages from the transcript. `cargo +nightly clippy --release --target x86_64-unknown-uefi` on this machine, forced by touch: 0 errors / 0 warnings plain and 0 errors / 79 warnings test-mode, matching baseline; the three warnings naming `tls.rs` are the pre-existing `if let Err(_) =` patterns inside existing tests, verified against `git show HEAD`. One mutation survived the first pass and exposed a real hole rather than a weak test. Dropping the Certificate message from the transcript passed 51 of 51, because nothing proved a CertificateVerify was bound to *which* certificate the peer sent, so a signature from a handshake using one chain form could replay into a handshake using another. `certificate_verify_is_bound_to_the_certificate_message` now runs two handshakes identical except that one sends `[LEAF, INTERMEDIATE]` and the other `[LEAF, INTERMEDIATE, ROOT_CA]` — both validate to the same leaf key and differ only in transcript — and requires the CertificateVerify from one to be refused by the other. Limits: QEMU is not installed on this machine, so the in-kernel run is CI's alone; the harness pulls both shipped files in by absolute `#[path]`. The peer is authenticated as some holder of a certificate the trust store issued, not as a particular name: `connect` takes an `IpAddr` and never sees a hostname, and binding it would mean passing one and requiring `x509::Certificate::matches_dns` on the leaf, which `x509.rs` already implements and tests. Certificate, CertificateVerify and Finished are still read as plaintext handshake records with no EncryptedExtensions and no client Finished, so this does not interoperate with a stock TLS 1.3 server — that was true before this change and the module doc now says so instead of listing two deviations that were wrong. What changed is that a handshake it does complete is now authenticated. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
…s bucket
`is_finished` has two arms — `Closed` with a peer and a drained buffer, and
`TimeWait` past 2MSL — and `_ => false` swallows `SynSent`. Nothing moves a
socket out of `SynSent` except an inbound SYN-ACK or an acceptable reset, and a
silent host sends neither. `retransmit_expired` backs the RTO off to
`RTO_MAX`, which is 64,000 ticks, and then retransmits at that rate forever
while `alloc_ephemeral_port` skips the port it holds. Both callers confirm
nothing cleans up: `http.rs:93` and `tls_socket.rs:78` spin until their own
3000-tick deadline, return `Err("TCP connect timeout")`, and drop a wrapper with
no `Drop` impl that never calls `close`.
`SynReceived` leaks identically and worse. `poll` builds an accepted socket per
inbound SYN and sends a SYN-ACK, and the same `_ => false` catches it, so a
peer that half-opens and walks away costs one table slot and one of the flow
index's 256 buckets per SYN with no local socket involved at all.
Both are now bounded by `SYN_RETRIES`, six, counted per handshake in
`TcpSocket::syn_retries` and raised only when an expiry fires in `SynSent` or
`SynReceived`, where the retransmit queue holds the handshake's own segment and
nothing else. Attempts land at 1, 3, 7, 15, 31 and 63 seconds; the seventh
expiry aborts instead of retrying, at 127 seconds — the same wall clock Linux
reaches from the same `tcp_syn_retries` default. Counting expiries rather than
polls matters: the poll rate is the caller's business, not the protocol's. The
aborted socket becomes `Closed` and the existing sweep reaps it, so
`state(handle)` returns `Closed`, both callers' loop conditions stay true, and
neither file needed a change.
Fixing that exposed a hole in 36e389f. A socket that aborts is `Closed`, and
`tcp_flow_key` treats a `Closed` socket as unkeyable, so `free_slot`'s
`remove_exact_flow_socket` was a no-op and the bucket leaked even though the
slot was returned. The reset path escaped it only because `handle_tcp_packet`
refreshes the index first; `poll` did not. `poll` now refreshes with the slot
from `enumerate()` before the sweep runs.
Verification: registered in-kernel assertions in this module go from 26 to 29,
all passing, with all 26 predecessors unchanged, against 26 passed / 3 failed
with the new assertions on the old code. Sixteen mutations were applied and all
sixteen killed, including shifting the limit by one in each direction, setting
it to 1, counting in every state rather than the two handshake states, bounding
only one of the two, counting polls instead of retransmissions, stopping the
retransmit without aborting, aborting without returning the index entry,
letting a second `connect` inherit spent retries, and halving `RTO_MAX`. Both
CI benchmarks are unmoved — `[BENCH] tcp-packet-demux ok=1 rx_bytes=4
cleanup=ok` and `[BENCH] tcp-roundtrip established=8 server_rx=512 cleanup=ok
result=pass` — and `--check-o1-network` reports `O(1) NETWORK OK`.
`cargo +nightly clippy --release --target x86_64-unknown-uefi` on this machine,
forced by touch: 0 errors / 0 warnings plain and 0 errors / 79 warnings
test-mode, none naming `net/tcp.rs`.
Two of the new assertions survived their own mutations on the first pass. The
poll-counting mutation had nothing to kill it until a control was added proving
twenty polls before any expiry cost nothing. The wrong-slot mutation survived
because the churn ran a single socket that always occupied slot 0; the churn now
anchors slot 0 with a live unconnected socket so every abandoned attempt sits at
slot 1 and the refresh must use its own slot.
Limits: QEMU is not installed on this machine, so the in-kernel run is CI's
alone; the harness pulls the shipped file in by absolute `#[path]` with
`overflow-checks = false` and a clock starting at 1,234,567.
`listener.pending_accept` still grows without bound under a SYN flood: reaping
the half-open socket returns its slot and its bucket, but the stale handle stays
on the listener's queue at 8 bytes per SYN and the listener may never be closed.
This change makes that strictly better and never worse, and generation-stamped
handles mean the stale entry cannot alias a later socket, but pruning listener
queues is a different shape of fix and is left as its own item. `SYN_RETRIES`
is fixed at 6 with no per-socket override; a caller wanting a shorter deadline
sets its own, as `http.rs` already does.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
…e downgrade window
`ReleaseChannel::new` set `accepted_index_version: 0` and held the rollback
floor in a struct field alone — read at channel.rs:239, written at :245, never
touching disk. A floor exists to stop an attacker replaying an old, validly
signed index with a known vulnerability. A floor that resets on reboot stops
nothing an attacker can wait out.
The floor now lives at `/packages/.channel_floor` through the same `with_vfs`
path `ManifoldPkg::install_file` already uses, rather than a second persistence
mechanism. The record is a fixed 80 bytes — magic `EPHFLR1\0`, the floor as
big-endian u64, and an Ed25519 signature over the first 16 under a key separate
from both the index and package keys. Fixed width means a short read is a
refusal and a rewrite cannot leave a stale tail.
A missing record accepts, and a corrupt one refuses everything. Those are
opposite answers to the same question and both are deliberate. A fresh system
has never established a floor, and the only thing that creates the record is a
first accept, so refusing on absence would leave the channel permanently dead
with nothing to downgrade below. A record that is present but short, misframed
or wrongly signed is different: treating it as zero turns one flipped byte into
"the floor is gone", which is the attack rather than the mitigation. That case
returns `FloorUnavailable` and refuses even a newer index; recovery is an
operator deleting the file.
The forward-only guard lives in the store rather than at the call site:
`persist_floor` re-reads and treats anything not strictly higher as a no-op, so
no future caller can lower it, not only the one caller that exists today.
Fixture and proof channels opt out through a new `ReleaseChannel::ephemeral`.
The boot proof deliberately replays index v2 after v3 to demonstrate rollback
refusal, so a fixture sharing the real persisted floor would poison it and turn
`result=pass` into `result=fail` on the second boot. `ReleaseChannel::new`, the
network-facing constructor, is the persistent one, so the default is the safe
one.
Verification: assertions in this module go from 17 to 23, all passing, against
17 passed / 3 failed before the fix. The central assertion is the attack: a
floor is written, the channel is dropped and rebuilt from nothing, and a
package below the floor is refused with `IndexRollback { accepted: 9, offered:
8 }` with the package count unchanged. Six mutations were applied and five
killed — dropping persistence fails five assertions, letting the floor move
backward fails one, and the boundary is pinned in both directions so accepting
a package exactly at the floor and refusing the first one above it each fail.
Treating a corrupt record as zero fails `forged_floor_refused`, and pointing the
fixtures at the persistent constructor fails six. The boot proof line is
byte-identical to the pristine one across two consecutive boots on the same
disk, `--check-doc-claim-contract` reports OK, and clippy was pinned by an A/B
against `git show HEAD:channel.rs` restored in place, giving an identical
warning set with none naming this file.
One mutation survived and is reported rather than papered over: swallowing a
failed floor write with `let _ =` instead of `?`. That branch is only reachable
when the VFS write itself fails, and no fault-injection seam exists in the VFS
to reach it. The `?` is kept because it fails in the safe direction, but it is
untested.
Limits: QEMU is not installed on this machine, so the in-kernel run is CI's
alone; the harness pulls the shipped file in by absolute `#[path]`. Nothing in
the kernel constructs a network-facing channel yet, so the persistent floor has
capability but no production caller, and `measure()` must stay on `ephemeral`
or the proof goes red on the second boot. The record key ships in the boot
image, so validation stops an attacker who can write the data partition without
reading the ESP, not one who has both. Signing cannot stop deletion or replay of
an older record the kernel itself signed, and both land on "no floor", which is
the accept direction; closing that needs monotonic storage this kernel does not
have, such as a TPM NV counter or a UEFI authenticated variable.
`docs/CRYPTO_AUDIT.md:416-418` and its L12 entry at :463 now describe the old
in-memory behaviour and need updating.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
…holes `check_file_permission` has three paths that return true without consulting a rule: `mac.rs:110` short-circuits for uid 0, `mac.rs:117` allows everything when no policy is loaded, and `mac.rs:141` falls off the end of the rule walk and allows anything uncovered. It is a lookup table with holes, and every hole is a question a human has to answer — which is the whole cost when an agent drives the machine. `security/perm_field.rs` adds a total function `evaluate(sources, query) -> Verdict` over `(uid, path, action)`, defined everywhere by construction from a sparse set of placed sources. Userspace membership is the same field with a different support rather than a separate predicate. Three properties carry the design and each has an assertion and a mutation. Deny dominates: any denying source in range returns `Deny` regardless of how many grants are nearer, so no point between a grant and a denial evaluates to a grant. Totality does not invent: a point no source reaches returns `Unknown`, and `Verdict::permits()` is true for `Allow` alone, so a caller cannot write `v != Deny` and quietly permit. `Unknown` refuses without prompting and reports the point as uncovered, which is what makes totality worth having — the kernel never asks a human, and an agent fixes the gap once by adding a source instead of answering forever. Inference only narrows, and structurally rather than by convention. `infer` returns a `Narrowing` holding `Cut`, and `Cut` has no polarity field: widening is not declined at runtime, there is nowhere to put it. `PermField::narrow` writes `Polarity::Deny` as a literal, and allowed observations enter only in a negative position, blocking a denial from lifting. A grant is not something inference can emit. The resource metric is descendant depth in the path tree, and it is asymmetric deliberately. A symmetric tree distance puts `/etc` two steps from `/data`, so a grant on `/data` with radius 2 would reach `/etc`; ancestors are excluded for the same reason, so granting `/data/x` cannot grant `/data`. Both directions are asserted. Subject and action stay discrete: nothing observable in this kernel makes two uids or two actions similar, and a fake metric there would generalize wrongly with confidence, which is worse than the table it replaces. The justification for the path axis is that `mac.rs` already writes every rule as a path prefix at component boundaries, so two siblings are security-similar exactly because the existing policy language cannot separate them without a new rule. The influence kernel is a step function on purpose. The verdict is a three-value lattice under deny-dominance, so any monotone-decreasing kernel with the same support produces the same verdict everywhere; smooth falloff would be decoration that cannot change an answer. Verification: registered in-kernel assertions go from 0 to 8, all passing, against 1 passed / 7 failed before the fix, where the red state was produced by transplanting today's `mac.rs` semantics into the field — the uncovered-path allow and an inference that widens. Seventeen mutations were applied and all seventeen killed, including letting a grant outrank a nearer deny, returning `Allow` out of range, inverting the polarity comparison, dropping each of the four bounds, leaking either wildcard, dropping the canonical-path or component-boundary check, and making `permits()` accept `Unknown`. The radius threshold is shifted in both directions — tightening it to `d < r` and loosening it by removing the clamp both fail assertions — because a guard nobody can over-tighten is a guard whose boundary was never tested. The radius bound is enforced twice, in `push` and again in `evaluate`, so a `&[Source]` handed straight to the free function still cannot exceed it, and each layer is mutated separately. `cargo +nightly clippy --release --target x86_64-unknown-uefi` on this machine: zero diagnostics name `perm_field.rs` in either profile. One assertion survived its own mutation and was repaired. The `MAX_OBSERVATIONS` bound was a comment rather than a guard, because `infer` already stopped at `MAX_SOURCES` cuts and dropping the observation slice changed nothing the test could see. It now uses a trace of exactly `MAX_OBSERVATIONS` allowed decisions followed by one denial, which produces no cut with the bound and one without it, plus a swap moving the denial one place earlier to show the assertion is not vacuous. `mac.rs` is untouched and this field is not wired into the live permission check. Replacing it is a separate change with its own risk, and shipping both at once means neither can be reviewed. Limits: QEMU is not installed on this machine, so the in-kernel run is CI's alone; assertions chain from `security::tests::register_all()`, which `testing/runner.rs:33` already calls, so no runner change was needed. The field cannot express any relation between applications, so a policy over a group of processes needs one source per uid against a budget of 64. It has no notion of content, time or state, so it cannot say "read only during boot" or "execute only if signed". A source reaches at most 8 levels below its anchor, where `mac.rs` prefix rules reach infinitely deep, so a deep tree needs more explicit sources and anything beyond is `Unknown` and therefore refused. Inference produces only denials and cannot propose the grant a human would obviously add, so a fresh system is entirely `Unknown` until someone authors grants by hand — the field removes repeated prompting, not the first authoring. `infer` is O(n^2 * MAX_RADIUS), about 131k component comparisons at the bound, which is fine off a hot path. Canonical input is checked rather than repaired: `/data/../root` evaluates to `Unknown` rather than to the verdict for `/root`. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
A model's demand for compute falls as it converges, and nothing in this OS noticed, so a converged job held everything it was given until it exited. `ml_engine/stratum.rs` already classifies a run as `Underfit`, `WellFit`, `Overfit` or `Collapsing` from topological signals; `tuner.rs` turns that into a share in `[floor, 1.0]` and gives the difference back. The model's own code contains no limit, which is the point — it does not know and must not have to. Reading the regime alone would have been wrong three separate ways, and finding that is most of this change. `classify` fails closed to `Collapsing` when the signal is unmeasurable, so a tuner trusting it would treat an unmeasurable signal as a reason to restore. The rule is that an unmeasurable signal leaves the allocation neither reduced nor raised, so `read_signal` mirrors the classifier's cascade and diverges in exactly one place: where `classify` must return some regime, this returns `Unmeasurable` and the tuner freezes. `classify` also returns `WellFit` while `samples < min_samples`. That is a default rather than a measurement, and reclaiming on it would starve every new job through its first sixteen steps. And under three points `measure()` returns the empty set with `spread = 1.0`, which reads as converged; `min_samples` normally hides that, but `set_field(5, 0.0)` is an accepted ABI value — `stratum`'s own `test_calibrate_rejects_unusable_ranges` asserts it is accepted — so an empty window can classify as converged. Both are gated. That third path is the one this whole design is defending against. Before it was fixed, `stratum` fabricated `shatter=1.000 h0_death=0 loop=0` for a cloud whose every pairwise distance had overflowed, reporting a run diverged to 1e200 as `WellFit` with every signal finite. A reclaimer built on a signal that can fabricate convergence starves exactly the jobs that most need capacity. Hysteresis is 3. Two would kill a one-on-one-off flap; three is the smallest that also kills a two-observation transient, because `quartile_drift` averages sixteen points and a single outlier moves the estimate for as long as it sits in the tail quartile. Reclaim is capped at a quarter of the current share per decision, which is the largest step for which a full descent still takes five decisions, so a transient cannot empty an allocation before the detector re-measures. The bound applies to reductions only — a restore returns everything this module took. The documented seven-observation descent is asserted rather than left in prose, since it is a claim about the code. Verification: 10 assertions, all passing, against 24 passed / 6 failed with the implementation stubbed, alongside 20 unmodified `stratum::*` assertions run through the same harness as a control that the harness is faithful. Sixteen mutations were applied and all sixteen killed, including treating unmeasurable as `WellFit`, dropping the warm-up or minimum-point gates, dropping the restore, crossing the floor in either direction, shifting hysteresis by one in each direction on both the reclaim and restore sides, exceeding the per-step bound, accepting a floor of zero, and swapping the streak counter's `saturating_add` for `wrapping_add`. The decisive one is raising the share on an unmeasurable signal: it separates "freeze" from "restore", which the regime alone cannot express. `cargo +nightly clippy --release --target x86_64-unknown-uefi` on this machine: 0 errors in both profiles, with zero diagnostics naming `tuner.rs`. One assertion passed vacuously under the stub and was repaired before the mutation run. `collapsing_run_is_restored` held for free because the share had never left the ceiling, so "restores to ceiling" was trivially true; it now requires the fixture to have actually been reclaimed first. Limits: QEMU is not installed on this machine, so the in-kernel run is CI's alone. **No GPU allocation is claimed.** `drivers/gpu/gpu_bench.rs` is a benchmark, and no path in the GPU tree divides a device between two workloads, so the share is a dimensionless fraction of the run's own initial grant and `reclaimed(t)` is a number rather than capacity. Making it real needs one thing in each direction: `ManifoldScheduler` dispatches by strict priority bucket and `Task` carries no CPU budget, so there is no quantity for a fraction to multiply — a per-task quantum that `schedule()` decrements and refuses to re-arm past would close it. For memory, `dispatch_brk` grows `brk_end` on request without consulting a limit, and `setrlimit(RLIMIT_DATA, ..)` assigns `brk_end` rather than bounding it, which is the same gap `FitAction::clamp_heap` already records. Confidence is expressed as accumulated observations rather than as a number derived from `h0_death`: `stratum` reports that as evidence and deliberately does not gate on it, and grading the share by it would gate on it one layer up with no ground truth. `sandbox.rs` is not imported; composing the two is a follow-up now that both have landed. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
…its own access pattern A sandbox for a guest workload whose resident frame count is derived from the structure of the pages it actually touches, rather than from a number chosen in advance. Page accesses are recorded as `(tick, page)` points, single-linkage H0 gives the working-region count, and the envelope follows. Both axes are rescaled to `[0,1]` over the observed range, which is not cosmetic: page indices run to millions while ticks run to 64, so raw Euclidean distance is page distance with rounding noise attached. After rescaling the summary is invariant under an affine relabel of either axis, which is asserted. Time is an axis rather than an ordering because a phase is what makes a region worth keeping — two page ranges touched in strict alternation are one working set, and the same two touched in separate phases are two, and only the time axis separates them. The tick is a counter the sandbox owns, never a wall clock. The cut is placed at the largest ratio between consecutive sorted MST edges rather than the largest gap, because a ratio is scale-free: eight regions separated by 10x is a reading worth acting on, and eight separated by 1.01x is noise about where the cut happened to land. That ratio is carried forward as confidence and scales the grant, so an unseparated reading grants nothing above the floor. Four rules hold and each has an assertion and a mutation that kills it. The cap is fixed at construction with no setter and is applied last and unconditionally, so no signal can raise the envelope past it. An unmeasurable signal sizes to the floor and never the ceiling — and the assertion compares the returned variant exactly, so a *conservative* fabrication dies too, not only a generous one. Allocation failure drains everything already taken and refuses, following `foliation::admit`, which was fixed today for publishing a resident leaf with no frame behind it. A shrink returns only unpinned frames and leaves the guest running. `saturating_add` is load-bearing rather than defensive. With `clusters` at `usize::MAX` a plain `floor + grant` wraps to 3 under the release profile's absent overflow checks, slips under the cap, and looks like the rule held for the wrong reason. Verification: 6 assertions, all passing, against a red state where the module did not exist and the harness would not build. Thirteen mutations were applied with the file restored and diffed identical afterwards. Twelve are killed by a named assertion, including removing the cap, sizing unmeasurable to the ceiling, fabricating either a generous or a conservative signal for a degenerate cloud, breaking out of the allocation loop instead of draining, shrinking a pinned frame, shifting the floor or the cap by one in either direction, and dropping the axis rescaling. `cargo +nightly clippy --release --target x86_64-unknown-uefi` on this machine: 0 errors and 0 warnings plain, 0 errors in test-mode, with zero diagnostics naming `sandbox.rs` in either — confirmed by an A/B with the module declaration removed and restored, since sibling agents moved the crate-wide count from 79 to 113 while this was being written. The thirteenth mutation, widening the sample window past the array, is killed by a bounds-check panic rather than by an assertion, and that is reported rather than counted as a pass. The window constant and the array length are the same named `MAX_SAMPLES` used twice so they cannot drift apart in shipped code, but the kill layer is a halt, not a refusal. Limits: QEMU is not installed on this machine, so the in-kernel run is CI's alone. **This sizes region count, not region extent, and that is the wrong quantity for the workload it is named after.** A model with one contiguous multi-gigabyte weight tensor reads as a single cluster and receives `FRAMES_PER_REGION` frames, which is catastrophically small; fixing it requires folding each cluster's population and diameter into the demand rather than counting clusters. `FRAMES_PER_REGION` is 4 with no derivation and is documented on the constant as the calibration knob, with the confidence weighting the only thing keeping a wrong value from being severe. A mostly-coincident cloud with one far outlier falls back to one cluster and under-sizes, which fails safe. A growth failure part-way through a re-evaluation leaves a partial grow with nothing recording it. Nothing calls this module yet: there is no syscall, no boot proof line, and no page-fault hook feeding `observe`, so the trace is empty and an empty trace sizes to the floor forever — that wiring is the next change. `SandboxPolicy` is local and minimal by instruction; connecting it to `security/perm_field.rs` is a follow-up now that both have landed. The MST loop is a near-copy of `stratum`'s private Prim implementation, which cannot be reused because it is hard-typed to `ManifoldPoint<3>` and returns only a maximum and median where this needs the whole sorted spectrum; lifting one shared `mst_edges` is noted in the file and touches two modules that were not in scope. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
…authenticate the header Commit 1046178 made the peer prove it holds the certificate's key. Three defects remained and each is closed here. `TlsSocket::connect` took an address and no name, so the peer was authenticated as some holder of a trust-store-issued certificate — any valid certificate from the anchor passed, including one issued for a different host. `x509.rs` has implemented and tested `matches_dns` all along with no production caller. `connect` now takes a hostname, threaded from `http.rs`, and `handle_certificate` requires the leaf to match it while the leaf still borrows the message buffer, so no state is carried. A session with no hostname matches nothing and refuses every chain. An address with no name is refused rather than accepted. RFC 6125 6.4 forbids matching an IP literal against a dNSName, so matching one anyway is exactly "silently accept any name", and matching an iPAddress SAN instead would need `parse_san` to stop walking past those GeneralNames, which is outside this scope. The guard sits in `connect` rather than in `http.rs` because every caller routes through it, so it is one guard and not two. `wrap_record` computed `payload.len() as u16`, so a plaintext at or above 65,536 bytes emitted a record whose length field had wrapped, reachable because `tls_socket.rs` passes caller data straight through. `encrypt` now fragments at 2^14 per RFC 8446 5.1, each fragment its own record with its own sequence number; refusing instead would have broken any body over 16 KiB and pushed chunking onto every caller. The guard is in the shared frame builder as well as the caller: `wrap_record` refuses anything over 2^14 and `record_header` over 2^14+256, so no future caller can wrap the field either. `encrypt` and `decrypt` both passed an empty AAD where RFC 8446 5.2 binds the record header. That was an undocumented third deviation in a module claiming exactly two. Both now bind `opaque_type || legacy_record_version || length`. No pinned ciphertext existed anywhere in the file, so nothing had to be regenerated — the only two AEAD sites round-trip within one session and move together. Verification: assertions go from 51 to 61, all passing. The strongest is `record_aad_is_the_rfc8446_header`, which constructs the additional data from the RFC 8446 5.2 text and the nonce from 5.3, then opens the kernel's record with a separate AES-GCM invocation that never calls `record_header`, and requires the same record to fail under empty AAD and under a wrong length field — so agreement means the record layer matches the specification rather than itself. Twelve mutations were applied and all twelve killed, including accepting a certificate for the wrong name, accepting any name when none was set, accepting an IP literal, masking the length, truncating instead of fragmenting, empty AAD on either side, zeroing or mis-sizing the AAD length field, dropping the receive-side overflow check, and matching against commonName instead of SAN. `cargo +nightly clippy --release --target x86_64-unknown-uefi` on this machine: 0 errors / 0 warnings plain and 0 errors test-mode, with the only three warnings naming `tls.rs` being the pre-existing `if let Err(_) =` patterns inside existing tests, shifted four lines by added documentation. Two mutations survived the first pass and both were the assertions' fault rather than the code's. One survived because an early `hostname.is_none()` return was dead — `is_some_and(None)` already fails closed — so the redundant guard was deleted rather than given a test for a check that cannot fail, and the mutation re-aimed at the real defect of accepting anything when no hostname is set. The other survived because the oversize record was built from garbage bytes and failed the AEAD tag regardless, so the assertion could not tell a length refusal from a tag refusal; it now forges a record with a genuinely valid tag at exactly `MAX_RECORD_LEN` and at one byte more, where only the length separates them. The line numbers in the dispatching brief were stale and each defect was relocated against the current file before anything was edited. Limits: QEMU is not installed on this machine, so the in-kernel run is CI's alone; the harness pulls both shipped files in by absolute `#[path]`. The name match is exact dNSName only — no wildcard and no iPAddress SAN, since `parse_san` walks past those without surfacing them. There is still no `server_name` extension in the ClientHello: this binds what this end will accept, not what the peer is asked to send. `x509.rs` has no name-mismatch variant, so a mismatch leaves `peer_cert_error` unset, the chain itself being sound, and reports the reason through the returned error instead. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
…e to ship it A fuzzy extractor that maps a password to a point cloud, computes an exact Vietoris-Rips H0 persistence diagram, quantises the death times to a stable fingerprint, and feeds that to a KDF with an Ed25519 commitment. The intent was typo tolerance backed by a hard cryptographic commitment, resting on standard primitives with topology only as a front end. The measurement says do not use it, and the measurement is the deliverable. Over an exhaustive corpus — all 65,536 passwords across a 16-character alphabet, so the distribution is exact rather than sampled — the construction produces 200 distinct keys, 6.293 bits of collision entropy and 4.871 bits of min-entropy, tolerating 63,364 of 65,536 case typos. `KDF(password)` gives 65,536 keys and 16 bits with no tolerance. `KDF(ascii_lowercase(password))` gives 4,096 keys and 12 bits, tolerates every case typo in the corpus with no boundary failures, and is one line. This module costs 9.707 bits against the first and 5.707 against the second, and buys strictly less tolerance than the second. The obvious rebuttal is that the grain is wrong, and it is answered by measurement rather than argument. A grain finer than any tolerated edit can move a death time is the raw diagram, which is the ceiling no quantiser can beat: 3,001 distinct keys and 10.182 bits, still 1.8 bits below the one-liner, and by then the tolerance is gone at 20 of 65,536. The lossy step is the topological sketch, not the quantiser. The original hypothesis was that the loss came from ordering; `perm_collisions=0/128` refuted it, and the documentation now records the measured cause instead of the predicted one. The module is therefore not wired into `shadow.rs`, `verify_login`, or any syscall. What ships is the apparatus and its verdict, re-runnable, with `CLAIMED_SHIPPABLE = false` asserted against the computed result so the conclusion cannot drift from the code. The topology is correct independently of that conclusion. All five invariants hold with assertions: permutation invariance over sixteen seeded shuffles and a tied grid, scale equivariance across c from 1e-6 to 1e6 with purely relative tolerance, the stability bound at 2*eps for three values of eps with the hypothesis re-asserted before the conclusion, the elder rule cross-checked against a separately written Prim MST, and a negative control paired with a positive one so that returning nothing cannot pass. A sixth covers the `stratum::mst_edge_stats` defect this session fixed: a NaN coordinate, an infinite coordinate, an overflowed distance and an over-cap cloud all return `None` rather than reading as a coincident point. Verification: 28 assertions, all passing, across both entropy arms and a stuck-source arm. Fourteen mutations were applied and all fourteen killed, including a grain no coarser than the stability bound, an absolute constant in the filtration, an inverted elder rule, a KDF that ignores the salt, a removed commitment check, a skipped overflow, a `bottleneck_h0` that always returns zero, a comparison that accepts anything, a discarded `verify_strict`, and a `CLAIMED_SHIPPABLE` flipped to true. `cargo +nightly clippy --release --target x86_64-unknown-uefi` on this machine: 0 errors / 0 warnings plain and 0 errors test-mode, with an A/B against the module removed showing this file adds exactly zero warnings. Three assertions survived their mutations on the first pass and all three were repaired. The scale sweep only used factors where every distance stayed above 1.0, so an absolute `.max(1.0)` never bit; it now spans 1e-6 to 1e6 with a purely relative tolerance, since the old tolerance went vacuous at small scale. A `bottleneck_h0` returning zero satisfied every stability assertion, so the yardstick is now calibrated against a known separation before it is trusted. And the version gate was unobservable because the signature already covered the parameter block, so the test now builds a validly signed forward-version record, asserts its signature genuinely verifies, and then asserts `open` still refuses it. A fourth mutation was correctly identified as equivalent rather than a hole: a constant salt of repeated bytes is absorbed by the stuck-source guard, so it was re-run with distinct bytes and then died. Limits: QEMU is not installed on this machine, so the in-kernel run is CI's alone; the harness pulls the shipped file in by absolute `#[path]`. Assertions register through `security::tests::register_all()`, which `testing/runner.rs:33` already calls, so the shared runner needed no edit. Only H0 is computed — H1 needs the 2-skeleton and O(n^3) simplices, which does not fit a fixed kernel heap. The KDF is iterated SHA-256 following the `shadow.rs` house idiom rather than an HMAC-based construction; `tls.rs:885` has a correct `hmac_sha256` with an RFC 4231 vector but it is private to that module, and making it `pub(crate)` is the upgrade. The salt comes only from the RDSEED/RDRAND arm of `drivers/entropy.rs`; `fallback_random_u64` is a never-reseeded xorshift whose own documentation calls it not security-grade, so enrolment fails closed rather than using it. Substitutions that change the folded letter and all insertions and deletions are not tolerated by design, and password bytes past 32 reach the key through a plain tail hash with no tolerance at all. `bottleneck_h0` returns an upper bound, which is the correct direction for asserting a bound, and returns infinity on mismatched cardinality rather than a matching it does not compute. Nothing calls `emit_boot_proof`, so the `[TOPOKEY]` line never reaches the boot log; whether a rejected construction deserves boot-log space is a decision, not an oversight. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Fix the CI gate chain so the in-kernel test harness can run
…w many b14631c recorded its own ceiling in its limits paragraph: the envelope counted working regions and ignored their extent, so an inference guest with one contiguous multi-gigabyte weight tensor read as a single cluster and received `FRAMES_PER_REGION` frames. That guest is the workload the module is named after, and count-shaped sizing is the wrong quantity for it — a tensor is one region with no separation, so every count-shaped term about it is 1. `WorkingSet::Clustered` now carries `pages` beside `clusters` and `separation`: the summed page span of every component holding at least `MIN_SAMPLES` accesses, read off the same MST cut the cluster count comes from. `mst_edges` returns edges with endpoints rather than lengths alone, because the partition is what carries a region's population and span; the spectrum is filtered out of that tree by the caller, so coincident points stay in one component instead of scattering into components of one. `size_envelope` takes the larger of the two demands, at `PAGES_PER_GRANTED_FRAME` = 32 pages per frame. Extent is deliberately not weighted by `separation` and deliberately not invariant under an affine page relabel. `separation` is confidence in the cut, so it weights the quantity the cut produced — the count — and a single contiguous region has no spectral gap to separate anything at, so a weighted extent would be worth exactly nothing on the case this change exists for. `pages` is a quantity of memory rather than a shape, measured from the raw page indices, so a guest striding seven times as far over seven times as much memory asks for seven times the stripe. The cut rule needed a second condition to support a partition. A uniformly sampled cloud has a spectrum uniform to within rounding, so every consecutive ratio in it is `1 + O(ulp)` and the largest lands wherever the last bit fell. b14631c tolerated that because a ratio that close to 1 grants nothing above the floor; a partition cannot, because a cut placed by rounding noise shreds one contiguous region into fragments and charges the guest for none of them. The gap must now clear `eps` in absolute terms as well as in ratio. Rule 1 is unchanged and matters more, not less: extent multiplies page counts rather than region counts, so it is the likelier of the two demands to wrap under a profile with `overflow-checks = false`, and a wrapped demand arrives under the cap looking like the cap held. Saturation is applied at the measurement as well as at the sizing — a component spanning page 0 to `u64::MAX` covers `u64::MAX + 1` pages, which is not a u64. Verification: registered assertions in this module go from 6 to 8. Both new ones are red on the pre-change code by construction, since `pages` does not exist there. `extent_sizes_one_large_region` pins three tensors that a count-driven envelope sizes identically — 64 accesses at strides of 16,384, 32,768 and 229,376 pages, all reading as `clusters == 1` — at 32,257, 64,513 and 451,585 frames, then re-asserts the cap against each of them at 256 and at 3, then asserts `frames_for_pages(u64::MAX) == 576,460,752,303,423,488` against a cap nothing can reach, then drives the whole thing through a live `Sandbox` whose 128-frame cap holds. `thin_cluster_buys_no_extent` builds three phases of 40, `MIN_SAMPLES` and `MIN_SAMPLES - 1` accesses and requires `pages` to be 39,937 + 3,073 exactly: the third phase straddles 100,001 pages and is charged to nobody, which is 1,345 frames rather than 4,375. `cargo +nightly clippy --release --target x86_64-unknown-uefi` from inside `kernel/seal-os` on this machine: exit 0, 0 errors and 0 warnings, no diagnostic naming `sandbox.rs`. Limits: QEMU is not installed on this machine, so the in-kernel run is CI's alone. `PAGES_PER_GRANTED_FRAME` is a calibration constant with no derivation, chosen against the trace window rather than a workload: a region the window can cover densely asks for 2 frames, below `FRAMES_PER_REGION`, so only a region wider than 128 pages moves the envelope at all. Population gates a component in and never multiplies its extent, because `MAX_SAMPLES` truncation makes a sample count a biased proxy for traffic — a region touched steadily holds fewer of the last 64 accesses than one touched in a burst — and the cost of that choice is a region whose share of the window falls under `MIN_SAMPLES` contributing no extent and falling back to the per-region grant. Extent is the span from lowest to highest page in a component, so a component with a hole in the middle is charged for the hole. The module still has no production caller: no syscall, no page-fault hook feeding `observe`, no boot-proof line, and an empty trace sizes to the floor forever. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
…agraphs that drove it The README stopped at 455/455 and a shell with pipelines. A new section covers the thirteen commits that landed after it on `ralph/graph-round-1` and what each one changed about the operating system, rather than about the test count. Seven are fixes to shipping code. TCP held every port it ever used, because `TCP_SOCKETS` only grew and `TimeWait` was terminal with no timer; a `SynSent` socket nobody answered retransmitted at the capped RTO forever and a half-open `SynReceived` cost a demux bucket per SYN across a table of 256. The TLS stack validated a certificate chain and set `connected`, with no CertificateVerify and no Finished anywhere in either file, so replaying a public chain passed — and after that was closed the peer was still authenticated as some holder of a trust-store certificate rather than as the host asked for, with a record-length field that wrapped at 65,536 bytes and an empty AAD where RFC 8446 5.2 binds the header. The package rollback floor lived in a struct field and reset on every boot. And `--check-o1-network` went red on the slot-map indirection while the property it enforces held. Five are subsystems that did not exist: shell scripting with `source`, comments and `echo`; a total permission field where an uncovered point returns `Unknown` and refuses without prompting; a tuner that reclaims from a converged training run and freezes rather than restores on an unmeasurable signal; and a sandbox whose resident envelope is sized from the H0 structure of its own access pattern. The thirteenth is the one the section is named for. A topological fuzzy extractor was built, measured against an exhaustive 65,536-password corpus, and refused by its own measurement: 200 distinct keys and 4.871 bits of min-entropy against 4,096 keys and 12 bits for a one-line `ascii_lowercase`, which also tolerates strictly more typos. It ships as apparatus and verdict with `CLAIMED_SHIPPABLE = false` asserted against the computed result, wired into no syscall. The section closes on a table of assertion counts and mutation results for all thirteen, and on three things the table is meant to show: that its one surviving mutation is listed rather than dropped, that four of the five new subsystems have no production caller and two of those four are unfinished rather than deliberately unwired, and that six of the thirteen commits exist because an earlier commit's `Limits` paragraph named the defect and someone came back and read it. Verification: the file grows from 6,381 to 6,985 lines, counted with `wc -l` before and after on this machine. Every count, constant and measurement quoted in the section is taken from the commit message of the commit it describes; no `.rs` file is touched. Limits: no kernel was booted for this revision, so the per-module assertion counts are as reported by the commits that registered them and not as observed in a run. The 455/455 figure the previous section records predates all thirteen. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
- Replaced full `useStore()` destructuring in `App.tsx` with individual selectors. - This optimization prevents the entire application root from unnecessarily re-rendering on every store state change. Co-authored-by: teerthsharma <78080953+teerthsharma@users.noreply.github.com>
|
👋 Jules, reporting for duty! I'm here to lend a hand with this pull request. When you start a review, I'll add a 👀 emoji to each comment to let you know I've read it. I'll focus on feedback directed at me and will do my best to stay out of conversations between you and other bots or reviewers to keep the noise down. I'll push a commit with your requested changes shortly after. Please note there might be a delay between these steps, but rest assured I'm on the job! For more direct control, you can switch me to Reactive Mode. When this mode is on, I will only act on comments where you specifically mention me with New to Jules? Learn more at jules.google/docs. For security, I will only act on instructions from the user who triggered this task. |
💡 What: Extracted Zustand properties using individual selectors
useStore((s) => s.property)instead of destructuringconst { ... } = useStore();inApp.tsx.🎯 Why: In Zustand, destructuring directly from the hook return object subscribes the component to the entire store. Since
App.tsxis the root component, any state update anywhere in the application (such as logs, telemetry, or loading states) would cause the entire React tree to unnecessarily re-render.📊 Impact: Prevents massive O(N) re-render cascades across the entire UI. The
Appcomponent will now only subscribe strictly to changes in the extracted setter functions (which typically remain stable).🔬 Measurement: Verify by utilizing the application (e.g. adding datasets, running commands) while profiling with React DevTools; the
<App>component itself should no longer blink/highlight on every state transition.PR created automatically by Jules for task 4628427529388954707 started by @teerthsharma