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

Minor pipeline adjustments #328

Merged
merged 3 commits into from Mar 21, 2018
Merged

Minor pipeline adjustments #328

merged 3 commits into from Mar 21, 2018

Conversation

JasonGross
Copy link
Collaborator

No description provided.

@JasonGross
Let-bind place
44441f3 
This allows vm_compute to run in 300 seconds on the from_associational
pipeline.
@JasonGross
Don't inline var nodes on the first pass through partial evaluation
facb2c2
@JasonGross JasonGross added this to To Do in Pipeline without CPS via automation Mar 21, 2018
@andres-erbsen
Copy link
Contributor

These changes look reasonable to my limited understanding. If you think this is the best place to continue on, merge away.

andres-erbsen
andres-erbsen reviewed Mar 21, 2018
View reviewed changes
src/Experiments/SimplyTypedArithmetic.v
expr_let v13 := ((uint64)((uint64)(v10) +₆₄ (uint64)(v3)) & 2251799813685247) in
(uint64)(v11) :: (uint64)(v13) :: (uint64)(v12) +₆₄ (uint64)(v5) :: (uint64)(v7) :: (uint64)(v9) :: [])%expr
: Expr (type.list (type.type_primitive type.Z) * type.list (type.type_primitive type.Z) -> type.list (type.type_primitive type.Z))
(*base_51_carry_mul =
Copy link
Contributor

Choose a reason for hiding this comment

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

is this change an intended consequence of this PR? I don't mind (no-brainer used-once fixes it), just curious.

Copy link
Collaborator Author

Choose a reason for hiding this comment

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

It's a side-effect of let-binding place. If we don't let-bind place, then it goes back to what it was.

@JasonGross
Copy link
Collaborator Author

For future reference, timing statistics on the bounds pipeline (post-caching) on radd, for 2^127-1, n=3, wordsize=64:

  • without dlet-binding place, lazy takes 0.074 secs, vm_compute takes 0.625 secs, and cbv takes 16.443 secs
  • with dlet-binding place, lazy takes 0.093 secs, vm_compute takes 0.032 secs, and cbv takes 0.423 secs

@JasonGross JasonGross merged commit e865bf2 into mit-plv:master Mar 21, 2018
Pipeline without CPS automation moved this from To Do to Done Mar 21, 2018
@JasonGross JasonGross deleted the minor-pipeline-adjustments branch March 21, 2018 23:51
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, [mit-plv#57, mit-plv#96])
index 0: mit-plv#345 != mit-plv#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, [mit-plv#57, mit-plv#96])
index 0: mit-plv#345 != mit-plv#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

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

Assignees
No one assigned
Labels
None yet
Projects
No open projects
Pipeline without CPS
  
Done
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
2 participants
@JasonGross @andres-erbsen