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

Fix JGross' Word Admits #91

Merged
merged 11 commits into from Nov 10, 2016
Merged

Fix JGross' Word Admits #91

merged 11 commits into from Nov 10, 2016

Conversation

varomodt
Copy link
Contributor

@varomodt varomodt commented Nov 1, 2016

@JasonGross Almost done -- I'm using a PR so you can review it easily

JasonGross
JasonGross previously requested changes Nov 1, 2016
View reviewed changes
Copy link
Collaborator

@JasonGross JasonGross left a comment

Choose a reason for hiding this comment

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

Thanks! Looking good. In addition to the specific changes mentioned in the review comments, I'd like the following three changes:

  1. There are a lot of long proofs in Z.Interpretations now. Could you factor each of the proofs into "lemmas just about words", which belong in Crypto.WordUtil, and "lemmas just about boundedness of Z operations", which belong in Crypto.ZUtil, and then just make use of those lemmas in Z.Interpretations, like I did for addition, subtractions, and multiplication?
  2. Please merge in or rebase on top of current master.
  3. Please move or copy the lemmas that you need about words and Zs out of the Assembly/ folder, and stick them in WordUtil or ZUtil.

src/Reflection/Z/Interpretations.v
@@ -342,50 +399,204 @@ Module BoundedWord64.
| progress autorewrite with push_word64ToZ
| progress repeat apply conj ].

Tactic Notation "admit" := abstract case proof_admitted.
Ltac ktrans k := do k (etransitivity; [|eassumption]); assumption.
Ltac trans' := first [ assumption | ktrans ltac:1 | ktrans ltac:2 ].
Copy link
Collaborator

Choose a reason for hiding this comment

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

This is not valid in 8.6. Try ltac:(1) and ltac:(2)?

src/Reflection/Z/Interpretations.v
Defined.

Definition mul : t -> t -> t.
Proof.
Ltac mul_mono :=
Copy link
Collaborator

Choose a reason for hiding this comment

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

Please don't put tactics inside proofs. Do Local Ltac ... right above the theorem statement.

src/Reflection/Z/Interpretations.v
Defined.

Definition shl : t -> t -> t.
Proof.
build_binop Word64.w64shl ZBounds.shl; t_start;
admit.
Ltac shl_mono := etransitivity;
Copy link
Collaborator

Choose a reason for hiding this comment

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

Same here: move the Ltac up, make it local

src/Reflection/Z/Interpretations.v
Defined.

Definition shr : t -> t -> t.
Proof.
build_binop Word64.w64shr ZBounds.shr; t_start;
admit.
Ltac shr_mono := etransitivity;
Copy link
Collaborator

Choose a reason for hiding this comment

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

And here: move the Ltac

src/Reflection/Z/Interpretations.v
@@ -164,10 +221,11 @@ Module ZBounds.
Definition shr : t -> t -> t
:= t_map2 (fun lx ly ux uy => {| lower := lx >> uy ; upper := ux >> ly |}).
Definition land : t -> t -> t
:= t_map2 (fun lx ly ux uy => {| lower := 0 ; upper := Z.min ux uy |}).
:= t_map2 (fun lx ly ux uy => {| lower := 0 ;
upper := 2^(Z.succ (Z.min (Z.log2 ux) (Z.log2 uy))) |}).
Copy link
Collaborator

Choose a reason for hiding this comment

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

This is unnecessarily tight. There should be a proof already in ZUtil or the standard library that Z.land x y <= x and Z.land x y <= y for nonnegative things.

src/Reflection/Z/Interpretations.v
Definition lor : t -> t -> t
:= t_map2 (fun lx ly ux uy => {| lower := Z.max lx ly;
upper := 2^(Z.max (Z.log2 (ux+1)) (Z.log2 (uy+1))) - 1 |}).
upper := 2^(Z.succ (Z.max (Z.log2 ux) (Z.log2 uy))) |}).
Copy link
Collaborator

Choose a reason for hiding this comment

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

Isn't there a tighter bound? It would be nice if lor (2^k-1) (2^k-1) said that the upper bound is 2^k-1, not 2^k. (That is, it would be nice if it's always possible to saturate the upper bounds, and if it's the case that repeatedly applying an operation that doesn't change the value won't make the upper bound grow without bound.)

src/Util/WordUtil.v
-> (Z.log2 (Zop (Z.of_N (wordToN x)) (Z.of_N (wordToN y))) < Z.of_nat sz)
-> (Z.of_N (wordToN (wop x y)) = (Zop (Z.of_N (wordToN x)) (Z.of_N (wordToN y)))))%Z).

