Feature/armv8a distilled - #5

Closed

clebreto wants to merge 74 commits into

mainfrom

feature/armv8a-distilled

Commits on Jul 10, 2026

Add ARMv8-A (AArch64) backend (functional milestone)
clebreto
committed
e6a40c3
armv8a: add 32-bit (W register) instruction forms
clebreto
committed
ec87917
armv8a: reserve XZR/x18, enforce 16-byte SP alignment, fix SP restore
clebreto
committed
b3df1fd
armv8a: prove core operation builders (ARMv8AFopn_coreP)
clebreto
committed
cd1f311
armv8a: prove params-level operation wrappers (ARMv8AFopnP)
clebreto
committed
d6759bf
armv8a: ground the shift-amount immediate checkers in the Arm ARM
clebreto
committed
4f5e044
armv8a: model A64 immediate legality in the argument checkers
clebreto
committed
598fd86
armv8a: prove the MOVZ/MOVN/MOVK immediate materialization (li)
clebreto
committed
1745b1d
armv8a: move the SP 16-byte alignment invariant to the stack-alloc oracle
clebreto
committed
6594122
armv8a: prove the stack-alloc and (most) linearization hypotheses
clebreto
committed
bc2af9c
armv8a: complete the linearization hypotheses (armv8a_hliparams)
clebreto
committed
f313433
armv8a: prove the assembly-generation hypotheses (armv8a_hagparams)
clebreto
committed
2eee820
armv8a: prove stack zeroization (armv8a_hszparams)
clebreto
committed
681c105
armv8a: prove lowering correct, complete h_architecture_params
clebreto
committed
737b366
armv8a: accept explicitly masked variable shift amounts
clebreto
committed
983734e
armv8a: test the 32-bit (W register) operations
clebreto
committed
767d809
armv8a: alphabetize the armv8a entries in _CoqProject
clebreto
committed
3d6ac4b
armv8a: list the armv8a check category next to the other base architectures
clebreto
committed
3be1aea
armv8a: error out instead of claiming safety for the unsupported checker
clebreto
committed
d627c2f
armv8a: factor the stack-pointer minimal-alignment bump in stackAlloc
clebreto
committed
3635bea
armv8a: make the minimal stack-pointer alignment a global option
clebreto
committed
8863f9a
arm, armv8a: share the NZCV flag declarations in arm_common
clebreto
committed
8333ff6
arm, armv8a: share the condition-code type in arm_common
clebreto
committed
cbfb7ce
arm, armv8a: share the condition-code evaluation in arm_common
clebreto
committed
a1d9a57
armv8a: remove the variable-shift mnemonics ASRV/LSLV/LSRV/RORV
clebreto
committed
cd98121
armv8a: carry the true per-operand width in pp_aop_args
clebreto
committed
41d3331
armv8a: print conditions in place and make pp_asm_arg total
clebreto
committed
ae3e6c1
armv8a: define each instruction's semantics next to its description
clebreto
committed
9474a95
armv8a: list the same modules as the other architectures in extraction
clebreto
committed
133614b
armv8a: define SUBS as ADCS x (invw y) true in the EasyCrypt model
clebreto
committed
27e574f
armv8a: generate size-suffixed op names, model both sizes in EasyCrypt
clebreto
committed
c63f6fe
armv8a: make is_doit_asm_op exhaustive, one case per mnemonic
clebreto
committed
11669f2
armv8a: fuse multiplications of any width at least the target into MADD/MSUB
clebreto
committed
dd6dc4b
arm, armv8a: extract the shared arm_common module
clebreto
committed
e69a242
armv8a: accept armv8a in the cmdliner tools (jasmin2ec, jasmin-ct, ...)
clebreto
committed
6164586

Commits on Jul 11, 2026

Merge branch 'main' into feature/armv8a
clebreto
committed
642405a
armv8a: fix ROR in the EasyCrypt model: rotate, not arithmetic shift
clebreto
committed
15101d8
armv8a: rename armv8a_linux_call_conv to armv8a_call_conv
clebreto
committed
6d7fcdf
armv8a: complete the port to upstream main
clebreto
committed
c4e0d27
armv8a: add the stack-zeroization test categories
clebreto
committed
2ea47ac
armv8a: test the instruction semantics against the hardware
clebreto
committed
05545d0
eclib: share the common Arm 32-bit operations in JModel_arm
clebreto
committed
47b94ef

Commits on Jul 21, 2026

arch: carry the DOIT classification in the instruction descriptors
clebreto
committed
ef8ea02
attach doit info to the declaration of the instruction

bgregoir
authored and
clebreto
committed
2633f35
armv8a: repair the MSUB case of lower_Papp2P
clebreto
committed
4175961
armv8a: restrict the shifted variant of instructions to register operands
clebreto
committed
ef31bc5
armv8a: forbid ROR on the shifted arithmetic instructions
clebreto
committed
5d64730
arch: cap the default zeroization step by the widest store, not reg_size
clebreto
committed
7177f76
armv8a: state MVN's register-only argument kinds directly
clebreto
committed
c762306
armv8a: trim the alias-of-V boilerplate from the shift doc blocks
clebreto
committed
f00e297
armv8a: distill the instruction model to the lowering-emitted set
clebreto
committed
8c46ec4
armv8a: reject halfword shifts 32/48 on the 32-bit wide moves
clebreto
committed
4d2d6af
armv8a: drop the stale shifted-ROR skip note from the hw-semantics test
clebreto
committed
8d4c50f

Commits on Jul 22, 2026

Commits on Jul 23, 2026

arch: carry the DOIT classification in the instruction descriptors (#1520)

authored
98272e0

Commits on Jul 27, 2026

Target EasyCrypt 2026.07

vbgl
authored and
bgregoir
committed
6f751ed
Do not rely on implementation details of mod_pow2

vbgl
authored and
bgregoir
committed
3f11f9a
Update mathcomp-word

vbgl
authored and
bgregoir
committed
5fc1938
VPSLLV and VPSRLV reject 16 bit

sarranz
authored and
bgregoir
committed
487336d
CI: add libjade/curve25519 job

vbgl
authored and
bgregoir
committed
aeabc7c

Commits on Aug 18, 2026

CI: update nixpkgs

vbgl
authored and
eponier
committed
996c142
CI: update docker image

vbgl
authored and
eponier
committed
b347041
nix: minor cleaning

vbgl
authored and
eponier
committed
0fdf057
CI: fix job push-compiler-code

vbgl
authored and
eponier
committed
25ebb0c
Minor fix in pretyping

eponier
authored and
vbgl
committed
34552f6
Require mathcomp 2.4

vbgl
authored and
eponier
committed
a34faa2
Update mathcomp-word

vbgl
authored and
eponier
committed
7b6200d

Commits on Aug 19, 2026

Linearization params: make lload and llstore more general (#1536)
vbgl
authored
87d39fb

Commits on Aug 21, 2026

CI: update nixpkgs

vbgl
authored and
eponier
committed
5125ecb

Commits on Aug 25, 2026

Memoize i_loc0

vbgl
authored and
eponier
committed
0e96330

Commits on Aug 26, 2026