| b22e3c4 | Kevin Kane | 24 September 2019, 16:57:09 UTC | Add qTESLA to CI Makefile target | 24 September 2019, 16:57:09 UTC |
| 75d5cbb | Kevin Kane | 24 September 2019, 16:52:27 UTC | Remove references to Lib_PrintBuffer.{c,h} as it's not needed | 24 September 2019, 16:52:27 UTC |
| 72bd1e2 | Kevin Kane | 24 September 2019, 16:37:57 UTC | Remove copy of Frodo | 24 September 2019, 16:37:57 UTC |
| ed80d4d | Kevin Kane | 19 September 2019, 23:07:04 UTC | Hints update after post-merge build and verify run Commits for various repos: everest: 8ff5893906ccf2db347dbc23f0daf9197b73dd7e fstar: e0d3a0adff2a07b4b590c8671b138be5916eea3b kremlin: c04d180288897d5bd8068a7e59bd12b5c447541c | 19 September 2019, 23:07:04 UTC |
| 8a31437 | Kevin Kane | 19 September 2019, 21:33:36 UTC | Merge branch 'fstar-master' into _qtesla | 19 September 2019, 21:33:36 UTC |
| 4ff311c | Kevin Kane | 19 September 2019, 21:32:15 UTC | Add new hints files | 19 September 2019, 21:32:15 UTC |
| a447e5c | Dzomo the everest Yak | 18 September 2019, 08:26:11 UTC | [CI] regenerate hints | 18 September 2019, 08:26:11 UTC |
| 8dd4105 | Dzomo the everest Yak | 17 September 2019, 08:26:11 UTC | [CI] regenerate hints | 17 September 2019, 08:26:11 UTC |
| d7b1997 | Guido MartÃnez | 16 September 2019, 19:33:56 UTC | bump an rlimit | 16 September 2019, 19:33:56 UTC |
| 4ecb6b8 | Dzomo the everest Yak | 15 September 2019, 08:26:08 UTC | [CI] regenerate hints | 15 September 2019, 08:26:08 UTC |
| 542f8f4 | Dzomo the everest Yak | 14 September 2019, 08:26:31 UTC | [CI] regenerate hints | 14 September 2019, 08:26:31 UTC |
| 2223824 | Dzomo the everest Yak | 13 September 2019, 08:28:14 UTC | [CI] regenerate hints | 13 September 2019, 08:28:14 UTC |
| e881372 | Nikhil Swamy | 13 September 2019, 03:50:57 UTC | Merge remote-tracking branch 'origin/nik_erasable' into fstar-master | 13 September 2019, 03:50:57 UTC |
| c213271 | Nikhil Swamy | 12 September 2019, 22:01:30 UTC | enabling nl arith in a wrapper proof | 12 September 2019, 22:01:30 UTC |
| 88c983a | Dzomo the everest Yak | 12 September 2019, 08:27:18 UTC | [CI] regenerate hints | 12 September 2019, 08:27:18 UTC |
| 921f171 | Kevin Kane | 11 September 2019, 23:53:49 UTC | Relax post-condition on sparse_mul32 and pre-condition on reduce Facts that are true about the provable parameter set versions of these functions aren't true in the heuristic. Plus the precondition on the input for reduce isn't a precondition, but was just a stated fact of bounds on the inputs at one particular call site. | 11 September 2019, 23:53:49 UTC |
| c25ec5e | Dzomo the everest Yak | 11 September 2019, 08:27:03 UTC | [CI] regenerate hints | 11 September 2019, 08:27:03 UTC |
| f17ea8c | Kevin Kane | 10 September 2019, 22:43:28 UTC | Removed another assumption, made some notes narrowing down on proofs Full build and test run. | 10 September 2019, 22:43:28 UTC |
| ae15f16 | Dzomo the everest Yak | 10 September 2019, 09:38:59 UTC | [CI] regenerate hints | 10 September 2019, 09:38:59 UTC |
| c31b986 | Kevin Kane | 09 September 2019, 21:00:44 UTC | Change poly_sub_correct precondition to be sparse_mul_output Also comment out use of barr_reduce in qtesla_sign not done in heuristic parameter sets. Will need to uncomment later for provable parameter sets. | 09 September 2019, 21:00:44 UTC |
| a191cc5 | Kevin Kane | 09 September 2019, 17:18:34 UTC | Prove assumptions added to qtesla_sign_update_v to call poly_sub_correct Full build and test run not done for this commit. | 09 September 2019, 17:19:20 UTC |
| 4d370d9 | Dzomo the everest Yak | 09 September 2019, 08:27:20 UTC | [CI] regenerate hints | 09 September 2019, 08:27:20 UTC |
| 8f9dcfb | Dzomo the everest Yak | 08 September 2019, 08:27:24 UTC | [CI] regenerate hints | 08 September 2019, 08:27:24 UTC |
| dc0d7ad | Dzomo the everest Yak | 07 September 2019, 08:28:19 UTC | [CI] regenerate hints | 07 September 2019, 08:28:19 UTC |
| 6831bc6 | Chris Hawblitzel | 06 September 2019, 23:18:03 UTC | Restore "--use_extracted_interfaces true" to vale directories | 06 September 2019, 23:18:03 UTC |
| e29835d | Kevin Kane | 06 September 2019, 22:29:36 UTC | Shamelessly rip off useful lemmas from HACL* for shift_arithmetic_right proofs | 06 September 2019, 22:29:36 UTC |
| 11cfba6 | Kevin Kane | 06 September 2019, 21:34:46 UTC | Prove admitted lemmas and remove unneeded ones | 06 September 2019, 21:34:46 UTC |
| 90381ad | Kevin Kane | 06 September 2019, 20:24:57 UTC | Narrow assumptions in polynomial code down to at most proving the result of a single iteration satisfies the desired predicate. | 06 September 2019, 20:24:57 UTC |
| 0b19c5a | Dzomo the everest Yak | 06 September 2019, 08:31:12 UTC | [CI] regenerate hints | 06 September 2019, 08:31:12 UTC |
| 32a0666 | Chris Hawblitzel | 05 September 2019, 23:51:37 UTC | Add "open FStar.Mul" to every fst/fsti file in vale/ | 05 September 2019, 23:51:37 UTC |
| 6e58473 | Kevin Kane | 05 September 2019, 19:42:27 UTC | Remove more complicated proof from decode_pk for stability's sake Since we have to assume the output of decode_pk is valid, remove the more fine-grained proof that was there which would have been used had we been able to prove the operations actually guaranteed the bounds. Since it turns out that's not the case, remove all the proof code around slowly expanding a public key to satisfy the predicate, and just assume the whole thing is in range with an assumption at the end. The proof had been assuming the smallest possible fact and then using that to build to the larger conclusion, but that was making the prover randomly cancel. | 05 September 2019, 19:42:27 UTC |
| afc5973 | Chris Hawblitzel | 05 September 2019, 15:36:51 UTC | Tweak some options for recent Makefile change | 05 September 2019, 15:36:51 UTC |
| ac17e8d | Chris Hawblitzel | 05 September 2019, 13:00:05 UTC | Simplify Makefile by moving custom options out of Makefile into individual files inside vale directory | 05 September 2019, 13:00:05 UTC |
| b8e3da5 | Dzomo the everest Yak | 05 September 2019, 08:29:03 UTC | [CI] regenerate hints | 05 September 2019, 08:29:03 UTC |
| 737f69c | Kevin Kane | 29 August 2019, 16:43:24 UTC | Added proper pre/post-conditions to low-level math functions Added pre- and post-conditions based on conversation with Patrick. Added a few assumptions in at call sites for now to cover for later proving. Assumed results of decode_sk and decode_pk are within known ranges, consistent with the practice of the reference code. | 04 September 2019, 22:42:01 UTC |
| 90008dd | Chris Hawblitzel | 04 September 2019, 20:33:41 UTC | Don't say "friend Vale.Arch.BufferFriend", because that transitively friends many other modules and greatly slows verification | 04 September 2019, 20:33:41 UTC |
| 1ac2ff9 | Chris Hawblitzel | 04 September 2019, 18:35:11 UTC | Merge branch 'fstar-master' into _vale_heap | 04 September 2019, 18:35:11 UTC |
| 4caa04f | Chris Hawblitzel | 04 September 2019, 18:26:05 UTC | Add unfolded view_n to make verification of "% view_n t" faster | 04 September 2019, 18:26:05 UTC |
| 6beadeb | Dzomo the everest Yak | 04 September 2019, 08:26:51 UTC | [CI] regenerate hints | 04 September 2019, 08:26:51 UTC |
| cc61acf | Dzomo the everest Yak | 03 September 2019, 08:30:38 UTC | [CI] regenerate hints | 03 September 2019, 08:30:38 UTC |
| d846520 | Dzomo the everest Yak | 02 September 2019, 08:27:29 UTC | [CI] regenerate hints | 02 September 2019, 08:27:29 UTC |
| f919215 | Dzomo the everest Yak | 01 September 2019, 08:27:12 UTC | [CI] regenerate hints | 01 September 2019, 08:27:12 UTC |
| 9564cbc | Dzomo the everest Yak | 31 August 2019, 08:27:37 UTC | [CI] regenerate hints | 31 August 2019, 08:27:37 UTC |
| 6db4efc | Chris Hawblitzel | 30 August 2019, 21:37:52 UTC | Simplify Vale.Arch.Heap slightly | 30 August 2019, 21:37:52 UTC |
| 3040331 | Chris Hawblitzel | 30 August 2019, 18:00:11 UTC | Bring vale_state and machine_state closer together. Rather than considering vale_state and machine_state to be fundamentally different, treat them as two interchangeable views of the same underlying data (except for ms_trace, which only exists in machine_state). For example, there are now functions that convert back and forth between the two views and a round-trip lemma "lemma_to_of" that goes from machine_state to vale_state back to machine_state. The major change is that machine_state and vale_state now share the same heap type (Vale.Arch.Heap.heap_impl == Vale.Arch.HeapImpl.vale_heap_impl). | 30 August 2019, 18:00:11 UTC |
| e660623 | Dzomo the everest Yak | 30 August 2019, 08:27:27 UTC | [CI] regenerate hints | 30 August 2019, 08:27:27 UTC |
| 0318dd9 | Dzomo the everest Yak | 29 August 2019, 08:29:36 UTC | [CI] regenerate hints | 29 August 2019, 08:29:36 UTC |
| 7880cf2 | Kevin Kane | 27 August 2019, 22:40:18 UTC | Remove assumption about j in decode_sk Turns out the assumption that was proving difficult to prove was in fact false. Oops. Corrected the assertion to be actually true and now it proves. | 27 August 2019, 22:40:18 UTC |
| c0904da | Kevin Kane | 27 August 2019, 22:23:05 UTC | Remove all but two assumptions from Hacl.Impl.QTesla.Pack for qTESLA-I One has to do with guaranteeing coefficients of a secret key fit into the expected range, which I need to verify with Patrick because I don't see anywhere this is validated. The input may just be trusted since it's the secret key. The other is a pretty obvious inequality relationship that should be easy to prove but is being difficult for some reason. But this is still a significant advance and tests are passing, so making a commit. | 27 August 2019, 22:23:05 UTC |
| a5084d0 | Kevin Kane | 27 August 2019, 18:22:27 UTC | Eliminated assumptions from encode_sk and friends Recast encode_sk as a for loop so the prover can track the two indices more easily. Tests still passing. | 27 August 2019, 18:22:27 UTC |
| 0a85e21 | Kevin Kane | 27 August 2019, 15:32:58 UTC | Top-level file back to being assume-free after tracking down operator slash weirdness | 27 August 2019, 15:32:58 UTC |
| c7c22bd | Dzomo the everest Yak | 27 August 2019, 08:28:05 UTC | [CI] regenerate hints | 27 August 2019, 08:28:05 UTC |
| 7128ba5 | Dzomo the everest Yak | 26 August 2019, 08:27:30 UTC | [CI] regenerate hints | 26 August 2019, 08:27:30 UTC |
| 926528e | Dzomo the everest Yak | 25 August 2019, 08:28:02 UTC | [CI] regenerate hints | 25 August 2019, 08:28:02 UTC |
| df8f424 | Dzomo the everest Yak | 24 August 2019, 08:26:24 UTC | [CI] regenerate hints | 24 August 2019, 08:26:24 UTC |
| 97a0d25 | Kevin Kane | 23 August 2019, 15:59:58 UTC | Merge branch 'fstar-master' into _qtesla_wip | 23 August 2019, 15:59:58 UTC |
| 1cd60ae | Kevin Kane | 23 August 2019, 15:58:34 UTC | Change all options settings to push/pop style in main file after the initial setting | 23 August 2019, 15:58:34 UTC |
| 5c1ba25 | Dzomo the everest Yak | 23 August 2019, 08:27:21 UTC | [CI] regenerate hints | 23 August 2019, 08:27:21 UTC |
| 5131439 | Kevin Kane | 23 August 2019, 00:19:48 UTC | More proofs done, build still passing One assume ended up going back into test_correctness. Need to investigate why. | 23 August 2019, 00:19:48 UTC |
| 37c3310 | Dzomo the everest Yak | 22 August 2019, 08:27:24 UTC | [CI] regenerate hints | 22 August 2019, 08:27:24 UTC |
| 8c0f34a | Jonathan Protzenko | 21 August 2019, 12:15:04 UTC | Merge branch 'fstar-master' of pro.github.com:mitls/hacl-star into fstar-master | 21 August 2019, 12:15:04 UTC |
| 1ee04f2 | Jonathan Protzenko | 21 August 2019, 09:42:10 UTC | Also lift the length restriction for HKDF | 21 August 2019, 09:42:10 UTC |
| 00e7770 | Jonathan Protzenko | 21 August 2019, 09:36:21 UTC | Lift restriction on input length for HMAC | 21 August 2019, 09:36:21 UTC |
| 7af0972 | Dzomo the everest Yak | 21 August 2019, 08:27:21 UTC | [CI] regenerate hints | 21 August 2019, 08:27:21 UTC |
| 414118e | Santiago Zanella-Beguelin | 20 August 2019, 09:19:51 UTC | Merge branch 'santiago_merkle' into fstar-master | 20 August 2019, 09:19:51 UTC |
| b8d4d15 | Jonathan Protzenko | 20 August 2019, 08:03:21 UTC | Deeply rooted evil bug. ocamldep generated an entry with a backslash which from the GNU make point of view was a different production | 20 August 2019, 08:03:21 UTC |
| 5e0e44a | Santiago Zanella-Beguelin | 19 August 2019, 23:12:26 UTC | Simplify sequence comparison | 19 August 2019, 23:12:26 UTC |
| 14182d1 | Santiago Zanella-Beguelin | 19 August 2019, 23:11:00 UTC | Fixed one-char typo in MD5 specification: logxor -> logor | 19 August 2019, 23:11:00 UTC |
| d50718d | Santiago Zanella-Beguelin | 19 August 2019, 18:24:49 UTC | Hints | 19 August 2019, 18:24:49 UTC |
| 70a824b | Santiago Zanella-Beguelin | 19 August 2019, 18:24:18 UTC | Non-constant time comparison alternative | 19 August 2019, 18:24:18 UTC |
| a3e0a96 | Santiago Zanella-Beguelin | 19 August 2019, 16:53:21 UTC | Hints | 19 August 2019, 16:53:21 UTC |
| 1dc9a98 | Santiago Zanella-Beguelin | 19 August 2019, 16:13:23 UTC | Get rid of annoying warning | 19 August 2019, 16:13:23 UTC |
| 73ec644 | Santiago Zanella-Beguelin | 19 August 2019, 16:12:51 UTC | Port MerkleTree to new EverCrypt hash using Lib.IntTypes | 19 August 2019, 16:12:51 UTC |
| 8f64795 | Santiago Zanella-Beguelin | 19 August 2019, 16:11:09 UTC | Lib.RawBuffer module implementing blit from public to secret bytes | 19 August 2019, 16:11:09 UTC |
| 8c7762a | Chris Hawblitzel | 19 August 2019, 15:41:40 UTC | Use balanced binary search tree for taints in Vale.X64.Leakage | 19 August 2019, 15:41:40 UTC |
| 05ce38f | Dzomo the everest Yak | 19 August 2019, 08:27:11 UTC | [CI] regenerate hints | 19 August 2019, 08:27:11 UTC |
| 736d4df | Dzomo the everest Yak | 18 August 2019, 08:27:05 UTC | [CI] regenerate hints | 18 August 2019, 08:27:05 UTC |
| a7f9fdd | Dzomo the everest Yak | 17 August 2019, 08:28:07 UTC | [CI] regenerate hints | 17 August 2019, 08:28:07 UTC |
| 463a2c2 | Aymeric Fromherz | 16 August 2019, 20:45:30 UTC | Update poly semiring tactic wrt F* master | 16 August 2019, 20:45:30 UTC |
| d9948ca | Aymeric Fromherz | 16 August 2019, 20:38:39 UTC | rlimits | 16 August 2019, 20:38:39 UTC |
| 75dd1f3 | Kevin Kane | 16 August 2019, 20:26:07 UTC | WIP | 16 August 2019, 20:26:07 UTC |
| 0dcabce | Aymeric Fromherz | 16 August 2019, 18:47:00 UTC | Start addressing Santiago's comments | 16 August 2019, 18:47:00 UTC |
| 3676f21 | Aymeric Fromherz | 16 August 2019, 17:38:37 UTC | Fix flaky Spec.BignumQ.Lemmas proof | 16 August 2019, 17:38:37 UTC |
| 726a060 | Santiago Zanella-Beguelin | 16 August 2019, 17:30:48 UTC | Simplify proofs | 16 August 2019, 17:30:48 UTC |
| 5e37959 | Jonathan Protzenko | 16 August 2019, 15:07:13 UTC | one last fix | 16 August 2019, 15:07:13 UTC |
| d00bce5 | Jonathan Protzenko | 16 August 2019, 13:36:57 UTC | Try fix | 16 August 2019, 13:36:57 UTC |
| b89225b | Jonathan Protzenko | 16 August 2019, 13:00:12 UTC | Merge remote-tracking branch 'origin/santiago_fix' into fstar-master | 16 August 2019, 13:00:12 UTC |
| c5827ab | Santiago Zanella-Beguelin | 16 August 2019, 12:58:33 UTC | Use canon_semiring instead of canon_semiring_with | 16 August 2019, 12:58:33 UTC |
| 6d9599e | Jonathan Protzenko | 16 August 2019, 12:15:47 UTC | Merge branch 'fstar-master' of pro.github.com:mitls/hacl-star into fstar-master | 16 August 2019, 12:15:47 UTC |
| 71ea08a | Jonathan Protzenko | 16 August 2019, 12:15:23 UTC | Cleanup the bundle variables in the Makefile and add a Mozilla distribution | 16 August 2019, 12:15:23 UTC |
| 1bea24d | Jonathan Protzenko | 16 August 2019, 12:14:55 UTC | hints | 16 August 2019, 12:14:55 UTC |
| 500f2ab | Dzomo the everest Yak | 16 August 2019, 08:27:09 UTC | [CI] regenerate hints | 16 August 2019, 08:27:09 UTC |
| 5ec25bb | Aymeric Fromherz | 16 August 2019, 05:15:34 UTC | Merge branch 'fstar-master' into afromher_ed | 16 August 2019, 05:15:34 UTC |
| 82e1aed | Aymeric Fromherz | 16 August 2019, 03:16:32 UTC | Work towards merkle trees | 16 August 2019, 03:16:32 UTC |
| 2ea5339 | Chris Hawblitzel | 16 August 2019, 02:28:17 UTC | Add small SymCrypt example and make fast_sqr_part2 verify faster | 16 August 2019, 02:28:17 UTC |
| dc2f5b7 | Aymeric Fromherz | 15 August 2019, 21:25:17 UTC | Merge branch 'fstar-master' into afromher_ed | 15 August 2019, 21:25:17 UTC |
| 187617f | Aymeric Fromherz | 15 August 2019, 21:17:04 UTC | Fix gcmencryptOpt interop | 15 August 2019, 21:17:04 UTC |
| b187043 | Santiago Zanella-Beguelin | 15 August 2019, 16:46:25 UTC | Trying with fuel = 0 | 15 August 2019, 17:00:21 UTC |
| 0525b55 | Santiago Zanella-Beguelin | 15 August 2019, 14:34:43 UTC | Tighter modifies clause and reduced ifuel for fast_sqr_part2 | 15 August 2019, 14:34:43 UTC |
| caaee96 | Dzomo the everest Yak | 14 August 2019, 12:21:12 UTC | [CI] regenerate hints | 14 August 2019, 12:21:12 UTC |
