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.

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

src/lemmas.k.md: rewrite TIME lemma #63

Open
wants to merge 6 commits into
base: master
Choose a base branch
from

Conversation

asymmetric
Copy link
Contributor

@asymmetric asymmetric commented Apr 13, 2020

The previous form matched against any (maxUInt32 & X), including places
where it shouldn't have (e.g. rules for reading from packed storage).

@asymmetric asymmetric requested a review from a team April 13, 2020 13:32
The previous form matched against any (maxUInt32 & X), including places
where it shouldn't have (e.g. rules for reading from packed storage)
@asymmetric asymmetric force-pushed the better-constrain-time branch from f997def to 029c270 Compare April 13, 2020 13:33
Copy link
Contributor

@d-xo d-xo left a comment

Choose a reason for hiding this comment

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

lgtm assuming CI passes. Thx for fixing my bad lemma!!! 🥰✨

src/lemmas.k.md Outdated Show resolved Hide resolved
@asymmetric asymmetric force-pushed the better-constrain-time branch from acbfe86 to 613d6f3 Compare April 13, 2020 14:10
@asymmetric asymmetric force-pushed the better-constrain-time branch from ca26def to b4ccbd1 Compare April 13, 2020 15:03
src/lemmas.k.md Show resolved Hide resolved
K doesn't seem to know that the chop can be removed in this case.
rangeUInt(224, pow224) is false, which means our rule wouldn't have applied.
@asymmetric asymmetric force-pushed the better-constrain-time branch from 6ef4644 to 774d84b Compare April 14, 2020 12:03
@asymmetric asymmetric mentioned this pull request Apr 30, 2020
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants