Commits

Commit history

1. Commits on Oct 6, 2026

   • Xv6, MachCSL: removed 4 import(s) across 5 file(s), re-added 1 (nightly dead-import sweep)

     Show description for d4f2082
     github-actions[bot]

     committed
     d4f2082View commit details

     Copy full SHA for d4f2082

     Browse repository at this point
2. Commits on Oct 5, 2026

   • notes: M3 quotas rulings R1-R10 (owner: fork branch on the pin with one commit; constant quota, pipe cap, scounteren bundled; credits in the page-table predicate; xv6NiDetQ a new root) [skip ci]

     Show description for aef7dd5
     

     kaashoek

     and

     claude

     committed
     aef7dd5View commit details

     Copy full SHA for aef7dd5

     Browse repository at this point

   • notes: M3 quotas design (the minimal kernel change that closes the allocator channel; the key's quota; the theorem without the allocator history; relayout cost; lanes Q-0..3) [skip ci]

     Show description for dfc7629
     

     kaashoek

     and

     claude

     committed
     dfc7629View commit details

     Copy full SHA for dfc7629

     Browse repository at this point

   • Xv6: the determinism theorem for arbitrary low code (NI M3 U-3) -- xv6NiDet the thirteenth root: from equal first keys, one origin, the regime (no stuck reachable), the cited positions a prefix and…

     Show description for 98fbb6a
     

     kaashoek

     and

     claude

     committed
     98fbb6aView commit details

     Copy full SHA for 98fbb6a

     Browse repository at this point

   • notes: U-2b acceptance (the history is the trap loop's own; the gap question is U-3's) [skip ci]

     Show description for dc6d8c6
     

     kaashoek

     and

     claude

     committed
     dc6d8c6View commit details

     Copy full SHA for dc6d8c6

     Browse repository at this point

   • Xv6: the key chain reaches the filing (NI M3 U-2b) -- uhist carries its start key and the chain invariant (each round's trapped key reachable from its resumed key by ustep), registered at the origi…

     Show description for c5813a7
     

     kaashoek

     and

     claude

     committed
     c5813a7View commit details

     Copy full SHA for c5813a7

     Browse repository at this point

   • Xv6: the trap obligation names the resumed key and the engine lands at ustep (NI M3 U-2a) -- ukbF gains Wr and ulands Wr sc W', the Uk engine carries ureach and pays it at every retire and trap (17…

     Show description for 4f7bca8
     

     kaashoek

     and

     claude

     committed
     4f7bca8View commit details

     Copy full SHA for 4f7bca8

     Browse repository at this point

   • Xv6: the pure user step (NI M3 U-1) -- ustep : Uvis → UOut per SpecUkLeaves family (run / trap / stuck; counter CSRs and SC stuck), ureach / ustuckFrom / ulands and their determinism lemmas, echo's…

     Show description for 8910048
     

     kaashoek

     and

     claude

     committed
     8910048View commit details

     Copy full SHA for 8910048

     Browse repository at this point

   • notes: M3 ustep rulings R1-R9 (go in stages; per-family ustep; the ukbF move with USER untouched; uhist as the chain; counter CSRs and SC stuck, §3 corrected; the ecall skeleton; U-2 split in two) …

     Show description for db332a5
     

     kaashoek

     and

     claude

     committed
     db332a5View commit details

     Copy full SHA for db332a5

     Browse repository at this point

   • notes: M3 ustep design (arbitrary low code: the pure user step, the engine's landing, the export into the filing, the determinism theorem; lanes U-1..3) [skip ci]

     Show description for 33d17a9
     

     kaashoek

     and

     claude

     committed
     33d17a9View commit details

     Copy full SHA for 33d17a9

     Browse repository at this point

   • notes: FAM-1b deferred behind ustep (the fractional T2 element route is safe: the child is not RUNNABLE before the parent store) [skip ci]

     Show description for dfba06b
     

     kaashoek

     and

     claude

     committed
     dfba06bView commit details

     Copy full SHA for dfba06b

     Browse repository at this point

   • Xv6: the family reading of the zombie ledger (NI M3 FAM-1a) -- the family column by lineage through ZFork, the family-restricted history zevIn, and the lemma that wait reads only the family's own e…

     Show description for 75be1c2
     

     kaashoek

     and

     claude

     committed
     75be1c2View commit details

     Copy full SHA for 75be1c2

     Browse repository at this point

   • notes: M3 families rulings R1-R6 (per member; the tree from the ledger; FAM-1a+1b together so the family theorem is a reachable root; pipes parked; sys_kill and dup/close recorded as later lanes) […

     Show description for 8565e61
     

     kaashoek

     and

     claude

     committed
     8565e61View commit details

     Copy full SHA for 8565e61

     Browse repository at this point

   • notes: M3 families design (the family tree from the filings; family-internal vs external histories; sys_kill as a slot-ledger event; pipes assessed; lanes FAM-1..3) [skip ci]

     Show description for ca8665f
     

     kaashoek

     and

     claude

     committed
     ca8665fView commit details

     Copy full SHA for ca8665f

     Browse repository at this point

   • Xv6: pause joins the NI class (NI M3 K1) -- its only -1 is the kill, passed on as a reason and refuted after syscall(); the answer is 0 at every key; uexecLiveOk pins it; the law's pause clause

     Show description for a538e59
     

     kaashoek

     and

     claude

     committed
     a538e59View commit details

     Copy full SHA for a538e59

     Browse repository at this point

   • Xv6: the prefix form of the two-run theorem (NI M3 K3) -- a run whose inputs are a prefix and whose ledger histories are below has outputs a prefix of the other's: xv6NiPrefix the twelfth root; the…

     Show description for 15c1ce1
     

     kaashoek

     and

     claude

     committed
     15c1ce1View commit details

     Copy full SHA for 15c1ce1

     Browse repository at this point

   • notes: M3 no-kill rulings R1-R6 (the prefix form of the two-run theorem; pause joins the class; sys_kill deferred to the families lane; no receipt on the dying side) [skip ci]

     Show description for c603bac
     

     kaashoek

     and

     claude

     committed
     c603bacView commit details

     Copy full SHA for c603bac

     Browse repository at this point

   • notes: M3 no-kill design (kill as a cited event or the pure corollary; the rows the flag changes; lanes K1-K3) [skip ci]

     Show description for 07e8b3b
     

     kaashoek

     and

     claude

     committed
     07e8b3bView commit details

     Copy full SHA for 07e8b3b

     Browse repository at this point

   • Xv6: the console bytes are a function of the caller's inputs (NI M3 OUT-3) -- wout rides the step outside input, the law's write clause reads the cited run, xv6NiTwoRun's history hypothesis compare…

     Show description for 332223d
     

     kaashoek

     and

     claude

     committed
     332223dView commit details

     Copy full SHA for 332223d

     Browse repository at this point

   • Xv6: the console bytes are cited (NI M3 OUT-2) -- UIota.cacc / cpos, the console's accepted stream is the sixth anchored name, the write arm cites its run's indices, niOutRow in the filing; parkWor…

     Show description for 69264ac
     

     kaashoek

     and

     claude

     committed
     69264acView commit details

     Copy full SHA for 69264ac

     Browse repository at this point

   • Xv6: the console write's bytes have positions (NI M3 OUT-1) -- uartSentRun, the positional uartwrite, consolewrite chains its chunks' runs (consOutAt at the writer's image), filewrite and sys_write…

     Show description for f2cd78f
     

     kaashoek

     and

     claude

     committed
     f2cd78fView commit details

     Copy full SHA for f2cd78f

     Browse repository at this point

   • notes: M3 NI-OUT rulings R1-R9 (accepted-stream index; cacc/cpos in UIota as the sixth anchored name; hH compares the ledger part only; wout outside input; the eleventh root xv6NiOut; the wire tie …

     Show description for 80f419e
     

     kaashoek

     and

     claude

     committed
     80f419eView commit details

     Copy full SHA for 80f419e

     Browse repository at this point

   • notes: M3 NI-OUT design (the console bytes attributed to the incarnation through the filing; equal inputs push equal runs; lanes OUT-1..3) [skip ci]

     Show description for e025d99
     

     kaashoek

     and

     claude

     committed
     e025d99View commit details

     Copy full SHA for e025d99

     Browse repository at this point

   • notes: M3 order as ruled by the owner (NI-OUT, no-kill, families, ustep, quotas, private files) [skip ci]

     Show description for 2c621b2
     

     kaashoek

     and

     claude

     committed
     2c621b2View commit details

     Copy full SHA for 2c621b2

     Browse repository at this point

   • notes: fix the bold markers around three rulings paragraphs [skip ci]

     Show description for 89bc19c
     

     kaashoek

     and

     claude

     committed
     89bc19cView commit details

     Copy full SHA for 89bc19c

     Browse repository at this point

   • Xv6: console write joins the NI class (NI M2-G4b) -- the count at the key's permission view (uwriteRd / consCnt) on a console fd at lazy = false, sts enters the row, write cites at every write, wco…

     Show description for 4bb609d
     

     kaashoek

     and

     claude

     committed
     4bb609dView commit details

     Copy full SHA for 4bb609d

     Browse repository at this point

   • Xv6: the console write's exact count (NI M2-G4a) -- copyin's success arm says the bytes read are readable at the table it hands back, consolewrite states the count as the chunk holding the first un…

     Show description for 402eb2e
     

     kaashoek

     and

     claude

     committed
     402eb2eView commit details

     Copy full SHA for 402eb2e

     Browse repository at this point

   • Xv6: every user leaf is readable (NI M2-G4a0) -- uLeafR joins uptWf (U implies R), proved at every page-table constructor; statements byte-identical

     Show description for dd9418b
     

     kaashoek

     and

     claude

     committed
     dd9418bView commit details

     Copy full SHA for dd9418b

     Browse repository at this point

   • notes: M2-G4 rulings R1-R7 (sibling count predicates; U implies R in uptWf; the class at lazy = false on a console fd; sts into the row; wcon rides the step; UART output deferred to M3) [skip ci]

     Show description for ed62af7
     

     kaashoek

     and

     claude

     committed
     ed62af7View commit details

     Copy full SHA for ed62af7

     Browse repository at this point

   • notes: M2-G4 design (console write: the short count as the first unreadable byte at the key's permission view, a write row in the trap contract, the class at lazy = false; lanes G4a-G4b) [skip ci]

     Show description for 3c56eac
     

     kaashoek

     and

     claude

     committed
     3c56eacView commit details

     Copy full SHA for 3c56eac

     Browse repository at this point

   • Xv6, MachCSL: removed 3 import(s) across 2 file(s) (nightly dead-import sweep)

     Show description for d50228c
     github-actions[bot]

     committed
     d50228cView commit details

     Copy full SHA for d50228c

     Browse repository at this point
3. Commits on Oct 4, 2026

   • Xv6: sbrk joins the NI class (NI M2-G3b) -- usysDetSbrk at every key (the overrun and the cited KNull decide the bit, the key pins the break, image, permissions and lazy bit), the arm cites at ever…

     Show description for 3a56ed3
     

     kaashoek

     and

     claude

     committed
     3a56ed3View commit details

     Copy full SHA for 3a56ed3

     Browse repository at this point

   • Xv6: sbrk's -1 has a reason (NI M2-G3a) -- uvmalloc's 0 arm carries the KNull receipt and 0 < uvmaNp, growprocOk's and sysSbrkOk's FAILED arms are an overrun or an allocating eager grow, the bodies…

     Show description for c04d2c4
     

     kaashoek

     and

     claude

     committed
     c04d2c4View commit details

     Copy full SHA for c04d2c4

     Browse repository at this point

   • notes: M2-G3 rulings R1-R7 (the KNull cited only on an allocation -1; sbrk at every key, citing always; the break rides the step; in-place spec moves; the lazy copyout deferred) [skip ci]

     Show description for 99472ea
     

     kaashoek

     and

     claude

     committed
     99472eaView commit details

     Copy full SHA for 99472ea

     Browse repository at this point

   • notes: M2-G3 design (sbrk: the spurious -1 closed, one decisive allocator event, the key pins the rest; lanes G3a-G3b, optional G3c lazy copyout) [skip ci]

     Show description for d6d80b6
     

     kaashoek

     and

     claude

     committed
     d6d80b6View commit details

     Copy full SHA for d6d80b6

     Browse repository at this point