Skip to content

feat(vcr-isa): AddWithCarry family + flag-free ALU + shifts + moves bridged to Sail/ASL (#242, VCR-ISA-001) #671

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
avrabe merged 1 commit into from
Jul 8, 2026
Merged

feat(vcr-isa): AddWithCarry family + flag-free ALU + shifts + moves bridged to Sail/ASL (#242, VCR-ISA-001) #671

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
24 changes: 23 additions & 1 deletion artifacts/verified-codegen-roadmap.yaml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -617,7 +617,24 @@ artifacts:
Sail memory vs Z->I32 model). RISC-V half unmeasured — sail-riscv's
maintained Coq export may admit the import path there; re-evaluate
separately.
status: proposed

ROUND 2 LANDED (2026-07-08, same day): the spike's priority items (1)
and (2) + the moves stretch — SailArmBridge.v now 81 Qed / 0 Admitted /
0 new axioms covering the FULL AddWithCarry family (ADD/ADDS/CMP +
SUB/SUBS/CMN/RSB + ADC/SBC with live-C carry_in — the i64 pair-codegen
primitives), flag-free ALU (AND/ORR/EOR/MVN), all four shifts in
immediate (1..31) and register (0 < amt < 32; amt = 0 on the unsigned
view) forms via a faithful Shift_C transcription incl. shifter
carry-out, and MOV/MOVW/MOVT. Measured cost ~0.5 day for six-plus
classes (well under the spike's per-class estimate; the flag-machinery
amortization held). BONUS FINDING: the bridge surfaced two latent
hand-model divergences from the ASL (LSR/ASR #32 and register shift
amounts >= 32 — unreachable from Compilation.v since WASM masks to
0..31), documented in-file as gaps 6-7 — the exact bug class this item
exists to surface. Still open (why not implemented): PC-indexed
executor (the trap-guard admits, this item's core motivation),
MUL/UMULL/CLZ/RBIT/memory/branches, and the whole RISC-V half.
status: approved
tags: [semantics, sail, isa, trust, rocq, track-b, unblocks-admits]
links:
- type: derives-from
Expand All @@ -643,6 +660,11 @@ artifacts:
transcribe-and-bridge against provenance-pinned Sail source, not
against an imported generated model. RV32 export build remains
unmeasured (the spike's ARM no-go on import does not transfer).
STATUS proposed -> approved (2026-07-08): two landed increments
(23 then 81 Qed, //coq:verify_proofs green) validate the revised
criterion's method on the i32 straight-line integer core; approved
means the approach is committed, NOT that the item is implemented —
the PC-executor refactor, memory ops, and the RISC-V half remain.

- id: VCR-WASM-001
type: sw-req
Expand Down
8 changes: 5 additions & 3 deletions coq/BUILD.bazel
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -73,9 +73,11 @@ rocq_library(
deps = [":arm_semantics"],
)

# VCR-ISA-001 spike (#242): Sail/ASL-derived semantics bridge — AArch32
# ADD/ADDS/CMP (register) transcribed from rems-project/sail-arm with
# line-level provenance, proven ≡ ArmSemantics.v on registers + NZCV.
# VCR-ISA-001 (#242): Sail/ASL-derived semantics bridge — the AArch32
# integer core (AddWithCarry family ADD/ADDS/CMP/SUB/SUBS/CMN/RSB/ADC/SBC,
# flag-free ALU AND/ORR/EOR/MVN, LSL/LSR/ASR/ROR imm+reg via Shift_C,
# MOV/MOVW/MOVT) transcribed from rems-project/sail-arm with line-level
# provenance, proven ≡ ArmSemantics.v on registers + NZCV.
rocq_library(
name = "sail_arm_bridge",
srcs = ["Synth/ARM/SailArmBridge.v"],
Expand Down
Loading
Loading