{"push_id":1240748280,"size":4,"distinct_size":1,"ref":"refs/heads/stage","head":"1a10fc66eca75f362568a6db9b04857307b2f8db","before":"3ed8de0b2b488f79b7e2e5b16396b23c9715efae","commits":[{"sha":"805d95d827bd6ddcf8edaee1b7f9c03f1027d98c","author":{"name":"Jason Gross","email":"b9ac16d1328e8db3a77c42cb3badbae06d42598f@google.com"},"message":"More zarith hints\n\nAfter    | File Name                                       | Before   || Change\n----------------------------------------------------------------------------------\n1m48.45s | Total                                           | 1m46.02s || +0m02.42s\n----------------------------------------------------------------------------------\n0m14.25s | Specific/GF25519                                | 0m21.36s || -0m07.10s\n0m06.46s | ModularArithmetic/Pow2BaseProofs                | 0m04.38s || +0m02.08s\n0m17.46s | ModularArithmetic/ModularBaseSystemProofs       | 0m16.20s || +0m01.26s\n0m15.08s | Experiments/SpecEd25519                         | 0m14.04s || +0m01.04s\n0m05.67s | ModularArithmetic/Tutorial                      | 0m04.06s || +0m01.61s\n0m04.94s | BaseSystemProofs                                | 0m04.27s || +0m00.67s\n0m04.38s | ModularArithmetic/Montgomery/ZProofs            | 0m03.52s || +0m00.85s\n0m03.64s | Util/ZUtil                                      | 0m03.29s || +0m00.35s\n0m03.29s | Experiments/SpecificCurve25519                  | 0m03.26s || +0m00.03s\n0m02.61s | ModularArithmetic/BarrettReduction/ZGeneralized | 0m02.31s || +0m00.29s\n0m02.43s | ModularArithmetic/BarrettReduction/ZHandbook    | 0m02.56s || -0m00.12s\n0m02.37s | ModularArithmetic/ModularBaseSystemOpt          | 0m02.18s || +0m00.18s\n0m02.22s | Encoding/PointEncodingPre                       | 0m01.59s || +0m00.63s\n0m02.10s | Specific/GF1305                                 | 0m02.02s || +0m00.08s\n0m01.97s | ModularArithmetic/ModularArithmeticTheorems     | 0m02.65s || -0m00.68s\n0m01.68s | ModularArithmetic/ExtendedBaseVector            | 0m01.72s || -0m00.04s\n0m01.61s | BaseSystem                                      | 0m01.29s || +0m00.32s\n0m01.39s | Experiments/DerivationsOptionRectLetInEncoding  | 0m00.93s || +0m00.45s\n0m01.34s | Util/NumTheoryUtil                              | 0m01.09s || +0m00.25s\n0m01.25s | ModularArithmetic/ModularBaseSystemListProofs   | 0m01.16s || +0m00.09s\n0m01.16s | ModularArithmetic/PrimeFieldTheorems            | 0m01.08s || +0m00.07s\n0m01.09s | ModularArithmetic/BarrettReduction/Z            | 0m01.59s || -0m00.50s\n0m01.00s | Testbit                                         | 0m00.66s || +0m00.34s\n0m00.98s | ModularArithmetic/ExtPow2BaseMulProofs          | 0m00.77s || +0m00.20s\n0m00.96s | Encoding/ModularWordEncodingTheorems            | 0m00.74s || +0m00.21s\n0m00.93s | Spec/ModularWordEncoding                        | 0m00.65s || +0m00.28s\n0m00.90s | ModularArithmetic/ModularBaseSystem             | 0m00.70s || +0m00.20s\n0m00.85s | ModularArithmetic/ModularBaseSystemField        | 0m00.84s || +0m00.01s\n0m00.72s | Encoding/ModularWordEncodingPre                 | 0m00.92s || -0m00.20s\n0m00.65s | ModularArithmetic/ModularBaseSystemList         | 0m00.68s || -0m00.03s\n0m00.61s | ModularArithmetic/PseudoMersenneBaseParamProofs | 0m00.69s || -0m00.07s\n0m00.57s | ModularArithmetic/Pow2Base                      | 0m00.58s || -0m00.01s\n0m00.53s | Spec/ModularArithmetic                          | 0m00.54s || -0m00.01s\n0m00.51s | ModularArithmetic/Pre                           | 0m00.61s || -0m00.09s\n0m00.44s | ModularArithmetic/PseudoMersenneBaseParams      | 0m00.51s || -0m00.07s\n0m00.41s | ModularArithmetic/Montgomery/Z                  | 0m00.58s || -0m00.17s","distinct":false,"url":"https://api.github.com/repos/JasonGross/fiat-crypto/commits/805d95d827bd6ddcf8edaee1b7f9c03f1027d98c"},{"sha":"1855c01d960b9bf5ddb2225ddc70fc1558ed1b05","author":{"name":"Jason Gross","email":"b9ac16d1328e8db3a77c42cb3badbae06d42598f@google.com"},"message":"Add lemma in 8.6 std lib to ListUtil for 8.4","distinct":false,"url":"https://api.github.com/repos/JasonGross/fiat-crypto/commits/1855c01d960b9bf5ddb2225ddc70fc1558ed1b05"},{"sha":"64c6ac262aff3f8fc1d9d810be70e5e8102613dc","author":{"name":"Jason Gross","email":"b9ac16d1328e8db3a77c42cb3badbae06d42598f@google.com"},"message":"Montgomery: Add a variant that does reduction through partial_reduce","distinct":false,"url":"https://api.github.com/repos/JasonGross/fiat-crypto/commits/64c6ac262aff3f8fc1d9d810be70e5e8102613dc"},{"sha":"1a10fc66eca75f362568a6db9b04857307b2f8db","author":{"name":"Jason Gross","email":"b9ac16d1328e8db3a77c42cb3badbae06d42598f@google.com"},"message":"zsimplify: Better support for existentials\n\n[omega] can sometimes solve things that [lia] cannot (see also\nhttps://coq.inria.fr/bugs/show_bug.cgi?id=5003)","distinct":true,"url":"https://api.github.com/repos/JasonGross/fiat-crypto/commits/1a10fc66eca75f362568a6db9b04857307b2f8db"}]}
{"actor":{"display_login":"JasonGross"}}