Repository navigation
Compiled-core parity: fixture profiles declare and prove their integer slots - #241
Merged
Merged
Conversation
- The shared wire codec, the markup adapter, and the markup frame channel prove decoded integer slots in place: bind the value, range-guard it with ordered comparisons, and state wholeness with Math.trunc at the write. - Fixture counter bumps saturate at the i64 class's provable ceiling, ±(2^53 − 1), so range discharges. - Model.pastBytes stays f64-classed: it holds 2^53 by design, past the provable window.
- The text SDK gains one provable selection constructor: every editor-produced selection is range-guarded and stated whole with Math.trunc, keeping the proof local to the construction site. - The ai-chat composer binds composition bounds and proves them at the write; -1 stays the no-composition sentinel. - The chat_response status and nextId bumps prove in place with the same guard-and-trunc idiom.
- Samples, probe results, and ps rows bind, range-guard, and Math.trunc their counts at each classed write; unprovable values keep the previous sample or skip the line like any other malformed row. - The adapter proves dispatch values and classed helper returns in place with the same guard-and-trunc idiom. - Structurally identical union arms lower to one record shape, so one code slot and one pid slot carry the class for their siblings (SC4009 keeps colliding declarations out).
- Catalog ids, playback clocks, and queue counters bind, range-guard, and Math.trunc at each classed write; the clock-tick cap comparison replaces Math.min so the proof stays in view. - The adapter proves its ten classed helper returns in place with the same guard-and-trunc idiom. - The id-carrying Msg arms share one lowered record shape with QueueEntry, which carries the class for all of them (SC4009 keeps colliding declarations out).
- Snapshot, helper-result, record, and channel encoders write classed slots with wI64 (optionals via wOptionalI64), matching the contract each adapter now attests. - Text-input decoding reads selection offsets and composition cursors as i64; selection offsets ride a saturating reader because select-all sends the maxInt to-the-end sentinel, which every consumer snaps to the text's length. - Classed helper results route through their proven wrappers and encode with wI64.
|
The latest updates on your projects. Learn more about Vercel for GitHub.
|
- The ten same-shaped Msg arm slots join the soundboard and system-monitor profiles, so the declared set covers every provable reference slot and only the deliberate 2^53 boundary probe stays f64. - Decode ingress proves in place where synthesized record slots carry write obligations: soundboard's id dispatches and audio clocks, and the shared composition-cursor decode, each range-guarded with wholeness stated by Math.trunc. - The ai-chat and markup profiles drop a subscriptions_export naming a function their entry modules never exported; a dangling name refuses instead of resolving silently.
This branch was successfully deployed
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Every compiled-core fixture profile now declares the integer slots its transpiled twin attests, and the paired-core battery proves the attestations byte-for-byte on the wire.
What changed
integer_slots: [].Math.trunc; counter bumps saturate at the provable ±(2^53 − 1) ceiling. The text SDK gains one provable selection constructor (caretSelectionAt) so editor-produced selections carry their proof at the construction site. All edits are semantics-neutral for values that are integers in fact, and the transpiled lane stays green throughout.The one slot that stays undeclared
Model.pastBytesholds 2^53 by design — it exists to probe the boundary where 2^53 and 2^53 + 1 share a wire value, so it cannot also attest staying inside the provable window. A comment at its declaration records this.Follow-up commit
Ten arm slots whose payloads share a lowered record shape (
id,code,pidspellings across sibling arms) initially could not be declared because agreeing declarations on one shape refused; they now coalesce, and the profiles declare them. The same round tightened two other seams: synthesized record slots (audio clocks, the composition cursor) gained compile-time write obligations, so their decode-ingress sites prove in place with the same range-guard-and-trunc idiom the adapters already use, and two profiles dropped asubscriptions_exportnaming a function their entry modules never exported, which now refuses instead of resolving silently.Verification
PARITY_SHOTS-gated screenshot test, which skips in both lanes).integer_slotsdiffs against the transpiled reference list exactly as the residue above — nothing extra, nothing else missing.zig build,zig build test,zig build test-ts-core-e2e, andzig build sidecar-conformanceall pass.This battery does not run in CI. The runners have no external core compiler installed, so the step is a no-op there. It is a local and future-CI harness, not a gate on this pull request.