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

row-wise flatten #324

Closed
wants to merge 31 commits into from
Closed

row-wise flatten #324

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
31 commits
Select commit Hold shift + click to select a range
1cff7d0
some work on rowwise flatten
jadephilipoom Feb 28, 2018
fb0d01a
preliminary version of rowwise flatten
jadephilipoom Feb 28, 2018
215f3de
rowwise flatten (more fleshed-out) and proof outline
jadephilipoom Mar 1, 2018
ada3906
prove sum_rows_div_mod and fix up Rows.from_columns a bit
jadephilipoom Mar 2, 2018
08da5da
clean up proofs a bit
jadephilipoom Mar 2, 2018
ee3c375
progress on from_columns proofs
jadephilipoom Mar 2, 2018
0dff238
finish from_columns proofs
jadephilipoom Mar 2, 2018
30ec66d
proved admits about sum_rows
jadephilipoom Mar 2, 2018
f0ab368
finish flatten_partitions and slightly change the format of _partitio…
jadephilipoom Mar 6, 2018
4ef6797
move mul_converted to its own module
jadephilipoom Mar 6, 2018
80300fa
add Rows.from_associational and some more length proofs that allow Ro…
jadephilipoom Mar 6, 2018
5154315
Make Montgomery example use row-wise flatten (involves adding Nat.max…
jadephilipoom Mar 6, 2018
59d2810
inline shifts for Montgomery example
jadephilipoom Mar 6, 2018
153e54b
make add_with_get_carry with a constant zero for the carry translate …
jadephilipoom Mar 6, 2018
97420c7
inline lands and also shifts/lands of (fst (Var _ _))
jadephilipoom Mar 6, 2018
87aca56
changing Montgomery notations
jadephilipoom Mar 6, 2018
60fd532
fix typo and add booleans for carries
jadephilipoom Mar 7, 2018
00897b2
move some lemmas/hints to ListUtil
jadephilipoom Mar 7, 2018
b99d85e
clean up some [flatten] proofs
jadephilipoom Mar 7, 2018
dadb07f
more cleanup of flatten proofs
jadephilipoom Mar 7, 2018
bb360cf
organize proofs into sections
jadephilipoom Mar 7, 2018
f8d4fa0
organize Rows into sections
jadephilipoom Mar 7, 2018
7749df7
automate some Rows proofs
jadephilipoom Mar 8, 2018
a3197ae
more proof automation in Rows
jadephilipoom Mar 8, 2018
8d158e3
reprint Montgomery output (order of additions in Rows.flatten changed)
jadephilipoom Mar 8, 2018
5ab37f3
move some shared lemmas between Columns/Rows into a Saturated module
jadephilipoom Mar 8, 2018
dd83644
move some lemmas to ZUtil/ListUtil
jadephilipoom Mar 8, 2018
b49688c
make a more general kind of mul_converted_halve that produces the cor…
jadephilipoom Mar 8, 2018
1802315
rename w_half to w_mul
jadephilipoom Mar 8, 2018
8655b72
make montgomery not depend on intermediate weight for multiplication …
jadephilipoom Mar 8, 2018
fd29a0e
move requires to the top of the file
jadephilipoom Mar 9, 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
Loading