Repository navigation

[closed due to licencing issues] Verify pasta_curves' AArch64 Pasta Montgomery routines - #35

Closed

daira wants to merge 9 commits into

mainfrom

aarch64-pasta-mul

Closed

[closed due to licencing issues] Verify pasta_curves' AArch64 Pasta Montgomery routines#35
daira wants to merge 9 commits into
mainfrom
aarch64-pasta-mul

Commits on Sep 8, 2026
- asm: transcribe pasta_curves' AArch64 Pasta Montgomery routines
  
  daira
  and
  claude
  committed
  c131ec3
Commits on Sep 9, 2026
- asm: generate the mechanical part of the AArch64 correctness proofs
  
  daira
  and
  claude
  committed
  b912050
- asm: prove the shared Montgomery reduction helper correct
  
  daira
  and
  claude
  committed
  6afd636
- asm: prove the conversion out of Montgomery form correct
  
  daira
  and
  claude
  committed
  3b3e39c
- asm: derive the skeleton's per-instruction facts from lemmas, not omega
  
  daira
  and
  claude
  committed
  96f83c6
- asm: say which units of the verification remain
  
  daira
  and
  claude
  committed
  0072b3f
- asm: make the skeleton's locals opaque in one step
  
  daira
  and
  claude
  committed
  d0ab9c7
- asm: extract each instruction's lets from the folded hypothesis
  
  daira
  and
  claude
  committed
  bbc7a9e
- asm: prove the Montgomery multiplication correct
  
  daira
  and
  claude
  committed
  bd96831