Skip to content

CI: wire the gpio_thin_846 differential — the #846 size+execution headline is not CI-enforced #879

Description

@avrabe

scripts/repro/gpio_thin_846_differential.py is not referenced anywhere in .github/workflows/ci.yml, so the #846 result is only ever checked by hand.

That matters because it is a headline claim of two releases now:

  • v0.50.1 flipped SYNTH_SHIFT_MASK_ELIDE default-on (534 → 506 B)
  • v0.52.0 added the cross-block reaching-def (506 → 502 B / 3 residual masks)

and the same script also executes 75 mmio traces vs wasmtime including pin ≥ 32 — the mod-32 boundary where a wrong elision shows up. So the gate that would catch an unsound shift-mask elision on gale's real driver runs only when someone remembers to run it.

Pre-existing (it was never wired, not dropped by the v0.52 assembly merge); surfaced by the v0.52.0 cold review.

Ask

Wire it into the ARM oracle job alongside the other unicorn differentials. It needs wasmtime, unicorn, pyelftools and capstone (the mask census disassembles .text) — confirm capstone is in that job's pip install line, since several jobs install only the first three.

Assert a NON-ZERO check count as well as PASS: a harness that finds no masks and reports success is the vacuous-gate class this project keeps catching (cf. the llvm-objcopy-missing "0 ops accepted PASS" in the aarch64 matrix).

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions