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

Remove rweight #337

Merged
merged 2 commits into from
Mar 29, 2018
Merged

Remove rweight #337

merged 2 commits into from
Mar 29, 2018

Conversation

JasonGross
Copy link
Collaborator

No description provided.

@andres-erbsen
Copy link
Contributor 

File "./src/Experiments/SimplyTypedArithmetic.v", line 7450, characters 14-21:
Error: The reference rweight was not found in the current environment.

andres-erbsen
andres-erbsen approved these changes Mar 27, 2018
View reviewed changes
Copy link
Contributor

@andres-erbsen andres-erbsen left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Approved as long assuming you get it to build in a boring way / by doing similar transformations as in the rest of the file.

src/Experiments/SimplyTypedArithmetic.v
(Hc : length c = len_c)
(Hidxs : length idxs = len_idxs).
Definition weight (i : nat)
:= 2^(-(-(limbwidth_num * i) / limbwidth_den)).
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

is the double negation used here to make it round up? I don't know whether the trick here works, but I would believe you if you said it does. In C I often use (n + d - 1)/d for rounding up. Edit: hah, you proved it correct below. I approve of both the trick and the fact that the code was already set up in a way to make it the right thing to do to prove it.

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I got the "trick" by unfolding Qceiling (Z.pos (Z.to_pos num) / Z.to_pos den) and then removing the matches

src/Experiments/SimplyTypedArithmetic.v Outdated
expand_lists ().
subst carrymod; reflexivity.
Qed.
Local Lemma weight_0 : weight 0 = 1.
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Could you get this lemma and the next from lemmas about 2^Qceiling(limbwidth*i) ? Or are your proofs intentionally duplicative because they look simpler?

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I was originally trying to be as permissive as possible. I'll strengthen the hypotheses to require 0 < limbwidth_den which is required for basing it on 2^Qceiling(limbwidth*i) to actually be a simplification.

src/Experiments/SimplyTypedArithmetic.v
@@ -6419,21 +6418,21 @@ Section rcarry_mul.
Definition rcarry_mul
:= BoundsPipeline
(carry_mul_gen
@ rw @ GallinaReify.Reify s @ GallinaReify.Reify c @ GallinaReify.Reify n @ GallinaReify.Reify (length c) @ GallinaReify.Reify idxs @ GallinaReify.Reify (length idxs))
@ GallinaReify.Reify (Qnum limbwidth) @ GallinaReify.Reify (Z.pos (Qden limbwidth)) @ GallinaReify.Reify s @ GallinaReify.Reify c @ GallinaReify.Reify n @ GallinaReify.Reify (length c) @ GallinaReify.Reify idxs @ GallinaReify.Reify (length idxs))
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

It might be easier to take in (Z*Z) instead of Q for the limbwidth. either is fine by me.

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Huh? limbwidth is computed in this section. I could also let-bind the numerator and denominator....

src/Experiments/SimplyTypedArithmetic.v
@@ -6591,6 +6584,7 @@ Section rcarry_mul.
| intros; apply eval_oppmod
| intros; apply eval_encodemod
| eassumption
| apply conj
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I remember having issues with non-conditional (e?)apply conj looping. if you think it's fine here then it's most likely fine

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

If it starts looping, I'll get rid of it. But this is really a very simple proof that goes by eauto modulo beta-iota-delta.

@JasonGross
Copy link
Collaborator Author

Updated to build to the end by plugging in a concrete weight function and proving a few extra lemmas.

@JasonGross
Copy link
Collaborator Author

@jadephilipoom Are you okay with the changes to montred that inline the weight function? I tried to do things in a way that minimally impacted your proof (so definitely feel free to later rewrite it more or whatever).

jadephilipoom
jadephilipoom approved these changes Mar 28, 2018
View reviewed changes
src/Experiments/SimplyTypedArithmetic.v
Let w_divides : forall i : nat, w (S i) / w i > 0
:= weight_divides _ _ log2R_good.
Let w_1_gt1 : w 1 > 1 := weight_1_gt_1 _ _ log2R_good.
Let w_half_1_gt1 : w_half 1 > 1 := weight_1_gt_1 _ _ half_log2R_good.
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Ugh, this is quite a lot of boilerplate. I was thinking of maybe making a record or something for saturated weight functions, and maybe this is another point for that strategy.

