prove memory safety for chacha20 implementation#72

Draft

andres-erbsen wants to merge 12 commits into

Commits on Jul 21, 2022

Fix probable typo introduced in bcd4bcf014b54db0137a534472baa32c9fd35200
JasonGross
committed
Create non-inlined chacha20_block
JasonGross
committed
pull out which byte/word instances to use in straightline

jmgrosen
authored and
JasonGross
committed
chacha20 memory safety proof wip

jmgrosen
authored and
JasonGross
committed
expose some slowness

andres-erbsen
authored and
JasonGross
committed
cbv for map lookup seems rather difficult

andres-erbsen
authored and
JasonGross
committed
step through chacha20 loop body

andres-erbsen
authored and
JasonGross
committed
get to Qed on basic chacha20 proof

jmgrosen
authored and
JasonGross
committed
a more useful postcondition on chacha20 spec

jmgrosen
authored and
JasonGross
committed
Fix after rebase
JasonGross
committed
Add back ring instance
JasonGross
committed

Commits on Jul 22, 2022

Improve perf of straightline_cleanup
JasonGross
committed