scry #290

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:

  • 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.