| Commit message (Collapse) | Author | Age |
|---|
| | |
|
| |
|
|
| |
This is for non-dependent [dlet]s, to help Coq's type inference
|
| |
|
|
|
|
|
|
|
|
|
| |
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.
|
| |
|
|
| |
interp_flat_type_rel_pointwise_Reflexive
|
| | |
|
| | |
|
| | |
|
| |
|
|
|
| |
These are for getting nicely reduced forms of, e.g., Tuple.map, without
knowing exactly what the tuple is
|
| |
|
|
| |
There was duplicate code in Reflection.Equality and Reflection.TypeInversion
|
| | |
|
| | |
|
| | |
|
| |
|
|
| |
proof of
|
| | |
|
| |
|
|
| |
multiplication operation; introduced modular equality to NewBaseSystem
|
| |
|
|
| |
someday)
|
| |
|
|
|
|
| |
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.
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| |
|
|
| |
pointencoding things with axioms pending pointencoding rewrite by Andres
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
* 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
|
| | |
|
| | |
|
| |
|
|
|
|
| |
```bash
$ git grep --name-only 'Interp_InlineCast\|Interp_InlineConst\|Interp_Linearize' | xargs sed s'/Interp_/Interp/g' -i
```
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| |
|
|
|
|
| |
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.
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
Jason Gross
jadep
Andres Erbsen