| f05368e | Andres Erbsen | 13 February 2017, 01:57:46 UTC | Attempt Weierstrass associativity again, good progress. | 02 March 2017, 18:37:14 UTC |
| bc46f85 | Andres Erbsen | 13 February 2017, 00:16:26 UTC | change weierstrass spec, prove most cases of associativity | 02 March 2017, 18:37:14 UTC |
| e8fab6b | Andres Erbsen | 12 February 2017, 02:59:58 UTC | split the algebra library; use fsatz more | 02 March 2017, 18:37:14 UTC |
| c56ca7b | Andres Erbsen | 10 February 2017, 15:12:44 UTC | fsatz, nsatz_solve_nonzero | 02 March 2017, 18:37:14 UTC |
| 55de48a | Andres Erbsen | 06 February 2017, 23:25:59 UTC | use field_nsatz in CompleteEdwardsCurve.Pre | 02 March 2017, 18:37:14 UTC |
| d641525 | Andres Erbsen | 06 February 2017, 23:25:31 UTC | field_nsatz | 02 March 2017, 18:37:14 UTC |
| 255ce63 | jadep | 02 March 2017, 16:19:18 UTC | make assert_preconditions way more sane; use vm_decide to kill most subgoals | 02 March 2017, 16:19:18 UTC |
| 5e8748b | jadep | 02 March 2017, 15:57:56 UTC | Separated out [carry] from other operations. | 02 March 2017, 15:57:56 UTC |
| 37fa62b | jadep | 02 March 2017, 03:00:37 UTC | Modify/add to NewBaseSystem to match with what is needed for proof of ring isomorphism to F | 02 March 2017, 03:00:37 UTC |
| 15d1439 | jadep | 01 March 2017, 22:20:08 UTC | Fixed carry bugs (indexes need to be reversed, and we need to convert to/from Positional every time we carry) and added an [encode] function | 01 March 2017, 22:20:42 UTC |
| 9b710b5 | jadep | 01 March 2017, 16:42:38 UTC | Defined [div] and [mod]; removed liftn_sig lemmas because they were actually no longer needed | 01 March 2017, 22:20:42 UTC |
| e9b9ddb | Jason Gross | 01 March 2017, 21:58:06 UTC | Adjust implicits of flatten_binding_list_same_in_eq | 01 March 2017, 21:58:06 UTC |
| 2a7e11e | Jason Gross | 01 March 2017, 21:56:29 UTC | Add flatten_binding_list_In_eq_iff, flatten_binding_list_same_in_eq | 01 March 2017, 21:56:29 UTC |
| e04c5d0 | Jason Gross | 01 March 2017, 20:32:35 UTC | Add η principles for sigma types | 01 March 2017, 20:32:35 UTC |
| 28b9e1d | Jason Gross | 01 March 2017, 18:27:39 UTC | Add dlet_nd notation This is for non-dependent [dlet]s, to help Coq's type inference | 01 March 2017, 18:27:39 UTC |
| 6b3048c | Jason Gross | 12 January 2017, 02:02:50 UTC | Switch to fully uncurried form for reflection This will eventually make a number of proofs easier. Unfortunately, the correctness lemmas for AddCoordinates and LadderStep no longer work (because of different arities), and there's a proof in Experiments/Ed25519 that I've admitted. The correctness lemmas will be easy to re-add when we have a more general version that handle arbitrary type shapes. | 01 March 2017, 16:45:47 UTC |
| 80dc66a | Jason Gross | 28 February 2017, 23:32:43 UTC | Add interp_flat_type_rel_pointwise_SmartVarfMap, interp_flat_type_rel_pointwise_Reflexive | 28 February 2017, 23:32:43 UTC |
| 945bb1c | Jason Gross | 28 February 2017, 23:10:18 UTC | Add SmartVarfMap Proper instance | 28 February 2017, 23:10:18 UTC |
| d92aecb | Jason Gross | 28 February 2017, 21:02:48 UTC | Add strip_eta_tuple lemmas | 28 February 2017, 21:02:48 UTC |
| e964773 | Jason Gross | 28 February 2017, 20:52:03 UTC | Better tuple_eta arguments | 28 February 2017, 20:52:03 UTC |
| 95f78be | Jason Gross | 28 February 2017, 20:14:19 UTC | Add eta_tuple functions These are for getting nicely reduced forms of, e.g., Tuple.map, without knowing exactly what the tuple is | 28 February 2017, 20:14:19 UTC |
| b99dcb2 | Jason Gross | 28 February 2017, 18:59:17 UTC | Deduplicate code There was duplicate code in Reflection.Equality and Reflection.TypeInversion | 28 February 2017, 18:59:17 UTC |
| a6ea73f | jadep | 27 February 2017, 20:53:25 UTC | Defined zero and one for NewBaseSystem | 27 February 2017, 20:54:03 UTC |
| 57e22f6 | jadep | 27 February 2017, 20:46:42 UTC | Added operation (including creating ) | 27 February 2017, 20:54:03 UTC |
| 2a50d69 | Jason Gross | 27 February 2017, 19:09:19 UTC | Update _CoqProject Version-controlled .v files should not be removed from _CoqProject. We can filter them out in the Makefile as necessary so that they don't get built by default, but if we desynchronize _CoqProject, then we can end up with confusing error messages that depend on which .v.d files are left over from previous builds. | 27 February 2017, 19:09:21 UTC |
| 52d5918 | jadep | 27 February 2017, 18:33:55 UTC | Added subtraction | 27 February 2017, 18:33:55 UTC |
| b94f708 | jadep | 27 February 2017, 16:55:10 UTC | added Positional wrappers for Associational operations, added correctness proof of | 27 February 2017, 16:55:34 UTC |
| 1fb1958 | jadep | 27 February 2017, 15:51:56 UTC | changed names of ops in NewBaseSystem to reflect that they are sig and not sigT | 27 February 2017, 15:51:56 UTC |
| ed53a28 | jadep | 26 February 2017, 19:16:02 UTC | Modified lemma and created tactic to handle it; added reduce step to multiplication operation; introduced modular equality to NewBaseSystem | 26 February 2017, 19:16:02 UTC |
| 69e3a21 | jadep | 26 February 2017, 17:09:26 UTC | removed leftover saturated stuff (will probably end up in a separate file someday) | 26 February 2017, 17:09:26 UTC |
| 60c9043 | Andres Erbsen | 23 February 2017, 19:55:18 UTC | speed up NewBaseystem synthesis Use a vm_compute hack fromhttps://arxiv.org/pdf/1305.6543.pdf section 5.5: pattern terms over what to keep opaque, then reduce the lambda using vm_compute. | 23 February 2017, 19:57:11 UTC |
| 2bda7f1 | Jason Gross | 23 February 2017, 17:03:09 UTC | Add BoundsInterpretations | 23 February 2017, 17:03:09 UTC |
| 18c5ee8 | Jason Gross | 23 February 2017, 16:43:50 UTC | Add log and non-log versions of FixedWordSizes lem | 23 February 2017, 16:43:50 UTC |
| 49eefc7 | Jason Gross | 23 February 2017, 16:26:50 UTC | Add invert_Some; add nat_N_Z to push_Zof_N | 23 February 2017, 16:26:50 UTC |
| aec88b3 | Jason Gross | 23 February 2017, 16:26:22 UTC | Minor change to reflection naming | 23 February 2017, 16:26:22 UTC |
| 371b69d | jadep | 23 February 2017, 15:20:07 UTC | added explanation of why CPS is useful | 23 February 2017, 15:20:49 UTC |
| 2b10dce | Andres Erbsen | 23 February 2017, 03:06:52 UTC | Merge rebased branch 'ed25519-fix' | 23 February 2017, 03:07:01 UTC |
| 8ee588a | jadep | 14 February 2017, 17:02:01 UTC | Removed code that will be completely replaced in the future; replaced some pointencoding things with axioms pending pointencoding rewrite by Andres | 23 February 2017, 02:45:56 UTC |
| 471465f | jadep | 14 February 2017, 14:57:43 UTC | move lemmas from Ed25519 to WordUtil | 23 February 2017, 02:45:56 UTC |
| 8c78ad4 | jadep | 13 February 2017, 20:44:54 UTC | move some lemmas from Ed25519 to ZUtil | 23 February 2017, 02:45:56 UTC |
| febcf9b | jadep | 13 February 2017, 19:25:52 UTC | moved more stuff to NUtil | 23 February 2017, 02:45:56 UTC |
| 305253c | jadep | 13 February 2017, 18:07:18 UTC | Moved N lemmas from Ed25519 and IterAssocOp into new NUtil file | 23 February 2017, 02:45:56 UTC |
| 5263553 | jadep | 13 February 2017, 17:42:29 UTC | categorize the rest of the stuff in Ed25519 | 23 February 2017, 02:45:56 UTC |
| b6db13e | jadep | 13 February 2017, 17:27:05 UTC | categorize some of the stuff in Ed25519 | 23 February 2017, 02:45:56 UTC |
| 453fa72 | Andres Erbsen | 23 February 2017, 02:24:39 UTC | NewBaseSystem: less verbose | 23 February 2017, 02:24:39 UTC |
| ce10def | jadephilipoom | 22 February 2017, 23:44:33 UTC | Merge new base system (#112) * Added sketch of new low-level base system code * Implemented and proved addition * Implemented carrying, which requires defining over Z rather than arbitrary ring * Proved carry and proved ring-ness of base system ops * Implemented split operation * Started implementing modular reduction * NewBaseSystem: prettify some proofs * andres base * improve andresbase * new base * first draft of goldilocks karatsuba * Factored out goldilocks karatsuba * Implement and prove karatsuba * goldilocks cleanup remodularize * merge karatsuba and goldilocs karatsuba parameter blocks * carry impl and proofs (not yet synthesis-ready) * newbasesystem: use rewrite databases * carry index range fix (TODO: allow for carry-then-reduce) * simpler carry implementation * Added compact operation for saturated base systems (this handles carries after multiplying or adding) * debugging reduction for compact_rows * rewrote compact * Converted saturated section to CPS * some progress on cps conversion for non-saturated stuff * Converted associational non-saturated code to CPS, temporarily commented out examples * pushed cps conversion through Positional * moved list/tuple stuff to top of file * proved lingering lemma * worked on generic-style goal for simplified operations * finished proving the generic-form example goal, revising a couple earlier lemmas * revised previous lemmas * finished revising previous lemmas * removed commented-out code * fixed non-terminating string in comment * fix for 8.5 * removed old file * better automation part 1 * better automation part 2 (goodbye proofs) * better automation part 3/3 * some work on freeze * remove saturated code and clean up exported-operations code * Move helper lemmas for list/tuple CPS stuff to new CPSUtil file * qualified imports * fix runtime notations and module-level Let as per comments * moved push_id to CPSUtil and cancel_pair lemmas to Prod * fixed typo * correctly generalized and moved lift_tuple2 (now called lift2_sig) and converted chained_carries into a fold * moved karatsuba section to new file * rename lemmas and definitions (now cps definitions are consistently <name>_cps and non-cps equivalents have no suffix) * updated timing on mulT * renamed push_eval to push_basesystem_eval | 22 February 2017, 23:44:33 UTC |
| 57a0a97 | Jason Gross | 22 February 2017, 02:35:15 UTC | Add various reflection improvements, boundbycast | 22 February 2017, 02:35:15 UTC |
| 371ba4b | Jason Gross | 21 February 2017, 20:12:57 UTC | Add interpf_smart_bound without exprf | 21 February 2017, 20:12:57 UTC |
| b7d2af4 | Jason Gross | 21 February 2017, 18:17:19 UTC | Rename Interp lemmas ```bash $ git grep --name-only 'Interp_InlineCast\|Interp_InlineConst\|Interp_Linearize' | xargs sed s'/Interp_/Interp/g' -i ``` | 21 February 2017, 18:17:19 UTC |
| b10381a | Jason Gross | 16 February 2017, 22:32:27 UTC | Add non-exprf version of interpf_smart_unbound | 16 February 2017, 22:32:27 UTC |
| 69993c7 | Jason Gross | 16 February 2017, 22:03:01 UTC | Add MapCastInterp | 16 February 2017, 22:03:01 UTC |
| 661072f | Jason Gross | 16 February 2017, 21:53:45 UTC | Add InterpByIsoProofs | 16 February 2017, 21:53:45 UTC |
| 9a71a7a | Jason Gross | 16 February 2017, 20:02:31 UTC | Add more display logs | 16 February 2017, 20:02:31 UTC |
| 0bdec2c | Jason Gross | 16 February 2017, 19:57:52 UTC | Fix typo | 16 February 2017, 19:57:52 UTC |
| f82872a | Jason Gross | 16 February 2017, 19:56:47 UTC | Add InterpByIso It's actually closer to interp_by_retraction... This lets you do [interp] on, e.g., products with fail-values (var * interp_base), as long as [var] is pointed. | 16 February 2017, 19:56:47 UTC |
| 27b1da9 | Jason Gross | 15 February 2017, 21:07:17 UTC | Add more display logs | 15 February 2017, 21:07:17 UTC |
| 316358c | Jason Gross | 15 February 2017, 21:04:34 UTC | make update-_CoqProject | 15 February 2017, 21:04:34 UTC |
| 5f92804 | Jason Gross | 15 February 2017, 21:04:12 UTC | Add some display logs | 15 February 2017, 21:04:12 UTC |
| c08d246 | Jason Gross | 15 February 2017, 21:03:53 UTC | Add some display logs | 15 February 2017, 21:03:53 UTC |
| d957f8d | Jason Gross | 15 February 2017, 21:03:16 UTC | ./copy_bounds | 15 February 2017, 21:03:16 UTC |
| efe4ef7 | Jason Gross | 15 February 2017, 21:01:11 UTC | Add rudimentary Java and C notation files, display | 15 February 2017, 21:01:11 UTC |
| 5bddc2b | Jason Gross | 15 February 2017, 00:45:52 UTC | Remove useless comment | 15 February 2017, 00:45:52 UTC |
| ceb59f8 | Jason Gross | 15 February 2017, 00:45:30 UTC | Mostly finish Wf_Boundify | 15 February 2017, 00:45:30 UTC |
| 98ae0a7 | Jason Gross | 15 February 2017, 00:41:45 UTC | Prove wff_bound_op | 15 February 2017, 00:41:45 UTC |
| 059e05c | Jason Gross | 14 February 2017, 21:03:58 UTC | Stub for wff_bound_op | 14 February 2017, 21:03:58 UTC |
| 890e3a7 | Jason Gross | 14 February 2017, 20:59:14 UTC | Add Wf_MapInterpCast to wf database | 14 February 2017, 20:59:14 UTC |
| b624825 | Jason Gross | 14 February 2017, 20:58:45 UTC | A bit more progress on BoundByCastWf | 14 February 2017, 20:58:45 UTC |
| 7b0b1cb | Jason Gross | 14 February 2017, 20:57:42 UTC | Add partially finished MapCastWf | 14 February 2017, 20:57:42 UTC |
| 8a90b07 | Jason Gross | 14 February 2017, 05:19:04 UTC | Add src/Reflection/BoundByCastWf.v | 14 February 2017, 05:19:04 UTC |
| 81364d2 | Jason Gross | 14 February 2017, 05:17:39 UTC | Update assumptions in src/Reflection/SmartBoundWf.v | 14 February 2017, 05:17:39 UTC |
| 62b34f2 | Jason Gross | 14 February 2017, 05:14:50 UTC | Add SmartBoundWf | 14 February 2017, 05:14:50 UTC |
| 5cbd80e | Jason Gross | 14 February 2017, 03:47:18 UTC | Prove nicer version of wf_SmartAbs | 14 February 2017, 03:47:18 UTC |
| 401297c | Jason Gross | 14 February 2017, 03:43:23 UTC | Add partially admitted lemma wf_SmartAbs | 14 February 2017, 03:43:23 UTC |
| 8bf0d79 | Jason Gross | 14 February 2017, 00:00:08 UTC | More uniform naming | 14 February 2017, 00:00:08 UTC |
| b6801b0 | Jason Gross | 13 February 2017, 23:55:27 UTC | Generalize EtaWf some (still one admit) | 13 February 2017, 23:55:27 UTC |
| 1dec2db | Jason Gross | 13 February 2017, 23:41:44 UTC | Add InlineCastInterp.v | 13 February 2017, 23:41:44 UTC |
| 2a6b992 | Jason Gross | 13 February 2017, 21:00:12 UTC | Add InlineCastWf | 13 February 2017, 21:00:12 UTC |
| 3b27d17 | Jason Gross | 13 February 2017, 20:45:29 UTC | Better cleanup in type_inversion | 13 February 2017, 20:45:29 UTC |
| 5895174 | Jason Gross | 13 February 2017, 20:44:11 UTC | Better type_inversion Now we don't loop on [Unit = Unit] hypotheses, clearing them instead. | 13 February 2017, 20:44:11 UTC |
| d650bb9 | Jason Gross | 13 February 2017, 20:40:07 UTC | Split off inversion_wff for constr-only hyps | 13 February 2017, 20:40:07 UTC |
| 7df92d6 | Jason Gross | 13 February 2017, 20:30:02 UTC | Add inversion_type | 13 February 2017, 20:30:02 UTC |
| 85f2903 | Jason Gross | 13 February 2017, 19:58:09 UTC | Generalize InlineWf | 13 February 2017, 19:58:09 UTC |
| d38d1a2 | Jason Gross | 13 February 2017, 19:39:13 UTC | Add SmartCast{Interp,Wf} | 13 February 2017, 19:39:13 UTC |
| 093834a | Jason Gross | 13 February 2017, 19:01:56 UTC | Split up BoundByCast | 13 February 2017, 19:01:56 UTC |
| f5ed7d8 | Jason Gross | 10 February 2017, 21:27:32 UTC | Generalize BoundByCast a bit The rules for handling | / & vs >> are different; we can truncate early on | / &, but not on >> | 10 February 2017, 21:27:32 UTC |
| 0c285f6 | Jason Gross | 10 February 2017, 21:10:44 UTC | Add EtaInterp, EtaWf | 10 February 2017, 21:10:44 UTC |
| 5a21585 | Jason Gross | 10 February 2017, 21:07:24 UTC | Use Eta in BoundByCast | 10 February 2017, 21:07:24 UTC |
| 7aac6f3 | Jason Gross | 10 February 2017, 21:04:20 UTC | Add Reflection/Eta.v | 10 February 2017, 21:04:20 UTC |
| 5ec315e | Jason Gross | 10 February 2017, 20:59:31 UTC | Fix a missing section close in ZToRing | 10 February 2017, 20:59:31 UTC |
| 6596935 | Jason Gross | 10 February 2017, 20:58:19 UTC | Add files for constant reflective notations | 10 February 2017, 20:58:19 UTC |
| 32849ba | jadep | 10 February 2017, 14:03:24 UTC | Accidentally pushed wrong file in last commit; this is the correct one | 10 February 2017, 14:03:24 UTC |
| bcc7277 | jadep | 09 February 2017, 19:01:40 UTC | added ZToRing to _CoqProject | 09 February 2017, 19:01:40 UTC |
| 750fe71 | jadep | 09 February 2017, 19:00:49 UTC | Added ZToRing lemmas | 09 February 2017, 19:00:49 UTC |
| 565785d | Jason Gross | 09 February 2017, 01:26:46 UTC | Remove useless imports | 09 February 2017, 01:26:46 UTC |
| 77a82e0 | Jason Gross | 09 February 2017, 01:25:23 UTC | Factor things into BoundByCast.v | 09 February 2017, 01:25:23 UTC |
| 430e03e | Jason Gross | 09 February 2017, 00:07:43 UTC | Fix type inference bug in 8.6 | 09 February 2017, 00:07:48 UTC |
| 1701df7 | Jason Gross | 08 February 2017, 21:04:33 UTC | Simpler version of MapCast Unfortunately, more of the casting logic is in MultiSizeTest2, now. I plan to make it more generic soon. | 08 February 2017, 21:04:33 UTC |
| eadfe1c | Jason Gross | 08 February 2017, 01:30:04 UTC | Remove the let-in from SmartValf It messes with reduction elsewhere | 08 February 2017, 01:30:04 UTC |
| 929d223 | Jason Gross | 08 February 2017, 00:46:17 UTC | Fix relation relb arguments | 08 February 2017, 00:46:17 UTC |
| d9d216d | Jason Gross | 08 February 2017, 00:35:21 UTC | Add things like interp_flat_type_rel_pointwise1_gen_Prop_iff_bool Because [simpl] unfolds things, so we want lemmas to rewrite with even after [simpl] | 08 February 2017, 00:35:21 UTC |
