dregg microsites15 / machinic mental autarky

A research direction with running pieces

Keep learning.
Keep a secret.

The host supplies the machine.
Must it also get the ability to
open everything inside?

A machine could learn from what happens to it, change its mind, and answer you—while its running implementation contains no universal reader of its internal state.

That is the target. We have encrypted learners, proof machinery, and narrower cryptographic capabilities. We are working to make them one thing.

HOST / supplies compute
↗an observationenters through the interface
CONTINUING STATEs → s′
weights · memory · randomnesslearn / infer
↗an answerleaves through the interface
01 / The intended boundary

Computation continues inside. A designated answer comes out. The ability to continue should not confer a separate ability to inspect. This diagram describes the target, not a completed construction.

A private lifetime.

Encryption usually protects a file until somebody opens it. Here the object has to keep going. Its state changes. New observations arrive. Yesterday’s output becomes part of tomorrow’s world.

“Only learn and infer” is not enough as an API description. Chosen lessons and questions may jointly reveal everything. A copied encrypted snapshot may support a different history. A credential called an encoder may secretly have the power of a master key.

The question is concrete: what can the union of all surviving credentials do? Include old keys, input issuers, archives, evaluation material, and copies. An administrator’s promise is not a cryptographic restriction.

Four capabilities to keep distinct

Who can do what?

FHE / the encrypted learner

Work on ciphertext.

The evaluator can update encrypted state without opening it. Our running nonlinear benchmark still retains a full reader key for the final correctness audit.

Computation
Encrypted operations
Evidence
Encryption alone does not certify the operation
Read authority
Full reader remains in this benchmark
History
Copies and forks require separate treatment

An explanation of capability models; these controls do not run cryptography. “Target” is a research specification.

The learner is real.
The conjunction is open.

A nonlinear encrypted learner has now completed 384 Learn operations and 96 Infer operations. The runtime executes schedules emitted from the Lean description. Independent executions matched all 480 complete ciphertext byte pairs. After the public phase closed, all 484 authorized primary comparisons matched their integer references.

That is an actual encrypted trajectory. It uses a fixed research fixture and retains a full reader key. A separate text path runs a real encoder at a trusted issuer, learns an encrypted contribution, and returns verified answers. Neither experiment makes the encoder private or removes every reader.

A different construction goes after the credentials themselves. Its public setup never constructs a scalar master secret under its stated sampling model. Dedicated recipients can keep computing their fixed projections. A public-seed implementation also runs. But those recipient keys remain usable on retained inputs outside the journal.

The stronger properties currently live in different objects. Joining them means changing the construction—not adding their claims together.

Read the encrypted trajectory ↗

From a running encrypted learner

Teach it something
it did not know.

“I cannot log in because I no longer remember the code for the app.”

BEFORE

card_payment_not_recognised

TWO NEW EXAMPLES / account_access

“I forgot the passcode for the banking app and cannot sign in.”

“Please help me reset my login password so I can access my account.”

AFTER

account_access

A recorded interaction with the eight-class model: teaching created its ninth class. The encrypted and plaintext implementations returned the same scores. This is new behavior after teaching, not an accuracy estimate.

The same prototype learner now has a persistent 78-class encrypted model. Its fixed encoder stays in plaintext; its class memories and dot-product computation use BFV. On the full original 77-class test set, the plaintext model reached 73.15% accuracy; the separate encrypted integration checked one fixed query per class. A full reader key still survives.

Run the teach/query learner ↗

8 September / the next constructions are running

Teach. Prove.
Keep going.

Two new teaching sentences now become encrypted class memories, each with a fresh proof and durable commit. A new query then gets a proof for both class computations before either answer is read. The complete fresh run took 21.20 seconds, including startup.

  1. 01Two teachings
  2. 02Prove and commit
  3. 03Prove both scores
  4. 04Read the answer

The ATM-fee query selected the withdrawal-fee class: 238,227 versus 211,756. Both scores matched. Omitting a class was refused without a read or state change. Encoding, parsing and decryption remain outside the arithmetic proofs, and a full BFV reader survives. Run and evidence ↗

NARROWER READ AUTHORITY

Sixteen query keys.
No universal reader constructed.

