Large-scale refactoring with parity proof

Splitting two oversized files into modules

AgentOS: the AgentOS store and admin CLI had grown into two very large Rust files, and I had them split into domain modules.

Lines in the entry files

Store, before40,300Admin CLI, before42,500Library root, after20Admin main, after67

I decided the split was finished only when someone who had not done it could show it was the same system.

A parity proof from a witness who did not do the work

The parity proof came from a separate witness seat. Test counts are taken before a refactor, so "all green" is measured against the original code, and comparing exported symbols in the witness's own release builds catches an accidental API removal while confirming the intended demotions to private.

Exported symbols, before

Exported symbols, after

1test counts taken before the split

2clean build, database-backed tests on, all passed

3release binaries built by the witness itself

4export lists compared, as above

Lit cells are public symbols, grey ones the functions meant to become private; the empty gaps after the split are the intended demotions. Cell counts are illustrative.

A failed proof is not amended; it is replaced by a new proof that names the problems it resolved.

Policy hooks ported to one binary

The hook layer, through which AgentOS turns policy into refusals inside coding-agent sessions, went through the same discipline.

Before · one block per shell hook

After · one Rust binary

one Rust binary

tested against fake hook contexts; a publisher checks the installed hook surfaces byte for byte

A GPU runtime ported without changing a token

ActiveKV: the largest rewrite I have directed is ActiveKV, a GPU serving runtime ported from Python to a native C++ engine without changing a token. It matched every exact and compressed cell bit for bit at the port, and 12 of 12 on both routes at release.

Counted · cells matched bit for bit at the port exact

compressed

Voided · Python against Python

over a thousand passing trials, drawn here at one cell per ten

Three rules decided what counted: bitwise equality only where the reference agrees with itself across two runs, no safety guard removed to make outputs line up, and a route counts as native only when startup shows native code bound before the code that chose the route.

The differential suites were rebuilt around the object types the server actually passes, after stand-in objects let a broken path pass. The full story is in Rewriting an engine extension without changing a token and Proving a rewrite is the same system.

That range, from an 80,000-line structural split with no behaviour change to a language migration of a GPU runtime that kept every output bit, is what directing a large rewrite by many parallel agents looks like when the result still has to be shown to be the same system.