@JasonGross JasonGross merged commit f17f20e into mit-plv:master Mar 29, 2018
@JasonGross JasonGross deleted the no-rweight branch March 29, 2018 00:06
JasonGross added a commit to JasonGross/fiat-crypto that referenced this pull request Feb 21, 2022
@JasonGross
Better error messages
c543bda 
Probably if the lists are the same lengths, then we want to compare them
element-wise rather than all at once.  It's way too verbose to keep
expanding them, so we only do that when lists are not the same length.

We now get error messages such as
```
Unable to unify: [inr [378, 381, 384]] == [inr [101, 106, 108]]
Could not unify the values at index 0: [mit-plv#378, mit-plv#381, mit-plv#384] != [mit-plv#101, mit-plv#106, mit-plv#108]
index 0: mit-plv#378 != mit-plv#101
(slice 0 44, [mit-plv#377]) != (slice 0 44, [mit-plv#98])
index 0: mit-plv#377 != mit-plv#98
(add 64, [mit-plv#345, mit-plv#375]) != (add 64, [#57, mit-plv#96])
index 0: mit-plv#345 != #57
(slice 0 44, [mit-plv#337]) != (slice 0 44, [#44])
index 0: mit-plv#337 != #44
(add 64, [#41, mit-plv#334]) != (add 64, [#25, #41])
index 1: mit-plv#334 != #25
(mul 64, [#1, mit-plv#331]) != (mul 64, [#0, #1, #22])
[(add 64, [mit-plv#329, mit-plv#329])] != [#0, (const 20, [])]
[(add 64, [(mul 64, [#7, mit-plv#328]), (mul 64, [#7, mit-plv#328])])] != [#0, (const 20, [])]
[(add 64, [(mul 64, [(const 2, []), (add 64, [#0, mit-plv#327])]), (mul 64, [(const 2, []), (add 64, [#0, mit-plv#327])])])] != [#0, (const 20, [])]
[(add 64, [(mul 64, [(const 2, []), (add 64, [#0, (mul 64, [#0, mit-plv#326])])]), (mul 64, [(const 2, []), (add 64, [#0, (mul 64, [#0, mit-plv#326])])])])] != [#0, (const 20, [])]
[(add 64, [(mul 64, [(const 2, []), (add 64, [#0, (mul 64, [#0, (const 4, [])])])]), (mul 64, [(const 2, []), (add 64, [#0, (mul 64, [#0, (const 4, [])])])])])] != [#0, (const 20, [])]
[(add 64, [(mul 64, [(const 2, []), (add 64, [(old 64 0, []), (mul 64, [(old 64 0, []), (const 4, [])])])]), (mul 64, [(const 2, []), (add 64, [(old 64 0, []), (mul 64, [(old 64 0, []), (const 4, [])])])])])] != [(old 64 0, []), (const 20, [])]
```

The second to last line is generally the one to look at; the last line
adds a bit more detail to it.  Perhaps we should instead list out the
values of indices rather than expanding one additional level?
JasonGross added a commit to JasonGross/fiat-crypto that referenced this pull request Feb 21, 2022
@JasonGross
Better error messages
bde03cc 
Probably if the lists are the same lengths, then we want to compare them
element-wise rather than all at once.  It's way too verbose to keep
expanding them, so we only do that when lists are not the same length.

