Commits · subp-loop · sovereign / why3-avr

07 Nov, 2019 1 commit
- test version (subp with loop is in 'bigint_subp_j.mlw') · 99d5d173
  Marc Schoolderman authored Nov 07, 2019
  
  99d5d173
04 Nov, 2019 2 commits
- Fix st_inc (increase dst, not src! src is not even an address) · 7ea1e096
  Jonathan Moerman authored Oct 31, 2019
  
  7ea1e096
- incorporated changes to the interface for the mul256 operation · 98a67a51
  Marc Schoolderman authored Nov 04, 2019
  
  98a67a51
01 Nov, 2019 1 commit
- incorporate subtle changes in negation-chain from Karatsuba128 to the version... · 2dfe64a8
  Marc Schoolderman authored Nov 01, 2019
```
incorporate subtle changes in negation-chain from Karatsuba128 to the version found in Curve25519 implementation
```
  2dfe64a8
30 Oct, 2019 1 commit
- bigint_mul256 copied of karatsuba128 · 55ebfb44
  Marc Schoolderman authored Oct 30, 2019
  
  55ebfb44
28 Oct, 2019 1 commit
- subp initial version · e5e78b92
  Marc Schoolderman authored Oct 28, 2019
  
  e5e78b92
03 Oct, 2019 1 commit
- removed some comments · dd6660c0
  Marc Schoolderman authored Oct 03, 2019
  
  dd6660c0
16 Sep, 2019 1 commit
- cleanup of square128 proof · e657e428
  Marc Schoolderman authored Sep 16, 2019
  
  e657e428
11 Sep, 2019 2 commits
- finished proof of squaring routine · da168358
  Marc Schoolderman authored Sep 11, 2019
  
  da168358
- finished functional verification (unoptimized); one non-functional goal as yet unsolved · 7eb18124
  Marc Schoolderman authored Sep 11, 2019
  
  7eb18124
10 Sep, 2019 3 commits
- third third of sqr128 (unoptimized) · 2a3cc8c6
  Marc Schoolderman authored Sep 10, 2019
  
  2a3cc8c6
- removed superfluous checks from second third of sqr128 · 24e5339a
  Marc Schoolderman authored Sep 10, 2019
  
  24e5339a
- second third of sqr128 (unoptimized) · cb0c1036
  Marc Schoolderman authored Sep 10, 2019
  
  cb0c1036
09 Sep, 2019 1 commit
- added first half of 128-bit squaring routine (un-optimized) · 312455d8
  Marc Schoolderman authored Sep 09, 2019
  
  312455d8
06 Sep, 2019 2 commits
- change wording · 1430466e
  Marc Schoolderman authored Sep 06, 2019
  
  1430466e
- merged avrmodel and avrmodel3 · 044df936
  Marc Schoolderman authored Sep 06, 2019
  
  044df936
05 Sep, 2019 2 commits
- reran proofs (on single core), moved lemma about lsr to the top · 9e2e0084
  Marc Schoolderman authored Sep 05, 2019
  
  9e2e0084
- rough formalized version of karatsuba128 (with intermediate checks) · ab4186f5
  Marc Schoolderman authored Sep 05, 2019
  
  ab4186f5
30 Aug, 2019 1 commit
- friday afternoon commit: second block of outer level karatsuba proven · 9c944eea
  Marc Schoolderman authored Aug 30, 2019
  
  9c944eea
29 Aug, 2019 2 commits
- work · 7d81c154
  Marc Schoolderman authored Aug 29, 2019
  
  7d81c154
- import previous work · a476a7d9
  Marc Schoolderman authored Aug 29, 2019
  
  a476a7d9
23 Aug, 2019 7 commits
- modified 96-bit karatsuba in similar sense · 274df245
  Marc Schoolderman authored Aug 23, 2019
  
  274df245
- convert karatsuba80 into a 'localized' version · 5538acc9
  Marc Schoolderman authored Aug 22, 2019
  
  5538acc9
- cleanup of karatsuba64 · 887f74f0
  Marc Schoolderman authored Aug 22, 2019
  
  887f74f0
- merged avr_code22 into karatsuba48/64 · 6f42fc27
  Marc Schoolderman authored Aug 22, 2019
  
  6f42fc27
- cleanup proof; moved two instructions back to original position · 0ffc2ae5
  Marc Schoolderman authored Aug 22, 2019
  
  0ffc2ae5
- ported to why3 0.88.3 · 70d2f1bd
  Marc Schoolderman authored Aug 22, 2019
  
  70d2f1bd
- experiment: express effects of all blocks in local terms (why3 0.87.3) · c83341b2
  Marc Schoolderman authored Aug 22, 2019
  
  c83341b2
22 Aug, 2019 2 commits
- typo: assume -> assert. luckily, it was easily proven. · 5279ed0a
  Marc Schoolderman authored Aug 22, 2019
  
  5279ed0a
- removed pvs files · 42741d7b
  Marc Schoolderman authored Aug 22, 2019
  
  42741d7b
20 Aug, 2019 2 commits
- updated README; removed vestigial dependency on Z3 · 1bcdae7f
  Marc Schoolderman authored Aug 20, 2019
  
  1bcdae7f
- major cleanup of directory structure · db0572e2
  Marc Schoolderman authored Aug 19, 2019
  
  db0572e2
19 Aug, 2019 1 commit
- ported the proofs to why3 version 0.88.3; · ca07259c
  Marc Schoolderman authored Aug 19, 2019
```
removed any dependency on alt-ergo < 2.0.0
```
  ca07259c
20 Apr, 2018 2 commits
- ran bisection on proofs · 02ec34b5
  Marc Schoolderman authored Apr 20, 2018
  
  02ec34b5
- slight optimization · 0ed6b403
  Marc Schoolderman authored Apr 20, 2018
  
  0ed6b403
09 May, 2017 1 commit
- optimised 96-bit version · f370892c
  Marc Schoolderman authored May 09, 2017
  
  f370892c
08 May, 2017 2 commits
- optimised (removed checks) · 9d308b2c
  Marc Schoolderman authored May 08, 2017
  
  9d308b2c
- added 64- 80- and 96-bit karatsuba versions · 3ab5cbd5
  Marc Schoolderman authored Apr 13, 2017
  
  3ab5cbd5
13 Apr, 2017 2 commits
- added markings to reduce the number of invariants/asserts needed · 5d08ecc9
  Marc Schoolderman authored Apr 13, 2017
  
  5d08ecc9
- version bump of tools used · 402accd8
  Marc Schoolderman authored Apr 13, 2017
  
  402accd8