aboutsummaryrefslogtreecommitdiff
path: root/src
Commit message (Collapse)AuthorAge
* rewrite ExtendedCoordinates, fix Ed25519Gravatar Andres Erbsen2017-03-02
|
* edwards curves over isomorphic fieldsGravatar Andres Erbsen2017-03-02
|
* src/Tactics/Algebra_syntax/Nsatz.v: power 1 onlyGravatar Andres Erbsen2017-03-02
|
* WIPGravatar Andres Erbsen2017-03-02
|
* address some code review commentsGravatar Andres Erbsen2017-03-02
|
* Weierstrass curve is a groupGravatar Andres Erbsen2017-03-02
|
* Attempt Weierstrass associativity again, good progress.Gravatar Andres Erbsen2017-03-02
|
* change weierstrass spec, prove most cases of associativityGravatar Andres Erbsen2017-03-02
|
* split the algebra library; use fsatz moreGravatar Andres Erbsen2017-03-02
|
* fsatz, nsatz_solve_nonzeroGravatar Andres Erbsen2017-03-02
|
* use field_nsatz in CompleteEdwardsCurve.PreGravatar Andres Erbsen2017-03-02
|
* field_nsatzGravatar Andres Erbsen2017-03-02
|
* make assert_preconditions way more sane; use vm_decide to kill most subgoalsGravatar jadep2017-03-02
|
* Separated out [carry] from other operations.Gravatar jadep2017-03-02
|
* Modify/add to NewBaseSystem to match with what is needed for proof of ring ↵Gravatar jadep2017-03-01
| | | | isomorphism to F
* Fixed carry bugs (indexes need to be reversed, and we need to convert ↵Gravatar jadep2017-03-01
| | | | to/from Positional every time we carry) and added an [encode] function
* Defined [div] and [mod]; removed liftn_sig lemmas because they were actually ↵Gravatar jadep2017-03-01
| | | | no longer needed
* Adjust implicits of flatten_binding_list_same_in_eqGravatar Jason Gross2017-03-01
|
* Add flatten_binding_list_In_eq_iff, flatten_binding_list_same_in_eqGravatar Jason Gross2017-03-01
|
* Add η principles for sigma typesGravatar Jason Gross2017-03-01
|
* Add dlet_nd notationGravatar Jason Gross2017-03-01
| | | | This is for non-dependent [dlet]s, to help Coq's type inference
* Switch to fully uncurried form for reflectionGravatar Jason Gross2017-03-01
| | | | | | | | | | | 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.
* Add interp_flat_type_rel_pointwise_SmartVarfMap, ↵Gravatar Jason Gross2017-02-28
| | | | interp_flat_type_rel_pointwise_Reflexive
* Add SmartVarfMap Proper instanceGravatar Jason Gross2017-02-28
|
* Add strip_eta_tuple lemmasGravatar Jason Gross2017-02-28
|
* Better tuple_eta argumentsGravatar Jason Gross2017-02-28
|
* Add eta_tuple functionsGravatar Jason Gross2017-02-28
| | | | | These are for getting nicely reduced forms of, e.g., Tuple.map, without knowing exactly what the tuple is
* Deduplicate codeGravatar Jason Gross2017-02-28
| | | | There was duplicate code in Reflection.Equality and Reflection.TypeInversion
* Defined zero and one for NewBaseSystemGravatar jadep2017-02-27
|
* Added operation (including creating )Gravatar jadep2017-02-27
|
* Added subtractionGravatar jadep2017-02-27
|
* added Positional wrappers for Associational operations, added correctness ↵Gravatar jadep2017-02-27
| | | | proof of
* changed names of ops in NewBaseSystem to reflect that they are sig and not sigTGravatar jadep2017-02-27
|
* Modified lemma and created tactic to handle it; added reduce step to ↵Gravatar jadep2017-02-26
| | | | multiplication operation; introduced modular equality to NewBaseSystem
* removed leftover saturated stuff (will probably end up in a separate file ↵Gravatar jadep2017-02-26
| | | | someday)
* speed up NewBaseystem synthesisGravatar Andres Erbsen2017-02-23
| | | | | | 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.
* Add BoundsInterpretationsGravatar Jason Gross2017-02-23
|
* Add log and non-log versions of FixedWordSizes lemGravatar Jason Gross2017-02-23
|
* Add invert_Some; add nat_N_Z to push_Zof_NGravatar Jason Gross2017-02-23
|
* Minor change to reflection namingGravatar Jason Gross2017-02-23
|
* added explanation of why CPS is usefulGravatar jadep2017-02-23
|
* Removed code that will be completely replaced in the future; replaced some ↵Gravatar jadep2017-02-22
| | | | pointencoding things with axioms pending pointencoding rewrite by Andres
* move lemmas from Ed25519 to WordUtilGravatar jadep2017-02-22
|
* move some lemmas from Ed25519 to ZUtilGravatar jadep2017-02-22
|
* moved more stuff to NUtilGravatar jadep2017-02-22
|
* Moved N lemmas from Ed25519 and IterAssocOp into new NUtil fileGravatar jadep2017-02-22
|
* categorize the rest of the stuff in Ed25519Gravatar jadep2017-02-22
|
* categorize some of the stuff in Ed25519Gravatar jadep2017-02-22
|
* NewBaseSystem: less verboseGravatar Andres Erbsen2017-02-22
|
* Merge new base system (#112)Gravatar jadephilipoom2017-02-22
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | * 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-05 08:40:42 +0000