ARM ISA Semantics for Lean (arm-v9.4-a)

These semantics are generated from the official ARM SPEC available at https://github.com/rems-project/sail-arm.

⚠️ While this repository covers the full ARM, our Lean backend for sail is still work-in-progress. As a result, our semantics are still full of warnings and errors. Similarly, our output is not yet polished for readability.

RISC-V Lean Statistics

Lines: 951606
Definitions: 33944
Inductive definitions: 89
Abbreviations: 929

Warnings and Errors

Errors found: 12
Warnings found: 0

Error Classes

• 2x unknown identifier 'lteq_real'
• 2x unknown identifier 'append_str'
• 1x unknown identifier 'zero_extend'
• 1x unknown identifier 'undefined_real'
• 1x unknown identifier 'sign_extend'
• 1x unknown identifier 'round_up'
• 1x unknown identifier 'round_down'
• 1x unknown identifier 'lt_real'
• 1x unknown identifier 'ediv_nat'
• 1x Lean exited with code 1