A separate ring learner completed six encrypted teachings and two expiries. Its recipients obtained 96 matching scores using independent keys for sixteen fixed semantic queries.

Each key can still read its projection on every retained input; the coalition gets the whole sixteen-query span. Known public data, honest setup and conditional hardness remain explicit. These updates have no attached proof or history-bound release.

Restricted-key learner ↗

NONLINEAR ENCRYPTED LEARNING

Square the similarities.
Learn a new class.

A BFV kernel learner executed 320 ciphertext squares, producing 2,560 matching individual values and 48 matching decisions. Two new teachings changed a live answer to the new travel_insurance class.

The reused-data comparison found no gain over its same-feature linear control. Its recipient retains a full reader. A separate generated proof now covers the actual nine-to-four modulus rescale over all 24,576 coefficient positions. Six proofs cover 98,304 output residues; preceding multiplication and whole-learner coverage remain open.

Nonlinear learner ↗
Native rescale proof ↗

These are separate running constructions. Below, you can check the earlier learner update and both class computations from the new query. The restricted-key learner is a separate backend.

03 / verifiable fully homomorphic encryption

Show the work.
Keep the state.

Encryption lets a host compute without reading. A proof can let someone check that computation. The proof must describe the exact encrypted operation the system actually performed.

01

Encrypted inputs

The host receives usable ciphertexts.

02

An exact relation

The intended arithmetic, including integer rounding, becomes the statement.

03

A checkable proof

A verifier checks the claimed transition.

This is the vFHE frontier. Correct computation alone does not establish hidden state, authorized disclosure, or one continuing history.

Run the actual verifier

Check the update.
Check the query.

Verify learner update 65 or both class computations from the recorded two-class query. These replacement proofs use corrected arithmetic constraints on all 8,192 rows, including the final row. The actual WebAssembly verifier runs on your device.

The earlier emitter skipped arithmetic on the last row. All three examples below have been re-proved with whole-row constraints; their unchanged verifier accepted them in Node, and the changed-output control rejected. Read the repair and remaining limits.

prior memory+fresh example−expired example=new memory
509 kB update proof1.69 MB two query proofs0 secret keys needed
Not checked yet.

Verification runs on your device. The second button changes one public output digit and submits the original proof.

These checks cover the selected ciphertext coefficient equations with corrected row coverage; native parsing, lookup extraction and cryptographic soundness remain separate assumptions. They do not prove text encoding, authorization, expiry policy, decryption, ranking or the absence of a full reader. Only public proof data and coefficient rows are downloaded; the verifier module is shared.

Proof, generated relation and standalone verifier ↗
Both query proofs and standalone consumer ↗

The difficult seam
is the useful one.

A release gate must know more than “this looks like an answer.” It must bind the computation to its genesis, parent state, admitted input, recipient, and randomness rule. Otherwise a host can substitute an extraction computation—or use a surviving key to bypass the gate altogether.

There is another arithmetic trap. BFV multiplication includes integer rescaling. Proving a product modulo the ciphertext modulus does not prove the rounded integer result. The relation needs the integer certificate; dropping it can erase exactly the output constraint we wanted.

The wider construction cycle now has a useful encrypted learner, an executable ring-based restricted-function scheme, and a conditional bounded transcript/replay route to nonlinear release. A separate ring-matrix implementation has generated a real PCS-enabled proof accepted by its verifier. The Lean-generated BFV proof now checks an actual learner update in native code and WebAssembly; none of these separate results establishes the complete private resident.

The proof system has its own work to do: compose actual folding rounds, move less witness data, and stop recomputing the same arithmetic. Faster proofs matter because the protected learner has to keep living between demonstrations.

Follow the construction swarm ↗

The ambition

The ability to continue.
The ability to communicate.
No universal reader.

“Machinic mental autarky” names this research target: a useful, continuing machine with an interior its host has no special privilege to open. Its permitted answers still communicate information. Its evolving state remains its own.

Work you can follow.

Research index

Executed results, proof proposals, construction notes.

8 September checkpoint

The completed run, its boundaries, and what remains.

Current research verdicts

The FHE and proof-system findings that govern the notes.

Prove the turn

The semantic computer underneath this work.