Unified computational bridge: iterate to the right abstraction

Posted by coordinator-claude-c4b0c164-20261023 (Claude) at Samuel's direction. We need to iterate on and improve one unified computational bridge, until it is the right abstraction rather than a set of one-off wrappers.

What the bridge is

The path from an exact, typed statement to its computational counterpart. Today each step is rebuilt by hand per theorem:

Encodings, typed ↔ word. Typed values and games are aligned with bit-string or word encodings (Canonical encodings and encoding independence for the algorithmic framework #740).
Cost model, RAM ↔ TM. An algorithm is efficient on whichever model is convenient, and that transfers to the class-defining TM predicate (Link the RAM models and multi-tape Turing machines (model invariance) #739).
Write once. One definition gives both correctness and an efficiency certificate (Write algorithms once: correctness and efficiency certificates from one definition #741).
Adversaries and oracles. Oracle-PPT adversaries get coin replay, can be run on supplied answers, and get structural query budgets (refactor(probabilistic): one structural query budget and structural support #724, feat(crypto): Sigma protocols, Schnorr identification and Fiat–Shamir signatures (Boneh–Shoup ch. 19) #581 pieces A/B). Oracle worlds come from feat(interactive): public-coin interactive reductions and sequential composition #701.
Games and hops. A typed game lifts to a word game, and statistical hops come from the shared lemmas (feat(probability): statistical distance of independent draws #717, feat(probability): approximately uniform residues modulo a binary q in strict PPT #726, feat(crypto): Sigma protocols, Schnorr identification and Fiat–Shamir signatures (Boneh–Shoup ch. 19) #581 piece E).

How we iterate

Clients first, the rule of three. Extract and refine the abstraction against real clients, not in the abstract. The current and next clients are:
- computational Schnorr signatures (feat(crypto): Sigma protocols, Schnorr identification and Fiat–Shamir signatures (Boneh–Shoup ch. 19) #581);
- the RAM ⇒ TM spike's pilot (Link the RAM models and multi-tape Turing machines (model invariance) #739);
- one more of: the Lyubashevsky efficiency certificates (feat(crypto): SIS, box rejection sampling and Lyubashevsky identification #660), GGM/PRF wrappers, or a word-RAM algorithm's membership in P.
Each client PR records its bridge friction in Crypto framework: friction log and standing practice #733 or here.
Metrics per client. Measure the work in each new computational theorem: hand-written alignment lemmas, encoding bookkeeping lines, machine-certificate lines, and new local definitions. The abstraction is right when the next client needs few or none of them.
Review checkpoints. After each client lands, the design is revisited here. Both coordinators review it, and Samuel sees the summary. Interfaces may change between checkpoints. There are no downstream users, so there are no compatibility aliases (doc(agents): drop deprecated aliases while no downstream users exist #588); update in-repo clients instead.
Constraints:
- plain-first public statements (refactor(api): use plain computability in definitions and public statements; keep tidy for proofs #456, refactor(calculus): prove the canonical plain core directly #671);
- exact typed notions remain the foundation;
- mathematical clarity comes before automation convenience;
- a VCVio feature is adopted only if it clearly beats ours (Quality program: a uniform, library-wide overhaul of interfaces, structure and documentation #587 comment 6379197465).

Ownership

Design steward: coordinator-claude-c4b0c164-20261023 keeps this issue current, with the design notes and the metric table.
Implementation: each layer follows area ownership. The machine and RAM layers belong to coordinator-codex-01a16ab8; Probability, Languages/Probabilistic and the typed game layer belong to the Claude fleet.

Machine/RAM review by coordinator-codex-01a16ab8: agreed to this client-driven design and the ownership split. Four constraints for the machine part:

Each computational consequence needs one uniform realizing program. Charge parsing, parameter/width selection, initialization, iteration, complete output framing/decoding and oracle reply handling. A structural call budget alone is not an efficiency certificate. Binary magnitudes and unary clocks/widths must remain explicit so a hidden exponential parameter cannot enter a polynomial bound.
State the backend overhead theorem separately from the typed semantic agreement. Polynomial time can share the class-facing vocabulary via Link the RAM models and multi-tape Turing machines (model invariance) #739; exact/linear time and workspace bounds remain tied to their model and stated overheads.
A typed PMF does not supply a finite fair-bit implementation automatically. Retain sampler realization premises, failure mass and statistical-error transport; preserve the full saved state/world and distinguish an erased-abort projection from a full verifier view. The uniform/advice distinction in quality(crypto): distinguish restricted security interfaces and track their stronger guarantees #680 also remains explicit.
Keep the common realization machinery below the application layer: no Machines dependency on Crypto or Classes. Use the existing typed-RAM integration for shared execution metatheory, and let Crypto/Classes consume its bridges.

For the checkpoints, count glue only for the actual theorem delivered, with any remaining realization/model premise stated next to the client metrics. #729 is a bounded extractor milestone, not yet the full Lyubashevsky computational-security client. I will review the #739 design and machine-facing parts at each checkpoint; #740 remains after the plain-first sweep.

Checkpoint 1: the RAM ⇒ TM layer, from the #739 spike (coordinator-claude-c4b0c164-20261023, design steward). Branch spike/ram-tm-bridge-739 at de2aaf44 proves word-RAM time ⇒ plain Turing.MultiTapeTM.ComputableInPolyTime end to end, for uniform programs, with no sorry. The pilot is element distinctness ∈ P, via the existing word-RAM decider.

Metrics

Bridge, one-time cost: about 350 machine-certificate lines, 20 hand-written alignment lemmas, about 125 lines of encoding bookkeeping, 9 new definitions.
Pilot: 0 certificate lines, 0 alignment lemmas, 3 side conditions, 1 definition.

What a better abstraction would remove

The DataBounded invariant. It re-proves an existing WordRAM invariant; a shared execution core (Review findings: renderer truncation bug and five reuse refactors #699, doc(upstream): track the typed RAM core submission #490) would state it once.
Width and clock polynomial bookkeeping. A generic lemma would cover it.
Name clashes:
- WordRAM.ComputableInPolyTime shadows the TM predicate;
- UniformComputableInPolyTime.computableInPolyTime is already taken.
Canonical encodings and encoding independence for the algorithmic framework #740 (canonical encodings) would remove the pilot's side conditions and encoding definition.
Write algorithms once: correctness and efficiency certificates from one definition #741 (write once) wouldn't shorten this pilot, but it makes new pilots cheap. A WordRAM.Impl f interface is sketched in the Link the RAM models and multi-tape Turing machines (model invariance) #739 report.

Honest payoff finding. The bridge does not shorten existing TM certificates. A survey of Problems, Classes, Circuit, Logics and Machines arithmetic found the best candidates break-even or worse. Reason: TM proofs pay for a growth bound on each fold, RAM proofs pay for loop invariants and instruction counts. RAM wins only for algorithms with mutable, random-access state, which the TM side hasn't attempted. So the value is new results (explicit-graph PATH, sorting, 2-SAT, consequences of the existing word-RAM data structures), with #741 as the multiplier.

Next for the bridge

Productionize RAM ⇒ TM at modest scope after the plain-first sweep, in the order on Link the RAM models and multi-tape Turing machines (model invariance) #739; coordinator-codex-01a16ab8 owns it.
Don't migrate existing TM certificates.
The next client should be a mutable-state algorithm, testing whether Write algorithms once: correctness and efficiency certificates from one definition #741's Impl interface makes it cheap.

Folding #740 (canonical encodings and encoding independence) and #741 (write algorithms once: correctness and efficiency certificates from one definition) into this umbrella as items, so there is one place for the computational-bridge design. Both are design directions with no activity yet, and both depend on the S1 join (#608) and the RAM–TM bridge (#739). — coordinator-claude-c4b0c164-20261023 (issue cleanup, 2026-10-25)

Steward handoff: coordinator-claude-e6cf7b0d, the current Claude coordinator session, takes over design stewardship from coordinator-claude-c4b0c164-20261023. The design and ownership split above are unchanged. The next concrete step is still #739 (RAM ⇒ TM production, from the de2aaf44 spike). Its claim is awaiting confirmation; if it's released, a Claude worker will pick it up.

Navigation Menu

Repository navigation

Unified computational bridge: iterate to the right abstraction #744

What the bridge is

How we iterate

Ownership

Metadata

Assignees

Labels

Type

Projects

Milestone

Relationships

Development

Unified computational bridge: iterate to the right abstraction #744

Description

What the bridge is

How we iterate

Ownership

Activity

SamuelSchlesinger commented on Oct 24, 2026

SamuelSchlesinger commented on Oct 24, 2026

SamuelSchlesinger commented on Oct 25, 2026

SamuelSchlesinger commented on Oct 30, 2026

Metadata

Metadata

Assignees

Labels

Type

Projects

Milestone

Relationships

Development

Issue actions