We now get error messages such as
```
Unable to unify: [inr [378, 381, 384]] == [inr [101, 106, 108]]
Could not unify the values at index 0: [mit-plv#378, mit-plv#381, mit-plv#384] != [mit-plv#101, mit-plv#106, mit-plv#108]
index 0: mit-plv#378 != mit-plv#101
(slice 0 44, [mit-plv#377]) != (slice 0 44, [mit-plv#98])
index 0: mit-plv#377 != mit-plv#98
(add 64, [mit-plv#345, mit-plv#375]) != (add 64, [#57, mit-plv#96])
index 0: mit-plv#345 != #57
(slice 0 44, [mit-plv#337]) != (slice 0 44, [#44])
index 0: mit-plv#337 != #44
(add 64, [#41, mit-plv#334]) != (add 64, [#25, #41])
index 1: mit-plv#334 != #25
(mul 64, [#1, mit-plv#331]) != (mul 64, [#0, #1, #22])
[(add 64, [mit-plv#329, mit-plv#329])] != [#0, (const 20, [])]
[(add 64, [(mul 64, [#7, mit-plv#328]), (mul 64, [#7, mit-plv#328])])] != [#0, (const 20, [])]
[(add 64, [(mul 64, [(const 2, []), (add 64, [#0, mit-plv#327])]), (mul 64, [(const 2, []), (add 64, [#0, mit-plv#327])])])] != [#0, (const 20, [])]
[(add 64, [(mul 64, [(const 2, []), (add 64, [#0, (mul 64, [#0, mit-plv#326])])]), (mul 64, [(const 2, []), (add 64, [#0, (mul 64, [#0, mit-plv#326])])])])] != [#0, (const 20, [])]
[(add 64, [(mul 64, [(const 2, []), (add 64, [#0, (mul 64, [#0, (const 4, [])])])]), (mul 64, [(const 2, []), (add 64, [#0, (mul 64, [#0, (const 4, [])])])])])] != [#0, (const 20, [])]
[(add 64, [(mul 64, [(const 2, []), (add 64, [(old 64 0, []), (mul 64, [(old 64 0, []), (const 4, [])])])]), (mul 64, [(const 2, []), (add 64, [(old 64 0, []), (mul 64, [(old 64 0, []), (const 4, [])])])])])] != [(old 64 0, []), (const 20, [])]
```

The second to last line is generally the one to look at; the last line
adds a bit more detail to it.  Perhaps we should instead list out the
values of indices rather than expanding one additional level?
JasonGross added a commit that referenced this pull request Feb 22, 2022
@JasonGross
Better error messages
cfe296f 
Probably if the lists are the same lengths, then we want to compare them
element-wise rather than all at once.  It's way too verbose to keep
expanding them, so we only do that when lists are not the same length.

We now get error messages such as
```
Unable to unify: [inr [378, 381, 384]] == [inr [101, 106, 108]]
Could not unify the values at index 0: [#378, #381, #384] != [#101, #106, #108]
index 0: #378 != #101
(slice 0 44, [#377]) != (slice 0 44, [#98])
index 0: #377 != #98
(add 64, [#345, #375]) != (add 64, [#57, #96])
index 0: #345 != #57
(slice 0 44, [#337]) != (slice 0 44, [#44])
index 0: #337 != #44
(add 64, [#41, #334]) != (add 64, [#25, #41])
index 1: #334 != #25
(mul 64, [#1, #331]) != (mul 64, [#0, #1, #22])
[(add 64, [#329, #329])] != [#0, (const 20, [])]
[(add 64, [(mul 64, [#7, #328]), (mul 64, [#7, #328])])] != [#0, (const 20, [])]
[(add 64, [(mul 64, [(const 2, []), (add 64, [#0, #327])]), (mul 64, [(const 2, []), (add 64, [#0, #327])])])] != [#0, (const 20, [])]
[(add 64, [(mul 64, [(const 2, []), (add 64, [#0, (mul 64, [#0, #326])])]), (mul 64, [(const 2, []), (add 64, [#0, (mul 64, [#0, #326])])])])] != [#0, (const 20, [])]
[(add 64, [(mul 64, [(const 2, []), (add 64, [#0, (mul 64, [#0, (const 4, [])])])]), (mul 64, [(const 2, []), (add 64, [#0, (mul 64, [#0, (const 4, [])])])])])] != [#0, (const 20, [])]
[(add 64, [(mul 64, [(const 2, []), (add 64, [(old 64 0, []), (mul 64, [(old 64 0, []), (const 4, [])])])]), (mul 64, [(const 2, []), (add 64, [(old 64 0, []), (mul 64, [(old 64 0, []), (const 4, [])])])])])] != [(old 64 0, []), (const 20, [])]
```

The second to last line is generally the one to look at; the last line
adds a bit more detail to it.  Perhaps we should instead list out the
values of indices rather than expanding one additional level?
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@jadephilipoom jadephilipoom jadephilipoom approved these changes

@andres-erbsen andres-erbsen andres-erbsen approved these changes

Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
3 participants
@JasonGross @andres-erbsen @jadephilipoom