1. 11 Feb, 2020 1 commit
  2. 17 Jan, 2020 5 commits
  3. 16 Jan, 2020 1 commit
  4. 10 Jan, 2020 3 commits
  5. 09 Jan, 2020 3 commits
  6. 20 Dec, 2019 4 commits
  7. 19 Dec, 2019 4 commits
  8. 13 Dec, 2019 3 commits
  9. 12 Dec, 2019 1 commit
  10. 06 Dec, 2019 1 commit
    • Jonathan Moerman's avatar
      Add fe25519_{sub,add,red} · f1509caa
      Jonathan Moerman authored
      Squashed commit of the following:
      
      commit 46963b1bb5df78d92cf6c499489f55fabbb91bf9
      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 1d4a3abe53b025647c51e3d1eb3b29c3cdc1669d
      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 1895db656d57898ecaf935fe8627d7d9bef17c63
      Author: Jonathan Moerman <jonathanmoerman@gmail.com>
      Date:   Thu Dec 5 17:17:00 2019 +0100
      
          Clean-up of assertions in fe25519_red
      
      commit b130146abcf972de92845188532e6ad7dcfa0f6a
      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 8fd5ba77da0094e39974d531f1dc2b02d83538d6
      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 a1c312d74d28b8832fa27267a7138298d90be618
      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 add8ffd19a02bde92d9679cd28dc57651e6593ce
      Author: Jonathan Moerman <jonathanmoerman@gmail.com>
      Date:   Thu Dec 5 16:15:36 2019 +0100
      
          Give fe25519 the same treatment
      
      commit 15a6109e203fdd92952397c38bddbac36a3cbb6b
      Author: Jonathan Moerman <jonathanmoerman@gmail.com>
      Date:   Thu Dec 5 15:48:47 2019 +0100
      
          Optimize fe25519_sub (-30s, less assertions)
      
      commit 7c4db91e90972b1b3e573a2c48a7c288066b8ac3
      Author: Jonathan Moerman <jonathanmoerman@gmail.com>
      Date:   Thu Dec 5 14:39:27 2019 +0100
      
          Finish fe25519
      
      commit b3496be7ee787a99ef62c7584c30adf24d3abea9
      Author: Jonathan Moerman <jonathanmoerman@gmail.com>
      Date:   Thu Dec 5 14:12:56 2019 +0100
      
          Reduction function is done, some cleanup required
      
      commit 52b7a195b80642ea07049ddc926920c2440e9a44
      Author: Jonathan Moerman <jonathanmoerman@gmail.com>
      Date:   Thu Dec 5 13:25:53 2019 +0100
      
          Prove the boring properties of the reduction function
      
      commit 72990334fab920f9ca5c7906ea40699c6fb4102d
      Author: Jonathan Moerman <jonathanmoerman@gmail.com>
      Date:   Thu Dec 5 12:53:47 2019 +0100
      
          Improve readability (further reduce uint and ref usage)
      
      commit f70ebbcf22e7b129640d3b59867d1126ee5074a1
      Author: Jonathan Moerman <jonathanmoerman@gmail.com>
      Date:   Thu Dec 5 12:31:36 2019 +0100
      
          Loop is done, clean up
      
      commit 5e0479f3fa6abc3ad6d5f2a1a2a49de37d3dbfe3
      Author: Jonathan Moerman <jonathanmoerman@gmail.com>
      Date:   Thu Dec 5 11:55:03 2019 +0100
      
          Specify behavior of 10 iterations of the loop
      
      commit 26e2a1c445a2c6965ea66284a9ff3fd5a05450e6
      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 5474ef3779dfde45ba82d30ed7a3daa1c811c05e
      Author: Jonathan Moerman <jonathanmoerman@gmail.com>
      Date:   Fri Nov 29 15:24:28 2019 +0100
      
          Finish everything up to the loop
      
      commit 0cb6f3fce330c81ec53975dc10f97a46943fe976
      Author: Jonathan Moerman <jonathanmoerman@gmail.com>
      Date:   Fri Nov 29 14:30:55 2019 +0100
      
          Pre-loop part is mostly done
      
      commit 5ec497b90be748bfafaf7a23fadbbe197286f8dc
      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 bd82630e802931686c322385b6f33dac8a103656
      Author: Jonathan Moerman <jonathanmoerman@gmail.com>
      Date:   Thu Nov 28 17:37:35 2019 +0100
      
          Simplify the reduction_loop_iter spec.
      
      commit e7005ddab018c560870645998e7f7deb698fa146
      Author: Jonathan Moerman <jonathanmoerman@gmail.com>
      Date:   Thu Nov 28 16:58:01 2019 +0100
      
          Initial work on fe25519_red
      
      commit aec69210a78bb2780a5289a5a07a55aa08a6b8cf
      Author: Jonathan Moerman <jonathanmoerman@gmail.com>
      Date:   Thu Nov 28 11:01:28 2019 +0100
      
          Add initial whyml conversion of fe25519_red
      
      commit c0e8aca0dcab9b5539867fda7fcd536887242936
      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 7f0ca3f23bb1befd67f07a7c3dc54fefd2123878
      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 5bc02abdbabf8c7958cf485be5f2408a85132d37
      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 0ac2c60931d17d606b221fea44d1a266c294f016
      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 bfc33ae5579ef5f57ff153228b3dcce78141ab94
      Author: Jonathan Moerman <jonathanmoerman@gmail.com>
      Date:   Fri Nov 22 16:49:55 2019 +0100
      
          Finish borrow propagation
      
      commit 1d7e10a02f6ac0113428372a2543a5b6ffc47e41
      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 164ab72914845c2399626d443d705a298639f56c
      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 450586f0cc39413693284e79b23f36f15208a1cd
      Author: Jonathan Moerman <jonathanmoerman@gmail.com>
      Date:   Fri Nov 22 15:42:05 2019 +0100
      
          Add fe25519_sub
      
      commit 0c0ed493db8749def782fbef686fe6494bad11cc
      Author: Jonathan Moerman <jonathanmoerman@gmail.com>
      Date:   Fri Nov 22 15:24:03 2019 +0100
      
          Use shadow registers to specify calling convention compliance
      
      commit dd3945b85f3278b81f26d50d9d796dbd9597aef3
      Author: Jonathan Moerman <jonathanmoerman@gmail.com>
      Date:   Fri Nov 22 15:05:28 2019 +0100
      
          fe25519_add: Clean ups
      
      commit 33b94a5039f29e55264dd5d2906f1ddbcab67b37
      Author: Jonathan Moerman <jonathanmoerman@gmail.com>
      Date:   Fri Nov 22 14:56:59 2019 +0100
      
          Remove slow additions
      
      commit 420d0aeb6e83523a5a364b6fd72995e019b1c998
      Author: Jonathan Moerman <jonathanmoerman@gmail.com>
      Date:   Fri Nov 22 14:33:03 2019 +0100
      
          Add a much faster add32
      
      commit 50ce565375a35ff6ffab27710b462478597f28f7
      Author: Jonathan Moerman <jonathanmoerman@gmail.com>
      Date:   Fri Nov 22 13:36:24 2019 +0100
      
          Add much faster add8 versions
      
      commit 0850cab343132df87c888dcc40c20e5554dbe19e
      Author: Jonathan Moerman <jonathanmoerman@gmail.com>
      Date:   Fri Nov 22 11:35:14 2019 +0100
      
          Using compute more selecitvely causes another large speedup
      
      commit daae36229a4ab857e0ddb0b000e28927f0e6b374
      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 9721c8b332f5b4c17539d6810d167da9ee8aa239
      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 bee371cf09c7ca106161e60c2f84328d3d4850aa
      Author: Jonathan Moerman <jonathanmoerman@gmail.com>
      Date:   Thu Nov 21 13:58:39 2019 +0100
      
          Cleanup pt2
      
      commit f4fb947a9ab7a3703bbb409c2f1ccc5637184ad6
      Author: Jonathan Moerman <jonathanmoerman@gmail.com>
      Date:   Thu Nov 21 13:56:19 2019 +0100
      
          Safe cleanup
      
      commit 63c201829a21b8d6f05302011cd820ba752ecfb2
      Merge: b6ea204 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 b6ea2040aa22c38211ab415eff4bf507a228281d
      Author: Jonathan Moerman <jonathanmoerman@gmail.com>
      Date:   Thu Nov 21 13:40:47 2019 +0100
      
          Prove that only r is modified
      
      commit 12441430003d82fc4c63c8ac625ec0d169a7faa4
      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 5bfa254c58c69997bff56a5875d2fe8cf21c08ee
      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 03240c7b8772d0eff2bfd22fc89f2d7c6701247e
      Author: Jonathan Moerman <jonathanmoerman@gmail.com>
      Date:   Fri Nov 15 17:46:58 2019 +0100
      
          fe25519 nearly done
      
      commit 72c3a1915429d429d637aa16bf87dc8e90bc0bc9
      Author: Jonathan Moerman <jonathanmoerman@gmail.com>
      Date:   Thu Nov 14 17:03:51 2019 +0100
      
          Loops are 'done'
      
      commit d4b8c7d9f247cf0a782c90ddf73114900c3a6365
      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 2b01419e5125e12767129adfa0aac7a0a22b94c1
      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 8f2b8f608e08e301e11bfea41187a6cdb4daf290
      Author: Jonathan Moerman <jonathanmoerman@gmail.com>
      Date:   Mon Nov 11 16:49:01 2019 +0100
      
          The current mess
      
      commit 8a8ca2b888f3ef3014cebbd3deb7a43930bf5aba
      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 3fa2a65503ea15cfaa6dc9dd8da31c0033e46ae7
      Author: Jonathan Moerman <jonathanmoerman@gmail.com>
      Date:   Thu Nov 7 14:27:07 2019 +0100
      
          Fix off by one
      
      commit b358b2f6f7e12e4d2f59d7e711bf451f2d6f9683
      Author: Jonathan Moerman <jonathanmoerman@gmail.com>
      Date:   Thu Nov 7 14:17:00 2019 +0100
      
          3 block proof of subp
      
      commit 06a8f2f364b8880fbc8e1f1d10a16abbe16fa0ed
      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
  11. 15 Nov, 2019 2 commits
  12. 07 Nov, 2019 5 commits
  13. 04 Nov, 2019 1 commit
  14. 01 Nov, 2019 1 commit
  15. 30 Oct, 2019 1 commit
  16. 28 Oct, 2019 1 commit
  17. 03 Oct, 2019 1 commit
  18. 16 Sep, 2019 1 commit
  19. 11 Sep, 2019 1 commit