Feature/armv8a distilled

.gitlab-ci.yml

@@ -5,7 +5,7 @@ stages:
 - test
 - deploy
 
-image: nixos/nix:2.24.15
+image: nixos/nix:2.34.8
 
 variables:
   EXTRA_SUBSTITUTERS: https://jasmin.cachix.org
@@ -219,7 +219,7 @@ libjade:
   stage: test
   parallel:
     matrix:
-      - PRIMITIVE: [ mldsa, mlkem, xmss ]
+      - PRIMITIVE: [ curve25519, mldsa, mlkem, xmss ]
   variables:
     EXTRA_NIX_ARGUMENTS: --arg ocamlDeps true
   extends: .common
@@ -287,7 +287,6 @@ push-compiler-code:
   needs:
   - tarball
   before_script:
-  - nix-env -iA nixpkgs.git
   - nix-env -iA nixpkgs.openssh
   - eval $(ssh-agent -s)
   - mkdir -p ~/.ssh

changes/01-feature/1528-easycrypt-2026_07.md

@@ -0,0 +1,4 @@
+- Extraction as EasyCrypt code targets version 2026.07
+  ([PR #1528](https://github.com/jasmin-lang/jasmin/pull/1528)).
+
+

changes/02-bugfix/1520-doit-instr-desc.md

@@ -0,0 +1,3 @@
+- Fix the DOIT classification of AVX instructions `VPMINS` and `VPMAXS` (not
+  doit for 32-bit elements)
+  ([PR 1520](https://github.com/jasmin-lang/jasmin/pull/1520/)).

changes/02-bugfix/1529-vpsllv-vpsrlv-16.md

@@ -0,0 +1 @@
+- `VPSLLV` and `VPSRLV` no longer accept 16 bits as a size.

compiler/Makefile

@@ -10,11 +10,14 @@ CHECKCATS ?= \
 	x86-64-Intel \
 	x86-64-nolea \
 	arm-m4 \
+	armv8a \
 	risc-v \
 	x86-64-stack-zero-loop \
 	x86-64-stack-zero-unrolled \
 	arm-m4-stack-zero-loop \
 	arm-m4-stack-zero-unrolled \
+	armv8a-stack-zero-loop \
+	armv8a-stack-zero-unrolled \
 	risc-v-stack-zero-loop \
 	risc-v-stack-zero-unrolled \
 	CCT CCT-DOIT SCT
@@ -33,7 +36,7 @@ DISTDIR ?= jasmin-compiler
 OBELISK ?= obelisk
 
 # --------------------------------------------------------------------
-.PHONY: all CIL check check-ci
+.PHONY: all CIL check check-ci check-armv8a-semantics
 .PHONY: clean install uninstall dist
 
 all:
@@ -56,6 +59,12 @@ check-ec:
 	$(MAKE) -C examples/gimli/proofs
 	$(MAKE) -C examples/extraction-unit-tests
 
+# Differential test of the ARMv8-A instruction semantics (the Coq model of
+# armv8a_instr_decl.v, evaluated through its OCaml extraction) against real
+# hardware execution. Requires an AArch64 (ARMv8-A) host.
+check-armv8a-semantics:
+	$(MAKE) -C tests/armv8a-hw-semantics check
+
 check-all: check
 	dune runtest -f
 

compiler/config/tests.config

@@ -54,6 +54,11 @@ bin = ./scripts/check
 args = -arch riscv
 okdirs = examples/**/risc-v tests/success/**/risc-v tests/success/**/common
 
+[test-armv8a]
+bin = ./scripts/check
+args = -arch armv8a
+okdirs = tests/success/**/armv8a
+
 [test-risc-v-extraction]
 bin = ./scripts/extract-and-check
 args = riscv
@@ -80,6 +85,16 @@ bin     = ./scripts/check
 args    = -arch arm-m4 -stack-zero=unrolled
 okdirs  = tests/success/stack_zeroization/**/arm-m4
 
+[test-armv8a-stack-zero-loop]
+bin     = ./scripts/check
+args    = -arch armv8a -stack-zero=loop
+okdirs  = tests/success/stack_zeroization/**/armv8a
+
+[test-armv8a-stack-zero-unrolled]
+bin     = ./scripts/check
+args    = -arch armv8a -stack-zero=unrolled
+okdirs  = tests/success/stack_zeroization/**/armv8a
+
 [test-risc-v-stack-zero-loop]
 bin     = ./scripts/check
 args    = -arch riscv -stack-zero=loop

compiler/default.nix

@@ -3,8 +3,8 @@ with import <nixpkgs> {};
 stdenv.mkDerivation {
   name = "jasmin-0";
   src = ./.;
-  buildInputs = [ mpfr ppl ]
-  ++ (with ocamlPackages; [ ocaml findlib dune_3 apron angstrom batteries camlidl cmdliner menhir menhirLib zarith yojson])
+  buildInputs = [ dune mpfr ppl ]
+  ++ (with ocamlPackages; [ ocaml findlib apron angstrom batteries camlidl cmdliner menhir menhirLib zarith yojson])
   ;
 
   installPhase = ''

compiler/doc/armv8a_register_model.md

@@ -0,0 +1,144 @@
+# ARMv8-A (AArch64) register model and stack-pointer handling — rationale and sources
+
+This note documents the modeling decisions in the Jasmin AArch64 backend that
+concern the **architecture declaration** (`proofs/compiler/armv8a_decl.v`) and
+the **stack-pointer handling** in the linearization parameters
+(`proofs/compiler/armv8a_params.v`). Each decision departs from a naive "one
+Coq constructor per hardware register" model for a documented architectural or
+ABI reason; the citations below let a reviewer check every claim.
+
+Primary sources:
+
+- **Arm ARM** — *Arm Architecture Reference Manual, A-profile*, Arm DDI 0487M.a
+  (`DDI0487_M.a.a_a-profile_architecture_reference_manual.pdf`,
+  sha256 `c07b1302a3db0c6bc0490808c771d66684ddd5adfb2ef64fd23e6beeb7b22e48`; the
+  same edition and hash recorded in `armv8a_isa_docs.json`). Page ids below are
+  the manual's own `Sn-NNNN` labels.
+- **AAPCS64** — *Procedure Call Standard for the Arm 64-bit Architecture
+  (AArch64)*, Arm IHI 0055F.
+- **Apple** — *Writing ARM64 Code for Apple Platforms*, Apple Developer
+  documentation.
+
+---
+
+## 1. The general-purpose register set
+
+AArch64 has 31 general-purpose registers `R0..R30`, each addressable as a 64-bit
+`X` register or a 32-bit `W` register, plus a dedicated stack pointer `SP`.
+`R30` is the procedure-call link register.
+
+> Arm ARM, **B1.2 "Registers in AArch64 Execution state"**, p. B1-203:
+> "31 general-purpose registers, R0 to R30 ... The X30 general-purpose register
+> is used as the procedure call link register. SP — A 64-bit dedicated Stack
+> Pointer register."
+
+The model keeps `R0..R30` and `RSP`. Two registers that a hardware-faithful
+model might include are deliberately omitted (§2, §3).
+
+## 2. The zero register (XZR/WZR) is not modeled
+
+In an instruction encoding the 5-bit register field value `31` (`0b11111`) does
+**not** name a physical register; its meaning depends on which register accessor
+the instruction uses:
+
+> Arm ARM, **B1.2**, p. B1-206:
+> "For the general-purpose register X[] accessor, register number 31 accesses
+> the zero register, ZR, which reads as zero and ignores writes."
+
+The stack pointer is reached through a **separate `SP[]` accessor**, so the same
+field value `31` means `SP` only for the instructions that select it (ADD/SUB in
+their SP forms, MOV-to/from-SP, and loads/stores that allow `SP` as base).
+
+Consequences for the model:
+
+- Modeling `ZR` as an allocatable register would be **unsound**: a value written
+  to it is discarded and any read returns 0. The register allocator, treating it
+  as ordinary storage, produced code such as `mov sp, xzr` (setting SP to 0).
+- We therefore omit it entirely, exactly as the Jasmin RISC-V backend omits the
+  hardwired `x0`/`zero`. The handful of operations that genuinely need `ZR` as an
+  operand — `CMP` (`SUBS` to `ZR`), `NEG`, `TST`, etc. — are emitted as dedicated
+  assembler mnemonics by the printer, never as writes to a `ZR` register.
+- `RSP` is the single encoding-31 register we keep, and it always denotes `SP`.
+
+## 3. The platform register (x18) is not modeled
+
+`x18` is not an architectural special register; it is reserved by the software
+ABI:
+
+> AAPCS64 (IHI 0055F), *General-purpose registers*: r18 is
+> "The Platform Register, if needed; otherwise a temporary register", and a
+> platform ABI may reserve it.
+>
+> Apple, *Writing ARM64 Code for Apple Platforms*:
+> "The platforms reserve register x18. Don't use this register."
+
+On Apple platforms, under Windows, and under shadow-call-stack Linux, the OS or
+runtime may overwrite `x18` **asynchronously** (i.e. between two instructions of
+otherwise straight-line user code). Jasmin's register allocator chooses the
+register that holds a function's saved stack pointer by proving the program does
+not clobber it (`get_reg_oracle` in `compiler/src/regalloc.ml`); that analysis
+cannot see writes performed outside the program, so it happily picked `x18` and
+the saved SP was corrupted to 0 at run time.
+
+Keeping `x18` out of the allocation pool is the only safe choice across these
+platforms. On a platform where `x18` is a plain temporary this merely forgoes
+one scratch register; correctness is unaffected.
+
+## 4. The stack pointer must stay 16-byte aligned
+
+Whenever `SP` is used as the base of a memory access it must be 16-byte aligned.
+This is an **architectural** check (an exception), not just an ABI convention:
+
+> Arm ARM, **D1.4.10.2 "SP alignment checking"**, p. D1-7135:
+> - rule **RRDMXG**: "When the SP is used as the base address of a calculation,
+>   regardless of any offset applied by the instruction, if bits [3:0] of the SP
+>   are not 0b0000, there is a misaligned SP."
+> - rule **RTFVSM**: "If SP alignment checking is enabled, then the execution of
+>   a load or store using the SP with a misaligned SP generates a synchronous SP
+>   Alignment exception on that load or store."
+> - rule **RSTDYJ**: the check is enabled by `SCTLR_EL1.SA` (EL1),
+>   `SCTLR_EL1.SA0`/`SCTLR_EL2.SA0` (EL0), etc.
+
+The check is enabled for EL0 on the platforms we target. The 16-byte alignment
+of `SP` at public interfaces is also mandated by the AAPCS64 (IHI 0055F, *The
+stack*: "SP mod 16 = 0"), which B1.2 (p. B1-203) cross-references.
+
+Jasmin sizes each stack frame to the alignment of the objects it holds
+(`sao_align`), which for pure 64-bit code is only 8 bytes, so a raw frame size
+need not be a multiple of 16. The backend therefore:
+
+- rounds every frame allocation/deallocation up to a multiple of 16
+  (`round_up_16`, used by `armv8a_allocate_stack_frame` /
+  `armv8a_free_stack_frame`), so nested calls preserve the invariant; and
+- never aligns a re-aligned frame to less than 16 bytes
+  (`armv8a_set_up_sp_register`).
+
+The extra padding lands at the top of the frame and is never accessed.
+
+## 5. The stack pointer cannot be an LDR destination
+
+Because a load writes its result through the general-purpose `X[]` accessor, and
+register number 31 in that accessor is `ZR` (§2), an A64 `LDR` can never write
+`SP`: its destination operand is `<Xt>`, not `<Xt|SP>`. (This differs from
+ARMv7, where R13/SP is an ordinary register that `LDR` can target — which is why
+the shared linearization default, `lloads_imm_dfl`, is fine for the 32-bit Arm
+backend but not here.)
+
+When the saved stack pointer has been spilled to the stack (the usual case for a
+function that saves callee-saved registers), it must therefore be reloaded into
+a scratch register and then copied to `SP` with a `MOV` (which reaches `SP` via
+the `SP[]` accessor). This is what the backend's custom `armv8a_lloads` does: it
+restores the ordinary saved registers first (relative to the still-live `SP`),
+then loads the saved `SP` into `X17` and issues `MOV SP, X17`.
+
+---
+
+### Cross-reference to the code
+
+| Decision | File / definition | Source |
+|---|---|---|
+| Omit `XZR` | `armv8a_decl.v` — `register`, `registers`, `register_to_string` | Arm ARM B1.2, p. B1-206 |
+| Omit `x18` | `armv8a_decl.v` — `register`, `registers`, `armv8a_internal_call_conv` | AAPCS64 IHI 0055F; Apple ABI |
+| Round frames to 16 | `armv8a_params.v` — `round_up_16`, `armv8a_allocate_stack_frame`, `armv8a_free_stack_frame` | Arm ARM D1.4.10.2 (RRDMXG, RTFVSM) |
+| Re-align frames ≥ 16 | `armv8a_params.v` — `armv8a_set_up_sp_register` | Arm ARM D1.4.10.2; AAPCS64 |
+| Restore `SP` via scratch + `MOV` | `armv8a_params.v` — `armv8a_lloads` | Arm ARM B1.2, p. B1-206 |

compiler/entry/commonCLI.ml

@@ -5,7 +5,8 @@ open Utils
 let arch =
   let alts =
     [
-      ("x86-64", Utils.X86_64); ("arm-m4", Utils.ARM_M4); ("riscv", Utils.RISCV);
+      ("x86-64", Utils.X86_64); ("arm-m4", Utils.ARM_M4);
+      ("armv8a", Utils.ARMv8A); ("riscv", Utils.RISCV);
     ]
   in
   let doc =

compiler/safetylib/arm_safety.ml

@@ -7,16 +7,16 @@ module Arm_safety
       with type reg = Arm_decl.register
        and type regx = Arch_utils.empty
        and type xreg = Arch_utils.empty
-       and type rflag = Arm_decl.rflag
-       and type cond = Arm_decl.condt
+       and type rflag = Arm_common.rflag
+       and type cond = Arm_common.condt
        and type asm_op = Arm_instr_decl.arm_op
        and type extra_op = Arm_extra.arm_extra_op)
   : SafetyArch
     with type reg = Arm_decl.register
      and type regx = Arch_utils.empty
      and type xreg = Arch_utils.empty
-     and type rflag = Arm_decl.rflag
-     and type cond = Arm_decl.condt
+     and type rflag = Arm_common.rflag
+     and type cond = Arm_common.condt
      and type asm_op = Arm_instr_decl.arm_op
      and type extra_op = Arm_extra.arm_extra_op
   = struct

compiler/safetylib/safetyMain.ml

@@ -60,3 +60,12 @@ let get_arch_with_analyze arch call_conv : (module ArchWithAnalyze) =
 
         let analyze = Safety.analyze
       end)
+  | ARMv8A ->
+      (module struct
+        module C = CoreArchFactory.Core_arch_ARMV8A
+        module A = Arch_full.Arch_from_Core_arch (C)
+
+        let analyze ?fmt:_ ~safety_param:_ _ _ =
+          hierror ~loc:Lnone ~kind:"safety analysis"
+            "the safety checker is not implemented for ARMv8-A"
+      end)

compiler/scripts/check

@@ -32,6 +32,9 @@ elif [ $ARCH = "riscv" ]
 then
      # +m enables integer multiplication
      ASARGS="--triple=riscv32 --mcpu=generic-rv32 -mattr=+m"
+elif [ $ARCH = "armv8a" ]
+then
+    ASARGS="--triple=aarch64"
 else
     ASARGS="--triple=x86_64"
 fi

compiler/src/arch_full.ml

@@ -35,12 +35,23 @@ module type Core_arch = sig
 
   val callstyle : reg callstyle
 
+  (* Minimal alignment of every stack frame. Frame sizes are rounded up to
+     the frame's alignment (see [stack_frame_allocation_size]), so this
+     bounds the alignment the stack pointer keeps across calls. AArch64
+     requires 16 bytes (SP alignment checking, Arm ARM DDI0487M.a,
+     D1.4.10.2); other architectures have no requirement beyond the one of
+     the stack slots themselves. *)
+  val sp_min_align : Wsize.wsize
+
+  (* Widest store the architecture can perform in one instruction. Used to
+     cap the default stack-zeroization clear step when [sp_min_align]
+     raises the frame alignment beyond it. *)
+  val max_store_size : Wsize.wsize
+
   val known_implicits : (Name.t * string) list
 
   val is_ct_asm_op : asm_op -> bool
-  val is_doit_asm_op : asm_op -> bool
   val is_ct_asm_extra : extra_op -> bool
-  val is_doit_asm_extra : extra_op -> bool
 
   val internal_call_conv : (reg, regx, xreg, rflag, cond) internal_calling_convention
 end
@@ -222,9 +233,11 @@ module Arch_from_Core_arch (A : Core_arch) :
     }
 
   let is_ct_sopn ?(doit = false) (o : extended_op) =
-   match o with
-   | BaseOp (_, o) -> (if doit then is_doit_asm_op else is_ct_asm_op) o
-   | ExtOp o -> (if doit then is_doit_asm_extra else is_ct_asm_extra) o
+   if doit then (Sopn.asm_op_instr asmOp o).Sopn.i_doit = Sopn.DOIT
+   else
+     match o with
+     | BaseOp (_, o) -> is_ct_asm_op o
+     | ExtOp o -> is_ct_asm_extra o
 
   let internal_call_conv =
     { icall_reg   = List.map var_of_reg  internal_call_conv.icall_reg

compiler/src/arch_full.mli

@@ -37,12 +37,17 @@ module type Core_arch = sig
 
   val callstyle : reg callstyle
 
+  (* Minimal alignment of every stack frame; see arch_full.ml. *)
+  val sp_min_align : Wsize.wsize
+
+  (* Widest store the architecture can perform in one instruction; see
+     arch_full.ml. *)
+  val max_store_size : Wsize.wsize
+
   val known_implicits : (Name.t * string) list
 
   val is_ct_asm_op : asm_op -> bool
-  val is_doit_asm_op : asm_op -> bool
   val is_ct_asm_extra : extra_op -> bool
-  val is_doit_asm_extra : extra_op -> bool
 
   val internal_call_conv : (reg, regx, xreg, rflag, cond) internal_calling_convention
 end