Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

rowwise flatten (with merge conflicts fixed) #334

Merged
merged 32 commits into from
Apr 3, 2018
Merged

rowwise flatten (with merge conflicts fixed) #334

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
32 commits
Select commit Hold shift + click to select a range
8d5fb1e
some work on rowwise flatten
jadephilipoom Feb 28, 2018
b09dc07
preliminary version of rowwise flatten
jadephilipoom Feb 28, 2018
ffa2370
rowwise flatten (more fleshed-out) and proof outline
jadephilipoom Mar 1, 2018
e8f3ea3
prove sum_rows_div_mod and fix up Rows.from_columns a bit
jadephilipoom Mar 2, 2018
ed2c5ef
clean up proofs a bit
jadephilipoom Mar 2, 2018
9d6d6a7
progress on from_columns proofs
jadephilipoom Mar 2, 2018
967c7aa
finish from_columns proofs
jadephilipoom Mar 2, 2018
333c4bb
proved admits about sum_rows
jadephilipoom Mar 2, 2018
b96a602
finish flatten_partitions and slightly change the format of _partitio…
jadephilipoom Mar 6, 2018
848692d
move mul_converted to its own module
jadephilipoom Mar 6, 2018
c8b0517
add Rows.from_associational and some more length proofs that allow Ro…
jadephilipoom Mar 6, 2018
747128b
Make Montgomery example use row-wise flatten (involves adding Nat.max…
jadephilipoom Mar 6, 2018
65c3585
inline shifts for Montgomery example
jadephilipoom Mar 6, 2018
c178e9d
make add_with_get_carry with a constant zero for the carry translate …
jadephilipoom Mar 6, 2018
469a24d
changing Montgomery notations
jadephilipoom Mar 6, 2018
b97dfa4
fix typo and add booleans for carries
jadephilipoom Mar 7, 2018
1c4a813
move some lemmas/hints to ListUtil
jadephilipoom Mar 7, 2018
65589b5
clean up some [flatten] proofs
jadephilipoom Mar 7, 2018
fdb715c
more cleanup of flatten proofs
jadephilipoom Mar 7, 2018
0d2aea1
organize proofs into sections
jadephilipoom Mar 7, 2018
06d46fa
organize Rows into sections
jadephilipoom Mar 7, 2018
72f351f
automate some Rows proofs
jadephilipoom Mar 8, 2018
70a6260
more proof automation in Rows
jadephilipoom Mar 8, 2018
459b26e
reprint Montgomery output (order of additions in Rows.flatten changed)
jadephilipoom Mar 8, 2018
4264462
move some shared lemmas between Columns/Rows into a Saturated module
jadephilipoom Mar 8, 2018
6c246bb
move some lemmas to ZUtil/ListUtil
jadephilipoom Mar 8, 2018
c613f51
make a more general kind of mul_converted_halve that produces the cor…
jadephilipoom Mar 8, 2018
c3fe459
rename w_half to w_mul
jadephilipoom Mar 8, 2018
67474ed
make montgomery not depend on intermediate weight for multiplication …
jadephilipoom Mar 8, 2018
b9da6a2
move requires to the top of the file
jadephilipoom Mar 9, 2018
5a8b041
pass-through after Andres's review in #334
jadephilipoom Mar 27, 2018
26a80e1
pass-through after Jason's review
jadephilipoom Mar 28, 2018
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion coqprime
Open in desktop
Submodule coqprime updated 2 files
+0 −6 .gitignore
+1 −1 opam/opam
Loading