arm: share the Arm-common declarations (arm_common, JModel_arm) - #1548
Merged
Conversation
The NZCV flag register, the condition codes evaluated on it, the condition evaluation itself (arm_eval_cond, previously in arm.v) and the flag-combination description are not specific to AArch32: every Arm architecture shares them. Move these declarations from arm_decl.v and arm.v to a new arm_common.v that arm_decl re-exports, and let the OCaml side refer to the extracted Arm_common module. Pure refactoring in preparation for the AArch64 backend (jasmin-lang#1541), which reuses these definitions; no behavior change.
Move the 32-bit operations of JModel_m4 that are not AArch32-specific (flag computations, the ALU and shift operations on W32 with their NZCV outputs) to a new JModel_arm theory that JModel_m4 re-exports, in preparation for the AArch64 backend (jasmin-lang#1541), which reuses them for its W-register forms. The alias abbrevs of JModel_m4 (ADD = ADD_32, ...) now name the shared operators qualified: since EasyCrypt 2026.07, JWord's W32.ALU theory also declares ADD_32/ADC_32/AND_32/CMP_32/MUL_32/SUB_32, and the unqualified references became ambiguous once the definitions moved out of the file.
vbgl
approved these changes
Sep 1, 2026
clebreto
marked this pull request as ready for review
September 1, 2026 20:41
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
2 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.
Split out of #1541 as suggested in review: the first phase of that PR is a refactoring of existing code, reviewable (and CI-checkable) on its own.
arm_eval_cond) and the flag-combination description move fromarm_decl.v/arm.vto a newarm_common.vthatarm_declre-exports; the OCaml side follows (Arm_commonmodule). Pure refactoring, no behavior change.JModel_m4.ecthat are not AArch32-specific move to a newJModel_arm.ectheory thatJModel_m4re-exports. This also fixes the CI failure observed on Add an ARMv8-A (AArch64) backend #1541: since EasyCrypt 2026.07,JWord'sW32.ALUtheory declaresADD_32/ADC_32/AND_32/CMP_32/MUL_32/SUB_32too, so the alias abbrevs (abbrev ADD = ADD_32) became ambiguous once the definitions moved out of the file; they now name the shared operators qualified (JModel_arm.ADD_32).Both are preparation for the AArch64 backend (#1541), which reuses these definitions; once this lands, the corresponding hunks disappear from that PR.
Note: I could not run EasyCrypt locally, so the eclib commit is CI-validated only.