Require Import Crypto.Assembly.WordizeUtil.
Copy link
Collaborator

Choose a reason for hiding this comment

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

Please move these to the top of the file.

@JasonGross JasonGross merged commit 3552e1b into master Nov 10, 2016
@JasonGross JasonGross deleted the rsloan-patch-wordutil-admits branch November 10, 2016 18:41
dderjoel added a commit to dderjoel/fiat-crypto that referenced this pull request Mar 22, 2022
@dderjoel
another test case
2cd122c 
Unable to unify: [inr [351, 349, 350]] == [inr [103, 108, 110]]
Could not unify the values at index 0: [mit-plv#351, mit-plv#349, mit-plv#350] != [mit-plv#103, mit-plv#108, mit-plv#110]
index 0: mit-plv#351 != mit-plv#103
(slice 0 44, [mit-plv#345]) != (slice 0 44, [mit-plv#100])
index 0: mit-plv#345 != mit-plv#100
(add 64, [mit-plv#58, mit-plv#95, mit-plv#343]) != (add 64, [mit-plv#58, mit-plv#98])
(add 64, [mit-plv#95, mit-plv#343]) != (add 64, [mit-plv#98])
(add 64, [mit-plv#95, (mul 64, [mit-plv#95, mit-plv#331])]) != (add 64, [(mul 64, [#3, mit-plv#95])])
(add 64, [mit-plv#95, (mul 64, [mit-plv#95, (const 4, [])])]) != (add 64, [(mul 64, [#3, mit-plv#95])])
(add 64, [(or 64, [mit-plv#91, mit-plv#93]), (mul 64, [(or 64, [mit-plv#91, mit-plv#93]), (const 4, [])])]) != (add 64, [(mul 64, [(const 5, []), (or 64, [mit-plv#91, mit-plv#93])])])
JasonGross pushed a commit to dderjoel/fiat-crypto that referenced this pull request Mar 22, 2022
@dderjoel @JasonGross
another test case
067efc4 
Unable to unify: [inr [351, 349, 350]] == [inr [103, 108, 110]]
Could not unify the values at index 0: [mit-plv#351, mit-plv#349, mit-plv#350] != [mit-plv#103, mit-plv#108, mit-plv#110]
index 0: mit-plv#351 != mit-plv#103
(slice 0 44, [mit-plv#345]) != (slice 0 44, [mit-plv#100])
index 0: mit-plv#345 != mit-plv#100
(add 64, [mit-plv#58, mit-plv#95, mit-plv#343]) != (add 64, [mit-plv#58, mit-plv#98])
(add 64, [mit-plv#95, mit-plv#343]) != (add 64, [mit-plv#98])
(add 64, [mit-plv#95, (mul 64, [mit-plv#95, mit-plv#331])]) != (add 64, [(mul 64, [#3, mit-plv#95])])
(add 64, [mit-plv#95, (mul 64, [mit-plv#95, (const 4, [])])]) != (add 64, [(mul 64, [#3, mit-plv#95])])
(add 64, [(or 64, [mit-plv#91, mit-plv#93]), (mul 64, [(or 64, [mit-plv#91, mit-plv#93]), (const 4, [])])]) != (add 64, [(mul 64, [(const 5, []), (or 64, [mit-plv#91, mit-plv#93])])])
JasonGross pushed a commit that referenced this pull request Mar 23, 2022
@dderjoel @JasonGross
another test case
b949c76 
Unable to unify: [inr [351, 349, 350]] == [inr [103, 108, 110]]
Could not unify the values at index 0: [#351, #349, #350] != [#103, #108, #110]
index 0: #351 != #103
(slice 0 44, [#345]) != (slice 0 44, [#100])
index 0: #345 != #100
(add 64, [#58, #95, #343]) != (add 64, [#58, #98])
(add 64, [#95, #343]) != (add 64, [#98])
(add 64, [#95, (mul 64, [#95, #331])]) != (add 64, [(mul 64, [#3, #95])])
(add 64, [#95, (mul 64, [#95, (const 4, [])])]) != (add 64, [(mul 64, [#3, #95])])
(add 64, [(or 64, [#91, #93]), (mul 64, [(or 64, [#91, #93]), (const 4, [])])]) != (add 64, [(mul 64, [(const 5, []), (or 64, [#91, #93])])])
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@JasonGross JasonGross JasonGross left review comments

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

Successfully merging this pull request may close these issues.

None yet
2 participants
@varomodt @JasonGross