id: VCR-RA-010
type: sw-req
title: "scry → synth: sound AI annotations as untrusted regalloc oracle + soundness-bearing narrowing pass"
description: >
synth consumes scry's sound over-approximation (range / known-bits /
reachability lattices over fused Core-Model modules emitted by meld) at two
distinct trust levels, kept architecturally separate so scry's soundness is
load-bearing in exactly one of them.
(A) UNTRUSTED ORACLE — regalloc quality. scry annotations feed
rematerialization candidate selection (constants, constant-offset address
computations, cheap pure functions of still-live values), spill-cost
pricing (Cortex MOV / MOVW+MOVT / literal-pool costs derived from the known
constant), coalescing, split placement, and liveness pruning via
constant-condition dead-edge elimination. These are HINTS. VCR-RA-003
re-derives liveness/interference from the IR and validates the assignment,
so nothing scry asserts enters the TCB: a wrong or adversarial annotation
degrades code quality, never correctness. scry is NOT a proof dependency on
this path.
(B) SOUNDNESS-BEARING — narrowing rewrite, BEFORE regalloc. Where scry
proves an i64's observable range fits 32 bits (or only the low half is
read), synth carries it in a single GP register and synthesizes the high
half on demand — halving pressure for that value on 32-bit Cortex. This is
a program rewrite, not an allocation knob; it cannot ride the untrusted
channel. Each narrowing carries its own discharged refinement obligation in
the Rocq substrate (or an equivalently-trusted local check); no narrowing
fires without it. scry's soundness IS load-bearing here, but the assurance
surface is one localized refinement check, not the whole interpreter pulled
into the TCB Verasco-style.
This is the same sound engine that staffs PulseEngine's third DO-333
technique class — sound static analysis, alongside the deductive-proof and
BMC layers. The synth consumer is one client of scry's analysis; the DO-333
verification role (and the phase-2 lift to Component-Model properties) is
another, served by the same lattices.
Relationship to VCR-DEC-001: path (A) is a candidate to close part of the
VCR-RA-001 revisit-trigger cycle gap WITHOUT porting regalloc3's bundle
model, since the regalloc2 transition win came from split/remat
sophistication, which scry sharpens directly.
status: proposed
tags: [codegen, register-allocation, scry, abstract-interpretation, do-333, track-a]
links:
- type: derives-from
target: VCR-001
- type: refines
target: VCR-RA-001
- type: relates-to
target: VCR-DEC-001
- type: depends-on
target: SCRY-001 # scry annotation schema + soundness statement
fields:
req-type: functional
priority: should
verification-criteria: >
(A) Annotation-fuzzing test: under arbitrary/corrupted scry annotations,
VCR-RA-003 still accepts and observable behaviour is identical to the
no-annotation build — only cycle counts move. This is the evidence that
path (A) sits outside the TCB.
(B) CI fails on any narrowing rewrite emitted without a corresponding
discharged refinement obligation.
(C) At VCR-RA-001 acceptance (v0.11.40 gate): release notes report the
measured cycle-gap delta attributable to scry-driven remat + narrowing,
feeding the VCR-DEC-001 revisit decision.
I got an idea you should investigate directly formulated as req
id: VCR-RA-010
type: sw-req
title: "scry → synth: sound AI annotations as untrusted regalloc oracle + soundness-bearing narrowing pass"
description: >
synth consumes scry's sound over-approximation (range / known-bits /
reachability lattices over fused Core-Model modules emitted by meld) at two
distinct trust levels, kept architecturally separate so scry's soundness is
load-bearing in exactly one of them.
(A) UNTRUSTED ORACLE — regalloc quality. scry annotations feed
rematerialization candidate selection (constants, constant-offset address
computations, cheap pure functions of still-live values), spill-cost
pricing (Cortex MOV / MOVW+MOVT / literal-pool costs derived from the known
constant), coalescing, split placement, and liveness pruning via
constant-condition dead-edge elimination. These are HINTS. VCR-RA-003
re-derives liveness/interference from the IR and validates the assignment,
so nothing scry asserts enters the TCB: a wrong or adversarial annotation
degrades code quality, never correctness. scry is NOT a proof dependency on
this path.
(B) SOUNDNESS-BEARING — narrowing rewrite, BEFORE regalloc. Where scry
proves an i64's observable range fits 32 bits (or only the low half is
read), synth carries it in a single GP register and synthesizes the high
half on demand — halving pressure for that value on 32-bit Cortex. This is
a program rewrite, not an allocation knob; it cannot ride the untrusted
channel. Each narrowing carries its own discharged refinement obligation in
the Rocq substrate (or an equivalently-trusted local check); no narrowing
fires without it. scry's soundness IS load-bearing here, but the assurance
surface is one localized refinement check, not the whole interpreter pulled
into the TCB Verasco-style.
This is the same sound engine that staffs PulseEngine's third DO-333
technique class — sound static analysis, alongside the deductive-proof and
BMC layers. The synth consumer is one client of scry's analysis; the DO-333
verification role (and the phase-2 lift to Component-Model properties) is
another, served by the same lattices.
Relationship to VCR-DEC-001: path (A) is a candidate to close part of the
VCR-RA-001 revisit-trigger cycle gap WITHOUT porting regalloc3's bundle
model, since the regalloc2 transition win came from split/remat
sophistication, which scry sharpens directly.
status: proposed
tags: [codegen, register-allocation, scry, abstract-interpretation, do-333, track-a]
links:
target: VCR-001
target: VCR-RA-001
target: VCR-DEC-001
target: SCRY-001 # scry annotation schema + soundness statement
fields:
req-type: functional
priority: should
verification-criteria: >
(A) Annotation-fuzzing test: under arbitrary/corrupted scry annotations,
VCR-RA-003 still accepts and observable behaviour is identical to the
no-annotation build — only cycle counts move. This is the evidence that
path (A) sits outside the TCB.
(B) CI fails on any narrowing rewrite emitted without a corresponding
discharged refinement obligation.
(C) At VCR-RA-001 acceptance (v0.11.40 gate): release notes report the
measured cycle-gap delta attributable to scry-driven remat + narrowing,
feeding the VCR-DEC-001 revisit decision.