barrett quotient error #343
Conversation
|
Seems to not build with Coq master... |
jadephilipoom
force-pushed
the
barrett_error
branch
from
5cadf19
to
adf8863
Compare
#345 . The "insight" was " |
There was a problem hiding this comment.
Nice!
Alas, it still does not build on master. But if you merge #345 (which does build on master), then the proofs here will also get shorter. Other than that, LGTM.
|
That's weird--it looks like the build failed, even though the same build succeeded on #345. Error is:
...which suggests to me that perhaps this is some issue with the build rather than the code? There's no difference between the code at those two commits. |
|
Adding a comment apparently "fixed" the build. We may want to investigate that, but I'm not really sure where to start and am pretty confident it has little to do with the code in this PR, so I'll merge it. |
|
The issue is definitely something to do with how we're caching vo files (which we do so that we can build more of the project than 1 hour's worth). The error message is because the version of Coq master that got installed here was different from the version of master used to build the cached .vo. I suspect that different PRs building at the same time interfere with each other's build caches, or (or maybe and) the daily-master build on launchpad got updated in the middle of the build. (Except I already restarted the entire build once, and that didn't fix it, but there was another build still going at the same time.) |
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])])])
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])])])
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])])])
The estimated quotient in Barrett reduction (
q, here) is known to have an error of at most 2--that is, using the variable names in theGeneralized.vfile,q = a / n - eand0 <= e <= 2.However, it turns out that for primes that fit a certain condition (see
n_goodin this PR), we can prove0 <= e <= 1, which lets us skip a modular reduction.@JasonGross These proofs are significantly messier than the ones you wrote in
Generalized--if you have tips for better utilizing the automation I'd appreciate it.