Add an ARMv8-A (AArch64) backend - #1541
Open
clebreto wants to merge 61 commits into
Open
Conversation
New architecture `-arch armv8a` targeting A64, modeled at the full 64-bit register width (reg_size = U64, X registers only). Coq: - armv8a_decl.v: registers R0..R30/RZR/RSP printed x0..x30/xzr/sp, NZCV flags, 14 condition codes, AAPCS64 calling convention, register shifts (0..63). - armv8a_instr_decl.v: 76 mnemonics with full semantics; each carries its ARM ARM (DDI 0487 M.a) documentation block (C6.2 section, page, summary, syntax and Operation pseudocode). Flag-setting forms are separate mnemonics (ADDS, ...); conditional selection (CSEL family) takes the condition as a first-class operand; loads/stores rely on the framework for the memory access and only extend values; MOVZ/MOVN/MOVK model wide immediate moves. - armv8a.v: NZCV condition evaluation and asm instance. - armv8a_extra.v: swap, add_large_imm and smart_li pseudo-instructions (smart_li expands to MOVZ/MOVK sequences; A64 has no conditional execution so there is no conditional variant). - armv8a_lowering.v (new): lowering pass; conditions via CMP/TST and NZCV, word conditional expressions via CSEL, large ADD/SUB immediates via add_large_imm, shifted-operand fusion. - armv8a_params_core.v, armv8a_params.v, armv8a_stack_zeroization.v: compiler passes parameters at U64. - arch_decl.v: new CAimmC_armv8a_shift_amount and CAimmC_armv8a_0_16_32_48 immediate checkers (other architectures reject them). OCaml: - pp_arm_v8a.ml: GNU/ELF AArch64 printer; W-register forms for narrow loads/stores, extensions and 32-bit multiplies; ADRP/ADD :lo12: for global addresses; b.cc branches and ret-based returns. - coreArchFactory retargeted to Armv8a_* modules; callstyle returns via X30. Docs: compiler/doc/armv8a_isa_docs.json machine-readable extraction of the ARM ARM instruction documentation (recording the PDF edition and hash of the source document). Tests: 14 test programs under tests/success/armv8a, wired as the `armv8a` check category (compiled, assembled with llvm-mc --triple=aarch64 and linked with ld.lld). Correctness proofs are deferred; every semantics function is total and the extraction cone contains no admitted statement.
Data-processing instructions, comparisons, conditional selection, moves and loads/stores now exist in both the 64-bit (X) and 32-bit (W) forms, selected by the new [opts_size] instruction option (intrinsic suffix _32, e.g. #ADD_32). W-form destinations zero the upper 32 bits ([MSB_CLEAR]) as in the architecture. The lowering pass lowers word operations at both sizes, including 32-bit comparisons, CSEL, MOVZ/MOVK immediate materialization, register-to-register sign/zero extensions (SXTB/SXTH/SXTW/UXTB/UXTH/UXTW) and narrow zero/sign-extending loads. Fixed-size instructions (UMULL, SMULH, ADR, LDRSW, REV32, ...) are only valid in the X form. The shared CAimmC_armv8a_shift_amount immediate checker takes the operand size (shift amounts are 0..31 in the W form).
Fixes the codegen "blind spots" that made real AArch64 output fault at run time, and documents each modeling decision against the spec. Register model (armv8a_decl.v): - Drop XZR from the register set. Field value 31 is the zero register in the X[] accessor (reads zero, ignores writes), so allocating it is unsound; it was producing `mov sp, xzr`. Like RISC-V's x0, omit it and emit ZR-operand ops (CMP, NEG, TST, ...) as dedicated mnemonics. - Drop x18: it is the platform register, reserved on Apple/Windows/SCS Linux where the OS may clobber it asynchronously (invisible to Jasmin's clobber analysis), which corrupted the saved stack pointer. Stack pointer (armv8a_params.v): - Round every frame allocation to 16 bytes and never re-align a frame to less than 16, so SP stays quadword-aligned across nested calls (AArch64 raises an SP Alignment exception otherwise). - Restore a spilled SP via a scratch register + MOV, since A64 LDR cannot target SP (its result goes through the X[] accessor, where 31 = ZR). Each decision is sourced (Arm ARM DDI0487M.a B1.2/D1.4.10.2, AAPCS64, Apple platform ABI) in the inline comments and in the new compiler/doc/armv8a_register_model.md. Validated: ML-DSA-65 compiled with -arch armv8a assembles cleanly and passes the full formosa-mldsa KAT suite (NIST DRBG, PQC, Wycheproof) natively on arm64.
Add armv8a_params_core_proof.v, mirroring arm_params_core_proof.v, with the sem_fopn_args correctness lemmas for the single-instruction core builders used by stack handling and immediate materialization: add, addi, sub, subi, mov, andi (the AND behind align), plus the smart_mov combinator. All proven, no admits. One AArch64-specific wrinkle vs ARMv7-M: SUB/AND semantics use word-scope operators (sub_word / wand) that are not definitionally equal to the ring operators in the lemma statements, so the proofs bridge with sub_wordE (ADD is fine since add_word is defeq to ring add). Deferred (documented in the file header): li and the gen_smart_opi / smart_addi / smart_subi combinators built on it. AArch64 li emits a variable-length MOVZ/MOVN/MOVK sequence over up to four 16-bit halves of a 64-bit register, whose correctness needs bit-level decomposition lemmas that do not port from ARMv7-M's fixed MOV/MOVT (two-halfword) materialization.
Add armv8a_params_common_proof.v, mirroring the portable part of arm_params_common_proof.v. Lifts the core sem_fopn_args results through the to_opn/Oarmv8a wrapper to the generic linear semantics: - sem_fopn_equiv / sem_fopns_equiv: the Oarmv8a-tagged op runs exactly as the core builder; - mov / addi / subi / align at sem_fopn_args level, and their eval_instr forms (the single-instruction builders used by allocate/free_stack_frame and set_up_sp_register); - armv8a_align_mask: the AND mask Z_mod_lnot (wsize_size al - 1) equals -wsize_size al modulo the register base, so align computes exactly align_word (proved via wrepr_wnot + ZlnotE). All proven, no admits. As in armv8a_params_core_proof.v, the li-based smart_* combinators remain deferred (AArch64 MOVZ/MOVK materialization; see that file's header).
Document why the two shift-amount checkers in caimm_checker_s carry different arguments (shift_kind for AArch32, wsize for AArch64), with verbatim spec sources: - shift_kind.v [shift_amount_bounds]: AArch32 amount range is type-dependent (LSL 0..31, LSR/ASR 1..32, ROR 1..31), from DecodeImmShift (Arm ARM DDI0487M.a, J1.2.3.7, p. J1-16079): LSR/ASR encode jasmin-lang#32 as imm5=0 and ROR #0 is RRX, so only LSL admits 0. - armv8a_decl.v [check_shift_amount]: AArch64 amount range is width-dependent and type-independent, [0, datasize), from the C6.2 shifted-register decode (p. C6-1813): shift_amount = UInt(imm6), datasize = 32 << UInt(sf), and "if sf == '0' && imm6<5> == '1' then UNDEFINED". - arch_decl.v: note at the caimm_checker_s constructors explaining the axis each is keyed on and pointing to the two predicates. Comment-only.
Replace the permissive CAimmC_none immediate checkers with predicates grounded in the Arm ARM (DDI 0487 M.a): - CAimmC_armv8a_arith_imm: imm12, optionally LSL jasmin-lang#12 (C6.2.5), for ADD/ADDS/SUB/SUBS/CMP/CMN. Same predicate as is_arith_small, which now aliases it. - CAimmC_armv8a_bitmask_imm: logical bitmask immediates (DecodeBitMasks), for AND/ANDS/ORR/EOR/TST. Executable check: replication tested as invariance under rotation by the element size, the element tested as a rotated run of ones over all (bounded) rotations. - CAimmC_armv8a_mov_imm: MOV alias immediates (wide, inverted wide, or bitmask; C6.2.192-194). - BIC/BICS and MVN have no immediate form in A64: register-only now. Non-encodable immediates (e.g. and x, x, #8380417) are now rejected at assembly generation with an error naming the constraint, instead of emitted as assembly the assembler refuses. Also settle the smart_li_args FIXME: rejecting sizes other than U64/U32 is by design (the only A64 operand widths with MOVZ/MOVK forms).
Discharge the central proof blocker of the ARMv8-A backend: correctness of ARMv8AFopn_core.li and the gen_smart_opi combinators built on it. Word level (ws-generic, reusable at U32 for the Oarmv8a_smart_li assembly-generation proof later): - wbit_n_add: bit-splitting of an n-aligned sum, requiring only that the sum fits the word (the ARMv7-M analog needs 2^n * 2^n <= wbase, which fails for the high chunks of a 64-bit word). - wor_wrepr_add: OR of an n-aligned value with a value below 2^n is addition. - wand_movk_mask_id: the MOVK keep-mask leaves a value untouched when its bits from the insertion position up are zero. - armv8a_MOVZ/MOVN/MOVK_semiE: closed forms of the wide-move semantics; MOVK inserting chunk c at position sh into a value below 2^sh yields wrepr (2^sh * c + m). Semantic level (register size): - movz/movn/movk sem_fopn_args lemmas. - li_lsem_1: the three-way case split of li (single MOVZ; single MOVN via Z_mod_lnot; general MOVZ + up-to-three conditional MOVK), the general case by the chunk-chain invariant that after treating the chunk at position sh the register holds wrepr U64 (n mod 2^(sh+16)) -- chunks skipped because they are zero preserve the invariant for free (z_mod_recombine). - gen_smart_opi_sem_fopn_args, ported from ARMv7-M now that li is available, and the ARMv8AFopnP lifts smart_addi/smart_subi and their _tmp variants in armv8a_params_common_proof.v.
…acle The linearization correctness specs (sf_correct, set_up_sp_register_correct) require lip_allocate/free_stack_frame to adjust SP by exactly the size they are given and set_up_sp_register to align by exactly the frame alignment, for any size — so the round_up_16 wrapping and the U128 alignment bump inside the ARMv8-A linearization params were unprovable as stated. Keep the params spec-exact and enforce the architectural invariant (SP alignment checking, Arm ARM DDI0487M.a D1.4.10.2) where frame shapes are decided instead: - Arch_full.Core_arch gains sp_min_align (U128 on armv8a, U8 elsewhere). - stackAlloc.ml raises every stack-using function's final alignment to sp_min_align (both the subroutine and export paths, next to the existing stack-zeroization bump). Frame sizes are rounded up to the frame alignment (stack_frame_allocation_size), so every SP adjustment becomes a multiple of 16 and the platform-guaranteed entry alignment is preserved across calls. Functions with no stack footprint keep their alignment so exports can still use SavedStackNone (which requires sf_align = U8). - armv8a_params.v: drop round_up_16 and the set_up_sp_register alignment bump; document the invariant's new home. Validated: emitted code aligns an 8-byte frame to 16 and ANDs SP with ~15 in the export prologue; all 14 armv8a tests pass; formosa-mldsa KATs pass for all three parameter sets.
New armv8a_params_proof.v, mirroring arm_params_proof.v: Stack alloc (complete, armv8a_hsaparams record built): - armv8a_mov_ofsP: the full ADR/LDR/MOV/ADD/shifted-ADD/add_large_imm/STR case analysis over mk_lea, ported from ARMv7-M (the two mov_ofs definitions are structurally identical) with the AArch64 semi unfoldings. - armv8a_immediateP: the Oarmv8a_smart_li sopn semantics is the identity, so this is immediate. - armv8a_swapP. Linearization (9 of 10 obligations): - allocate/free_stack_frame via the smart_subi/addi_tmp lemmas (tmp case) and the plain subi/addi lemmas (no-tmp case), now that the definitions are spec-exact (no rounding). - set_up_sp_register: sub-align-mov-mov chain over abstract var_i's. - lmove, lstore, lload; lstores via the generic lstores_imm_dfl_correct plus ladd_imm correctness of ARMv8AFopn_smart_addi. - lip_tmp <> lip_tmp2 and check_ws; ok_lip_tmp/tmp2 (X16/X17). - h_lower_addressing_params (identity on armv8a). Still missing: lloads_correct for the custom armv8a_lloads (SP restored through X17 + MOV since LDR cannot target SP) -- the last field of h_linearization_params -- then the lowering, asm-gen and stack-zeroization proofs before h_architecture_params can be assembled.
Prove lloads_correct for the custom armv8a_lloads and assemble the full h_linearization_params record. armv8a_lloads restores the saved stack pointer through the scratch register X17 and a MOV, since an A64 load writes through the X[] accessor for which register number 31 is ZR, not SP. The proof: - lloads_foldM_eq_ex: a restore foldM only modifies the variables it sets (induction over the restore list). - hsp: the SP-restoring tail, proven from any varmap holding the old SP, covering both the LDR-with-small-offset form and the smart_addi-through-X17 form, by direct computation of the LDR/MOV semantics. - The register-restore prefix by the generic lloads_aux_correct for the small-offset branch, and for the rebased branch an induction relating the specification's foldM (offsets from the old SP) to the rebased foldM (offsets from X17 = SP + ofs0), mirroring lloads_imm_dfl_correct's inner induction. Proof-engineering notes (the goals mix two convertible elaborations of the same instances: the asm_opI flavor from armv8a_params.v definitions and the _asmop-of-sip flavor from linearization_proof.v): cross-flavor facts cannot be rewritten directly; they are bridged with occurrence patterns folded by kernel conversion (rewrite -[X in ..]/(..)), exact:-checked restatements, and a generic bind_ok_estate/foldM_1 pair to reduce binds without simpl (whose over-reduction breaks matching).
Condition assembly (the NZCV/condition-code model): - condt_of_rflagP, condt_notP, condt_andP, condt_orP against armv8a_eval_cond, by exhaustive flag-boolean case analysis (the A64 cond-code table, C1.2.4), and the eval_assemble_cond induction over Fvar/Onot/Obeq(GE-trick)/Oand/Oor, giving assemble_cond_spec. Extra ops (assemble_extra_correct): - Oarmv8a_swap: the three-EOR sequence, via assemble_opsP. - Oarmv8a_add_large_imm: via the smart_addi correctness lemma. - Oarmv8a_smart_li at BOTH widths: U64 via li_lsem_1, and U32 via a new li_lsem_1_w32 in armv8a_params_core_proof.v (W-form MOVZ/MOVK chain of at most two chunks, reusing the ws-generic MOVZ/MOVN/MOVK_semiE word lemmas; the 32-bit value lives in the register-typed variable under the withsubword discipline and value_uincl absorbs the upper-bit clearing at the assembly level). - assemble_extra_sz, and the armv8a_hagparams record. Also armv8a_hshp (SLH is empty on armv8a) and armv8a_is_move_opP (MOV/LDR/STR/STRH/STRB all return their input truncated to the output width, proved uniformly over the operand size). Remaining before h_architecture_params: armv8a_lowering_proof.v and armv8a_stack_zeroization_proof.v.
Port arm_stack_zeroization_proof.v (781 lines). The two zeroization strategies (loop and unrolled) and their state-relation invariants carry over almost verbatim since the armv8a code generator mirrors ARMv7-M's structure and the NZCV flag semantics (nzcv_of_aluop) are shared; the differences: - store_zero_eval_instr: armv8a's STR at default_opts is 64-bit even for a 32-bit store (the Store lexpr does the truncation), so the ARM store_mn_of_wsizeP shape does not apply; proven by four-way case computation over the store width, now up to U64 (the ws <= U32 bound becomes ws <= U64 throughout, matching the armv8a command's assert). - fopn_li/fopn_movi/fopn_sub eval_instr lemmas proven locally (the armv8a wrappers live in armv8a_stack_zeroization.v itself; fopn_li is the Oarmv8a_smart_li pseudo-instruction whose sopn semantics is the identity -- its MOVZ/MOVK expansion is the already-proven assembly-generation lemma). armv8a_params_proof.v gains armv8a_hszparams. Eight of the ten h_architecture_params fields are now proven; only the lowering proof (hap_hlop) remains.
Add armv8a_lowering_proof.v (lower_callP and it_lower_callP) and build the full armv8a_h_params : h_architecture_params armv8a_params record: all ten fields are now proven. The proof is a port of arm_lowering_proof.v, generalized from ARM's single register width to the W (U32) and X (U64) forms: chk_ws_reg yields a width disjunction rather than an equation, so the operand width stays abstract and the operator resolution peels the per-operator width asserts instead of enumerating wsizes. Goal-number-based tactic selectors from the ARM proof are replaced by mnemonic-dispatched branches, which are insensitive to the goal count and order. armv8a-specific differences from the ARM proof: - Pif is lowered to CSEL (A64 has no conditional execution), with a direct semantic proof against armv8a_CSEL_semi. - The new large_arith_imm path (64-bit ADD/SUB immediates that do not fit imm12) is proven against Oarmv8a_add_large_imm. - MADD/MSUB replace MLA/MLS, with the product width pinned to the operation width by antisymmetry. - Stores only accept registers (no conditional stores), with the narrow-store accumulator width bump. - lower_mulu and the shifted three-operand class do not exist on A64 and are dropped; the shiftable unop class covers MVN and NEG. Fix a soundness gap in the shift lowering found while proving it: armv8a_shift_semi reduces the shift amount modulo the operand size (faithful to A64 register shifts), but Jasmin's source shifts clamp it, so the two disagree for amounts >= the operand size. Olsr/Olsl/Oasr now only lower compile-time-constant amounts in [0, wsize), matching the constant-only discipline of Orol and get_arg_shift; in-range constant shifts compile unchanged, while variable logical shifts (previously silently miscompiled for out-of-range amounts) are rejected. Rotates are unaffected since rotation is periodic.
Generalize the shift-amount discipline from constant-only to the x86 and RISC-V design: a logical/arithmetic shift amount is accepted if it is either a compile-time constant in [0, wsize) or an expression explicitly masked to the operand size (a & (wsize_bits - 1)). In the masked case the mask is dropped, since the A64 register shifts already reduce the amount modulo the operand size; on that range the hardware modulus and Jasmin's clamping source semantics coincide, which check_shift_exprP proves (via wand_modulo). This restores idiomatic variable shifts, x = y >> (n & 63), while keeping unmasked variable shifts a compile-time error rather than the silent miscompilation they used to be. The armv8a shift test is updated to the masked idiom. Validated: full proofs build, the armv8a test suite, and the ML-DSA KATs for all three parameter sets with the rebuilt compiler.
The backend supports both the X (u64) and W (u32) register forms and the correctness proofs are width-generic, but every test exercised u64 only. Add a u32 test covering the lowered surface at the W width: immediate materialization (MOVZ/MOVK sequences and bitmask immediates), additions and subtractions with imm12 (optionally shifted) and shifted-register operands, MUL/MADD/MSUB, UDIV/SDIV, the logical operations with 32-bit bitmask immediates, constant and masked-variable shifts, rotations by a constant and by a register, conditional selection for the four condition kinds, and 32-bit loads and stores including the narrow extending forms and stack slots. Validated beyond compilation: the generated W-form assembly was executed natively (arm64 macOS) against an independent C reference over multiple input vectors, including shift amounts beyond the operand size going through the mask, with all checks passing.
The ARMv8-A stub of the safety analyzer returned true, silently claiming every program safe. Raise a proper compilation error instead.
The same code and comment appeared twice (subroutine and export blocks); introduce enforce_sp_min_align.
Add -sp-min-align to override the per-architecture default (Core_arch.sp_min_align: u128 on armv8a, u8 elsewhere).
AArch32 and AArch64 have the same flag register: move rflag (with its instances and printer) and the flag-combination description out of arm_decl/armv8a_decl into a new arm_common module that both re-export.
The A64 condition codes are those of AArch32 (minus the always-true AL/NV, which are deliberately not modeled on either architecture: an unconditional instruction simply has no condition operand). Move condt and its instances/printer to arm_common.
arm_eval_cond and armv8a_eval_cond were identical; keep a single definition next to the shared condt type.
The alias forms ASR/LSL/LSR/ROR already accept both the register and the immediate shift amount (ak_rrr ++ ak_rr_imm_shift) with the same semantics, so the V forms were dead duplicates: the lowering only ever emits the alias mnemonics.
Pair each assembly argument with the width of the register form to print (W registers for the sources of the extensions, long multiplies and zero-extending narrow loads/stores), as x86 does, instead of patching the printed form position-by-position in the OCaml printer. Remove wform_positions: the printer now derives the W form purely from the declared width.
A64 conditions are ordinary last operands (CSEL, CSET, ...), so print them like any other argument instead of returning None and re-appending the condition after a filter_map.
Pure reorganization of armv8a_instr_decl.v, mirroring arm_instr_decl.v: every *_semi (with its ISA doc block) now sits right before the instruction description (or family helper) that uses it, so both can be reviewed together.
armv8a_params_core, armv8a_lowering and armv8a_stack_zeroization are dependencies of armv8a_params and are extracted transitively, exactly as for x86/arm/riscv; drop the redundant entries.
Same idiom as JModel_m4; CMP/CMN/TST become the flag-only aliases of SUBS/ADDS/ANDS instead of re-deriving the formulas.
AAPCS64 is the same on Linux, macOS and Windows for everything Jasmin uses, and the only platform-dependent register (x18) is excluded from the register file, so the convention is platform-independent; document this where it is declared.
Proof-using annotations required by 'Default Proof Using=' and the removal of lsem1, missed by the merge commit (the merge-time build reported success spuriously).
armv8a-stack-zero-loop and armv8a-stack-zero-unrolled, mirroring the other architectures. The new tests exposed two gaps, fixed here: - store_zero emitted the X form of STR for a 32-bit clear step, which assembly generation rejects; use the W form; - the default clear step is the frame alignment, which sp_min_align raises to u128 on armv8a, beyond what one store can clear; cap the default at the register size.
Add a differential test that checks, for every instruction form modeled in armv8a_instr_decl.v, that the Coq semantics matches native execution. An OCaml generator (compiler/tests/armv8a-hw-semantics/, linked against the extracted model) enumerates every mnemonic at both operand sizes (and the encodable shifted-register variants), evaluates id_semi on edge-case and fixed-seed pseudo-random operand vectors via app_sopn, and emits a C program that runs the same instructions with inline assembly and compares result words and NZCV flags (mrs/msr nzcv); loads and stores run against a scratch buffer. Every mismatch is reported and the program exits nonzero. Run with 'make -C compiler check-armv8a-semantics' on an AArch64 host: 748 instruction forms, 33544 checks, 0 failures. The only untestable mnemonic is ADR (PC-relative address formation, whose id_semi is the identity on an address computed by the framework); all other skips are non-encodable operand combinations, documented in the generator and in the header of the generated C file.
New JModel_arm holds the 32-bit operations whose semantics coincide on AArch32 and AArch64 (arithmetic and its flags, comparisons, result-only logical, multiplication, division, CLZ, REV/REV16, bit fields, loads and stores), using JModel_m4's exact formulations. JModel_m4 re-exports it and abbreviates the bare AArch32 names (abbrev [-printing] ADD = ADD_32, ...); JModel_armv8a re-exports it and keeps only the 64-bit forms and the AArch64-specific operations (flag-setting logical instructions, shifts, extensions, conditional selection, ...).
The DOIT/DIT classification used by jasmin-ct --doit was kept in
hand-written OCaml tables (is_doit_asm_op / is_doit_asm_extra in
{x86,arm,riscv}_arch_full.ml), disconnected from the instruction
descriptions.
Move this information into the descriptors:
- add a boolean field id_doit to arch_decl.instr_desc_t and a
corresponding field i_doit to sopn.instruction_desc; base ops forward
id_doit to i_doit (arch_extra.get_instr_desc);
- x86: the per-operator classification is transcribed from the OCaml
table into x86_op_is_doit and stamped into the descriptor by
x86_instr_desc;
- arm: every instruction description sets id_doit, transcribing the
per-mnemonic OCaml table; mk_cond, mk_shifted and idt_dropn preserve
the field;
- riscv: all instructions are classified as DOIT, as before;
- extra operators (x86_extra, arm_extra, riscv_extra) are all
classified as DOIT, as in the OCaml tables; pseudo and SLH operators
are classified as DOIT, which matches the CT checkers that treat
them as constant-time;
- delete the OCaml tables; Arch.is_ct_sopn ~doit:true now reads i_doit
from the instruction descriptor.
The classification is unchanged.
The width-generic MADD/MSUB proof was missing wopp_zero_extend (the subtraction unfolds to an addition of the opposite), and the failure was masked by reading a piped build status; also complete the Proof using annotations of the file.
…ands Address review feedback on the argument kinds of shifted instructions. On A64 a shifted operand exists only in the register form of an instruction: the immediate forms admit either no shift at all (logical instructions, whose bitmask immediate is checked by CAimmC_armv8a_bitmask_imm) or only LSL #0/LSL jasmin-lang#12, which is part of the immediate encoding itself and folded into CAimmC_armv8a_arith_imm. mk_shifted used to append the shift-amount operand to every alternative of the base instruction, relying on the argument-kind builders to have dropped the immediate alternatives beforehand. Make the distinction where it belongs: mk_shifted now keeps only the register alternatives of the base instruction and appends the shift amount to those, and the ak_rr_or_imm/ak_rrr_or_imm builders always list the immediate alternative unconditionally. Validated: full proofs build, extraction, compiler build, the armv8a test categories, and the ML-DSA KATs for the three parameter sets.
The arithmetic instructions (ADD/ADDS/SUB/SUBS/NEG/CMP/CMN) only admit LSL, LSR and ASR on their shifted-register operand; ROR is reserved (C6.2.5 "ADD (shifted register)"). Only the logical instructions admit all four shifts (C6.2.14 "AND (shifted register)"). The lowering used to fuse a rotation into any shift-taking instruction, so x + (y >>r 3) compiled to "add x0, x0, x1, ror #3", which assemblers reject. Classify the shift kinds per mnemonic (shift_allowed) and enforce the restriction at both levels: - the instruction descriptor rejects the combination: mk_shifted takes the mnemonic and conjoins shift_allowed to id_valid, so the semantics of a rotated arithmetic instruction is a type error rather than a claim the hardware does not honour; - the lowering only fuses an allowed shift (arg_shift and lower_base_op), so a rotated operand of an arithmetic instruction now falls back to the unfused form and surfaces as a compile-time error instead of invalid assembly, while rotations keep fusing into the logical instructions. The with_shift_unop/with_shift_binop lemmas take the corresponding shift_allowed premise, discharged at their call sites by the new lowering guard. Validated: full proofs build, extraction, compiler build, the armv8a test categories, the ML-DSA KATs for the three parameter sets, and native assembly of both directions of the gate (eor/and with ror still fuse and assemble; add with ror is now rejected at compile time).
Address review feedback on the stack-zeroization default clear step: capping it at Arch.reg_size bakes in the assumption that a register store is the widest store the architecture can perform, which stops holding once SIMD stores exist (a 128-bit NEON store on AArch64, a 256-bit YMM store on x86-64). Add a max_store_size field to the Arch module giving the widest single-instruction store and use it for the cap instead, so the default step follows the architecture's actual store capability.
Address review feedback: MVN has no immediate form (it is an alias of ORN (shifted register); writing a bitmask immediate goes through the MOV alias of ORR (immediate) instead), so say ak_rr rather than going through ak_rr_or_imm with the no-immediate parameter.
The variable forms (ASRV/LSLV/LSRV/RORV) are not modeled, so their alias plumbing in the ASR/LSL/LSR/ROR documentation (encoding-naming notes, double syntax, pseudocode attribution) was noise; keep the reference, the description and the operation pseudocode.
Reduce the modeled mnemonics from 72 to 43, keeping exactly the instructions that the compiler pipeline can emit: the lowering pass, the load-immediate and smart-address helpers, mov_ofs (ADR), stack zeroization, and pseudo-operation expansion. Dropped: SBC, SBCS, the widening/high multiplies (UMULL, SMULL, UMADDL, SMADDL, UMULH, SMULH), ANDS, BIC, BICS, the bit-field family (BFC, BFI, BFXIL, SBFX, UBFX, EXTR), the bit-manipulation family (RBIT, REV, REV16, REV32, CLZ, CLS), CMN, and the CSEL aliases (CSINC, CSINV, CSNEG, CSET, CSETM). The mnemonic tables (has_shift_mnemonics, ror_shift_mnemonics, sized_mnemonics), the lowering binop list and its proof, the OCaml DIT table, the hardware-semantics generator, and the intrinsics tests are pruned to match. Proofs, extraction, the armv8a test categories, the hardware differential test (21442 checks) and the ML-DSA known answer tests for all three parameter sets remain green.
The CAimmC_armv8a_0_16_32_48 checker accepted shifts 32 and 48 regardless of the operand width, while the W forms of MOVZ/MOVN/MOVK cannot encode them (the hw field has one bit in the W form); the mismatch was only documented as a skip in the hardware-semantics test. Make the checker carry the operand width, like CAimmC_armv8a_shift_amount, and rename it CAimmC_armv8a_halfword_shift: the legal shifts are the multiples of 16 below the operand width. The corresponding skip note disappears from the hardware-semantics generator.
Since the descriptors forbid ROR on the shifted arithmetic instructions (shift_allowed in id_valid), the shift kinds A64 cannot encode are invalid in the model rather than accepted-but-unassemblable, so the documented skip no longer describes a model/hardware gap. Also tighten a CSEL wording left over from the distillation.
…rface Move the five armv8a immediate conditions from the removed shared inductive to an architecture-local armv8a_caimm_cond type, following the caimm_cond interface of arch_decl: eqTypeC instance, checker and error-message printer live in armv8a_decl.v, and the argument kinds wrap the conditions in Some (None being an unconditioned immediate). The other architectures no longer see the armv8a conditions at all.
Set id_doit in every instruction description and i_doit on the extra operators, transcribing the per-mnemonic OCaml table: everything in the modeled set belongs to the A64 DIT instruction list (Arm ARM DDI0487M.a, section C3.2.13) except SDIV, UDIV and ADR. mk_rrr_instr takes the classification as an argument since its users differ (MUL is DIT, the divisions are not); mk_shifted preserves the field. The hand-written is_doit_asm_op / is_doit_asm_extra tables disappear from armv8a_arch_full.ml, as on the other architectures.
lip_lstore and lip_lload now take the width of the transferred value (main commit "Linearization params: make lload and llstore more general"): thread it through armv8a_lstore/armv8a_lload and the custom armv8a_lloads (per-variable width for the restored registers, Uptr for the saved stack pointer), and drop the vtype hypotheses that disappeared from the correctness specifications.
vbgl
reviewed
Aug 26, 2026
tests/success/armv8a/add.jazz at the repository root is a byte-identical duplicate of compiler/tests/success/armv8a/add.jazz, staged from the wrong directory in the initial backend commit; nothing references it (the test runner resolves its paths relative to compiler/).
vbgl
reviewed
Aug 26, 2026
Comment on lines
+257
to
+262
| "-sp-min-align", | ||
| Arg.Symbol (List.map fst Annot.ws_strings, set_sp_min_align), | ||
| " Minimal alignment kept by the stack pointer across calls (default \ | ||
| depends on the target architecture: u128, i.e. 16 bytes, on armv8a; \ | ||
| no constraint otherwise). Lowering it below the architectural \ | ||
| requirement may produce faulting code"; |
Member
There was a problem hiding this comment.
What is the purpose of this option?
Contributor
Author
There was a problem hiding this comment.
From what I understand, it's only useful in marginal cases: lowering the alignment on a platform where the OS has disabled SP alignment checking (SCTLR_ELx.SA0) in order to reclaim the stack padding, or raising it for experimentation purposes.
Since it is really hypothetical for me, this can be removed for now, as long as we keep the enforce_sp_min_align which is compulsory for armv8a.
vbgl
reviewed
Aug 26, 2026
vbgl
reviewed
Aug 26, 2026
Armv7-M guarantees that stack pointer values are at least 4-byte aligned: writes to SP force bits [1:0] to zero (Arm v7-M Architecture Reference Manual, B1.5.7). With no minimal alignment, a function whose frame is only 1- or 2-byte aligned lets the export prologue write a non-4-byte-aligned SP (BIC #1 on the aligned copy), which the hardware silently rounds, shifting every subsequent SP-relative access. Set sp_min_align to U32 for arm-m4 so such frames are padded to 4 bytes. The instack function of tests/success/common/unaligned.jazz asserted the computed alignment with #[stackalign=u16], which is now architecture-dependent; move it to per-architecture copies (unaligned_stackalign.jazz): u16 on x86-64 and risc-v, u32 on arm-m4 (failing before this change), and u128 on armv8a.
The doit/not_doit aliases in arch_decl.v were a leftover of the pre-squash version of the DOIT-in-descriptors branch this work was based on; the version merged on main writes the constructors directly. Drop the aliases and follow suit, leaving arch_decl.v untouched by this branch.
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
3 participants
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.
New architecture
-arch armv8atargeting A64 (AArch64), modeled at the full 64-bit register width.arm_common), 43 mnemonics — exactly the set the compilation pipeline can emit (lowering, load-immediate and smart-address helpers,mov_ofs, stack zeroization, pseudo-op expansion). Each instruction carries its ARM ARM (DDI 0487 M.a) documentation block, and the DIT classification lives in the descriptors (id_doit), everything being DIT except SDIV/UDIV/ADR.caimm_condcheckers (arith imm12, bitmask immediates, MOV-alias immediates, shift amounts, MOVZ/MOVN/MOVK halfword shifts restricted per operand width).h_architecture_paramshypotheses are proved; the extraction cone contains no admitted statement.-sp-min-align(SP stays 16-byte aligned across calls, with a custom epilogue restore since an A64 LDR cannot target SP).armv8aand stack-zeroization check categories; a hardware differential test (make -C compiler check-armv8a-semantics, AArch64 hosts only) compares the extractedid_semiof every instruction form against the silicon — currently 509 forms / 21442 checks.Validated end to end by compiling the ML-DSA reference implementations (formosa-mldsa) for the three parameter sets and running the full KAT suites.
Previous review round
A first round by @bgregoir happened on the fork: clebreto#5. Summary of the points and their resolutions:
compiler/doc/extract_armv8a_isa_docs.py) — removed from tracking and history.CAimmC_armv8a_halfword_shift) and rejects 32/48 in the W form.shift_allowedinid_valid).jasmin_checksafety.mlerror reporting "should go in a separated PR" — moved out (jasmin-checksafety: report analysis-time errors cleanly clebreto/jasmin#6); only the armv8a stub change insafetyMain.mlstays (error out instead of claiming safety).check-print-roundtripscript "can go to a separated PR" — moved out (Add a check-print-roundtrip test script clebreto/jasmin#7); thearmv8a-print-roundtripcategory left with it.