Add fe25519_sub, fe25519_add, fe25519_red from jmoerman/why3-avr/tree/subp (!1) · Merge requests · sovereign / why3-avr

Jonathan Moerman requested to merge jmoerman/why3-avr:curve25519 into curve25519 Dec 06, 2019

This also introduces common_lemmas.mlw which contains AvrModelLemmas and BV_asr_Lemmas The merge seems to have applied fairly cleanly and I have compressed the sessions, but I might have missed some issues as I haven't replayed all proofs.

Add fe25519_sub, fe25519_add, fe25519_red from jmoerman/why3-avr/tree/subp

Merge request reports