Primitive integers #6914
Primitive integers #6914
Conversation
You could add a commit (to this PR) reflecting this in the dates of his contributions in |
96b13f3 to
5472192
Compare
|
If you want a review in a reasonable time, I think you should split the set of changed files and ask many people (also the competence needed are quite different here and there) |
What do you mean by that? There's no way I can make the changes independent in general, so I'm not sure I get the point. |
|
This is likely the most naïve question on earth by why does the kernel needs to be modified? I would expect that having fast integers at the VM level should suffice for most applications [with a binary representation at the kernel level of course]. |
I explained that in the various talks I gave on the topic, including during the WG. Maybe you can have a look at the video (although I thought you were attending, but I'm not 100% sure). |
The short answer is that it doesn't, in many cases. You can read the corresponding part of my thesis to see citations of work using primitive integers, concretely. |
|
Yeah I know it was explained in the WG talk, but unfortunately I forgot :S IMHO a small summary of the motivations [in the now extremely terse commit logs] would help preserving this information to future diggers of the codebase. In particular as other systems seems to be pursuing the "fast VM" path. |
Ok, will try to improve the messages once the branch stabilizes. |
e214ae4 to
7e87fa3
Compare
|
This is a bit painful to review, since the addition of the
|
Sorry about that, I tried to do the best I could, initially even the patches adding I'll try to answer / take into account your remarks after figuring out other problems (I don't know why @bgregoir added the dedicated opcodes you mentioned), but I'm not sure what you mean by:
|
Why do we need it? Why is it impossible to write it in Coq? |
I think it is for efficiency. If you define it in Coq, you would need to iterate on a type that looks like binary integers I guess, so you'd lose a lot of the benefits. Do you see another way? |
|
I looked more into the remaining problems and missing bits, and it seems pretty clear that this is not going to be ready by Thursday, so let's postpone to 8.9. But thanks to all for the constructive feedback! I still hope to make quick progress on this given the maintenance cost. |
There was a problem hiding this comment.
I've rebased maximedenes#65 on top of the coqlib changes. Feel free to merge it into this, or to ask me to resubmit it as a PR to Coq after this is merged.
Changes in Ring31.v/Cyclic31. are necessary only if there are custom notations for 0 and 1.
I am baffled by the failure of CompCert, given that it does not show up for me locally, and that maximedenes#67 builds fine for me....
I would prefer to see maximedenes#67 and maximedenes#65 merged before this, but I also don't want to keep getting in the way of this PR being merged.
test-suite/output/sint63Notation.v
Outdated
| (((2 ^ (bw - 1) + v) mod (2 ^ bw)) - 2 ^ (bw - 1))%Z. | ||
|
|
||
| Definition sto_Z (v : sint) := as_signed 31 (to_Z (unwraps v)). | ||
| Unset Printing Records. (* not sure if this is needed; it's here just to be safe *) |
There was a problem hiding this comment.
This should not be needed, and I'd rather we test that it is not needed.
f0b47fd to
3be4238
Compare
|
I’ve just incorporated the two changes suggested by Jason. CompCert needed both. Thanks. |
This was a noop and will soon be an error (until `Inductive` properly supports locality attributes). See rocq-prover/rocq#6914
3be4238 to
084e9d0
Compare
| @@ -320,3 +321,6 @@ val entry_has_ident : notation_entry_level -> bool | |||
| (** Rem: printing rules for primitive token are canonical *) | |||
|
|
|||
| val with_notation_protection : ('a -> 'b) -> 'a -> 'b | |||
|
|
|||
| (** Conversion from bigint to int63 *) | |||
| val int63_of_pos_bigint : Bigint.bigint -> Uint63.t | |||
There was a problem hiding this comment.
Perhaps this belongs in the Uint63 module instead? (Unless we want to keep it outside the kernel.)
There was a problem hiding this comment.
I think there are no bigints in the kernel.
|
What is the documentation CI failure due to? |
084e9d0 to
807d210
Compare
|
@ppedrot No clue. But restarting the pipeline made the problem vanish. We still have to address Érik’s comment. |
This work makes it possible to take advantage of a compact representation for integers in the entire system, as opposed to only in some reduction machines. It is useful for heavily computational applications, where even constructing terms is not possible without such a representation. Concretely, it replaces part of the retroknowledge machinery with a primitive construction for integers in terms, and introduces a kind of FFI which maps constants to operators (on integers). Properties of these operators are expressed as explicit axioms, whereas they were hidden in the retroknowledge-based approach. This has been presented at the Coq workshop and some Coq Working Groups, and has been used by various groups for STM trace checking, computational analysis, etc. Contributions by Guillaume Bertholon and Pierre Roux <Pierre.Roux@onera.fr> Co-authored-by: Benjamin Grégoire <Benjamin.Gregoire@inria.fr> Co-authored-by: Vincent Laporte <Vincent.Laporte@fondation-inria.fr>
c226c52 to
191e253
Compare
|
@ppedrot This is now ready. |
|
Will merge when the CI agrees. |
|
CI agrees!! |
Ack-by: JasonGross Ack-by: SkySkimmer Ack-by: ejgallego Ack-by: gares Ack-by: maximedenes Ack-by: ppedrot
|
Thanks! |
|
Time to do vectors now ;-) |
|
Thanks! |
|
Thanks!
Would be great indeed. We are also still working on floats with Érik. |
|
It should be said that many plugins weren't properly ported to this PR as warning 8 is not fatal by default. |
This patch adds support for primitive integers. It can be seen as an evolution of the existing "retroknowledge" machinery, extending the benefits of compact representations of integers to the entire system (as opposed to only the VM and the native compiler). Useful for many applications around certified computations.
The main changes are:
Intconstruct toconstrand other term representationsStill TODO:
theories)Depends on
#6906#8773 [merged].A lot of this code is from @bgregoir.