1. 28 Feb, 2020 4 commits
  2. 27 Feb, 2020 1 commit
  3. 11 Feb, 2020 1 commit
  4. 17 Jan, 2020 5 commits
  5. 16 Jan, 2020 1 commit
  6. 10 Jan, 2020 3 commits
  7. 09 Jan, 2020 3 commits
  8. 20 Dec, 2019 4 commits
  9. 19 Dec, 2019 4 commits
  10. 13 Dec, 2019 3 commits
  11. 12 Dec, 2019 1 commit
  12. 06 Dec, 2019 1 commit
    • Jonathan Moerman's avatar
      Add fe25519_{sub,add,red} · f1509caa
      Jonathan Moerman authored
      Squashed commit of the following:
      
      commit 46963b1b
      Author: Jonathan Moerman <jonathanmoerman@gmail.com>
      Date:   Fri Dec 6 13:39:12 2019 +0100
      
          Add converted fe25519_mul121666 (brne, zero flag are still missing)
      
      commit 1d4a3abe
      Author: Jonathan Moerman <jonathanmoerman@gmail.com>
      Date:   Fri Dec 6 13:11:02 2019 +0100
      
          Reduce the amount of assertions in fe25519_sub/add
      
      commit 1895db65
      Author: Jonathan Moerman <jonathanmoerman@gmail.com>
      Date:   Thu Dec 5 17:17:00 2019 +0100
      
          Clean-up of assertions in fe25519_red
      
      commit b130146a
      Author: Jonathan Moerman <jonathanmoerman@gmail.com>
      Date:   Thu Dec 5 17:02:58 2019 +0100
      
          This is probably the most concise description of fe25519_red result
      
      commit 8fd5ba77
      Author: Jonathan Moerman <jonathanmoerman@gmail.com>
      Date:   Thu Dec 5 16:44:42 2019 +0100
      
          Make the result of fe25519_red slightly better readable
      
      commit a1c312d7
      Author: Jonathan Moerman <jonathanmoerman@gmail.com>
      Date:   Thu Dec 5 16:32:06 2019 +0100
      
          Remove apostrophes and a few assertions in fe25519_red
      
      commit add8ffd1
      Author: Jonathan Moerman <jonathanmoerman@gmail.com>
      Date:   Thu Dec 5 16:15:36 2019 +0100
      
          Give fe25519 the same treatment
      
      commit 15a6109e
      Author: Jonathan Moerman <jonathanmoerman@gmail.com>
      Date:   Thu Dec 5 15:48:47 2019 +0100
      
          Optimize fe25519_sub (-30s, less assertions)
      
      commit 7c4db91e
      Author: Jonathan Moerman <jonathanmoerman@gmail.com>
      Date:   Thu Dec 5 14:39:27 2019 +0100
      
          Finish fe25519
      
      commit b3496be7
      Author: Jonathan Moerman <jonathanmoerman@gmail.com>
      Date:   Thu Dec 5 14:12:56 2019 +0100
      
          Reduction function is done, some cleanup required
      
      commit 52b7a195
      Author: Jonathan Moerman <jonathanmoerman@gmail.com>
      Date:   Thu Dec 5 13:25:53 2019 +0100
      
          Prove the boring properties of the reduction function
      
      commit 72990334
      Author: Jonathan Moerman <jonathanmoerman@gmail.com>
      Date:   Thu Dec 5 12:53:47 2019 +0100
      
          Improve readability (further reduce uint and ref usage)
      
      commit f70ebbcf
      Author: Jonathan Moerman <jonathanmoerman@gmail.com>
      Date:   Thu Dec 5 12:31:36 2019 +0100
      
          Loop is done, clean up
      
      commit 5e0479f3
      Author: Jonathan Moerman <jonathanmoerman@gmail.com>
      Date:   Thu Dec 5 11:55:03 2019 +0100
      
          Specify behavior of 10 iterations of the loop
      
      commit 26e2a1c4
      Author: Jonathan Moerman <jonathanmoerman@gmail.com>
      Date:   Mon Dec 2 11:16:43 2019 +0100
      
          We can now perform 5 iterations of the loop + clean-ups
          It may be possible to extend te current technique to the entire loop, otherwise we can just add another level of abstraction: (now: instructions -> iteration -> loop, new: instructions -> iteration -> 5/6 iterations -> loop)
      
      commit 5474ef37
      Author: Jonathan Moerman <jonathanmoerman@gmail.com>
      Date:   Fri Nov 29 15:24:28 2019 +0100
      
          Finish everything up to the loop
      
      commit 0cb6f3fc
      Author: Jonathan Moerman <jonathanmoerman@gmail.com>
      Date:   Fri Nov 29 14:30:55 2019 +0100
      
          Pre-loop part is mostly done
      
      commit 5ec497b9
      Author: Jonathan Moerman <jonathanmoerman@gmail.com>
      Date:   Fri Nov 29 12:56:40 2019 +0100
      
          Use a few ghost functions to simplify the value of r21 prior to entering the loop
      
      commit bd82630e
      Author: Jonathan Moerman <jonathanmoerman@gmail.com>
      Date:   Thu Nov 28 17:37:35 2019 +0100
      
          Simplify the reduction_loop_iter spec.
      
      commit e7005dda
      Author: Jonathan Moerman <jonathanmoerman@gmail.com>
      Date:   Thu Nov 28 16:58:01 2019 +0100
      
          Initial work on fe25519_red
      
      commit aec69210
      Author: Jonathan Moerman <jonathanmoerman@gmail.com>
      Date:   Thu Nov 28 11:01:28 2019 +0100
      
          Add initial whyml conversion of fe25519_red
      
      commit c0e8aca0
      Author: Jonathan Moerman <jonathanmoerman@gmail.com>
      Date:   Mon Nov 25 18:21:08 2019 +0100
      
          Clean-ups; move BV_asr_Lemmas and AvrModelLemmas to a separate file
      
      commit 7f0ca3f2
      Author: Jonathan Moerman <jonathanmoerman@gmail.com>
      Date:   Mon Nov 25 17:48:59 2019 +0100
      
          Add missing abstract blocks and asserts, sub proof is done
      
      commit 5bc02abd
      Author: Jonathan Moerman <jonathanmoerman@gmail.com>
      Date:   Mon Nov 25 17:01:16 2019 +0100
      
          Fix the accidentally flipped signs in sub32_x_y_from_z_helper
      
      commit 0ac2c609
      Author: Jonathan Moerman <jonathanmoerman@gmail.com>
      Date:   Fri Nov 22 17:53:59 2019 +0100
      
          Use a let for reg_copy, fe25519_sub is now 75% complete
      
      commit bfc33ae5
      Author: Jonathan Moerman <jonathanmoerman@gmail.com>
      Date:   Fri Nov 22 16:49:55 2019 +0100
      
          Finish borrow propagation
      
      commit 1d7e10a0
      Author: Jonathan Moerman <jonathanmoerman@gmail.com>
      Date:   Fri Nov 22 16:13:58 2019 +0100
      
          use mod_256_to_256_m38 to prove congruence
      
      commit 164ab729
      Author: Jonathan Moerman <jonathanmoerman@gmail.com>
      Date:   Fri Nov 22 15:58:31 2019 +0100
      
          Port mod_256_to_256_m38 from fe25519_add to fe25519_sub
      
      commit 450586f0
      Author: Jonathan Moerman <jonathanmoerman@gmail.com>
      Date:   Fri Nov 22 15:42:05 2019 +0100
      
          Add fe25519_sub
      
      commit 0c0ed493
      Author: Jonathan Moerman <jonathanmoerman@gmail.com>
      Date:   Fri Nov 22 15:24:03 2019 +0100
      
          Use shadow registers to specify calling convention compliance
      
      commit dd3945b8
      Author: Jonathan Moerman <jonathanmoerman@gmail.com>
      Date:   Fri Nov 22 15:05:28 2019 +0100
      
          fe25519_add: Clean ups
      
      commit 33b94a50
      Author: Jonathan Moerman <jonathanmoerman@gmail.com>
      Date:   Fri Nov 22 14:56:59 2019 +0100
      
          Remove slow additions
      
      commit 420d0aeb
      Author: Jonathan Moerman <jonathanmoerman@gmail.com>
      Date:   Fri Nov 22 14:33:03 2019 +0100
      
          Add a much faster add32
      
      commit 50ce5653
      Author: Jonathan Moerman <jonathanmoerman@gmail.com>
      Date:   Fri Nov 22 13:36:24 2019 +0100
      
          Add much faster add8 versions
      
      commit 0850cab3
      Author: Jonathan Moerman <jonathanmoerman@gmail.com>
      Date:   Fri Nov 22 11:35:14 2019 +0100
      
          Using compute more selecitvely causes another large speedup
      
      commit daae3622
      Author: Jonathan Moerman <jonathanmoerman@gmail.com>
      Date:   Fri Nov 22 11:23:09 2019 +0100
      
          Speed up add31_cf_to_z, by a large amount
          Can't really repeat this for add8_x_y_to_z, unfortunately.
      
      commit 9721c8b3
      Author: Jonathan Moerman <jonathanmoerman@gmail.com>
      Date:   Thu Nov 21 17:17:06 2019 +0100
      
          No progress, but I hope that this will prevent why3 from corrupting ~the entire proof
      
      commit bee371cf
      Author: Jonathan Moerman <jonathanmoerman@gmail.com>
      Date:   Thu Nov 21 13:58:39 2019 +0100
      
          Cleanup pt2
      
      commit f4fb947a
      Author: Jonathan Moerman <jonathanmoerman@gmail.com>
      Date:   Thu Nov 21 13:56:19 2019 +0100
      
          Safe cleanup
      
      commit 63c20182
      Merge: b6ea2040 ef0b5271
      Author: Jonathan Moerman <jonathanmoerman@gmail.com>
      Date:   Thu Nov 21 13:48:04 2019 +0100
      
          Merge remote-tracking branch 'origin/master' into subp
      
      commit b6ea2040
      Author: Jonathan Moerman <jonathanmoerman@gmail.com>
      Date:   Thu Nov 21 13:40:47 2019 +0100
      
          Prove that only r is modified
      
      commit 12441430
      Author: Jonathan Moerman <jonathanmoerman@gmail.com>
      Date:   Thu Nov 21 13:16:00 2019 +0100
      
          Fix prover troubles by moving the interesting part to its own function
      
      commit 5bfa254c
      Author: Jonathan Moerman <jonathanmoerman@gmail.com>
      Date:   Thu Nov 21 12:31:34 2019 +0100
      
          fe25519_add: Proof is complete. but previously proven goals are now too difficult due to expanded proof context
      
      commit 03240c7b
      Author: Jonathan Moerman <jonathanmoerman@gmail.com>
      Date:   Fri Nov 15 17:46:58 2019 +0100
      
          fe25519 nearly done
      
      commit 72c3a191
      Author: Jonathan Moerman <jonathanmoerman@gmail.com>
      Date:   Thu Nov 14 17:03:51 2019 +0100
      
          Loops are 'done'
      
      commit d4b8c7d9
      Author: Jonathan Moerman <jonathanmoerman@gmail.com>
      Date:   Thu Nov 14 12:27:31 2019 +0100
      
          Contains too many asserts but z=x+y is done
      
      commit 2b01419e
      Author: Jonathan Moerman <jonathanmoerman@gmail.com>
      Date:   Mon Nov 11 17:10:21 2019 +0100
      
          Prove all assertions in add32_x_y_to_z2, doesn't prove postcond yet
      
      commit 8f2b8f60
      Author: Jonathan Moerman <jonathanmoerman@gmail.com>
      Date:   Mon Nov 11 16:49:01 2019 +0100
      
          The current mess
      
      commit 8a8ca2b8
      Author: Jonathan Moerman <jonathanmoerman@gmail.com>
      Date:   Thu Nov 7 15:43:45 2019 +0100
      
          Add fe25519_add, add a non incrementing ld (called ld_c for now)
      
      commit 3fa2a655
      Author: Jonathan Moerman <jonathanmoerman@gmail.com>
      Date:   Thu Nov 7 14:27:07 2019 +0100
      
          Fix off by one
      
      commit b358b2f6
      Author: Jonathan Moerman <jonathanmoerman@gmail.com>
      Date:   Thu Nov 7 14:17:00 2019 +0100
      
          3 block proof of subp
      
      commit 06a8f2f3
      Author: Jonathan Moerman <jonathanmoerman@gmail.com>
      Date:   Thu Oct 31 15:39:12 2019 +0100
      
          Fix st_inc (increase dst, not src! src is not even an address)
      f1509caa
  13. 15 Nov, 2019 2 commits
  14. 07 Nov, 2019 5 commits
  15. 04 Nov, 2019 1 commit
  16. 01 Nov, 2019 1 commit