Int63.eqb_correct doesn't compute

[vblot]

Description of the problem

Computation gets stuck on eqb_correct for native integers. This is a problem in particular when using Int63.cast, which blocks reduction.

Require Import Int63.

Goal match cast 0 0 with
      | Some f => f (fun x => bool) true
      | None => false
     end = true.
vm_compute.
Fail reflexivity.

Indeed, eqb_correct is an axiom, while it had an associated reduction rule in original native-coq.

Coq Version

at least on 8.10.2 and 8.13.2

[JasonGross]

I can think of two ways to resolve this issue.

1. Replace the primitive Boolean equality operator at
   

   coq/theories/Numbers/Cyclic/Int63/PrimInt63.v

   Line 79 in 147f4da

   Primitive eqb := #int63_eq.

   
   with something of type forall x y, option (x = y). It shouldn't be too hard to manufacture the relevant term in primitive land, and then all of the axioms about primitive equality can be wrapped in a version that first asks if they are decidably equal (hence returning a computing proof), and delegates to the axiom only to prove a contradiction
2. Implement something like Request for an extension of [Axiom] to something like Agda's primTrustMe, for judgmental reduction #3927 (I thought there was a PR to do this but I can't find it) Edit: I was thinking of User-defined rewrite rules ceps#50

[silene]

Please let us not replace a trivial opcode with a costly memory-allocating one. That said, having an additional opcode of type forall x y:int, option (x = y) makes sense to me, assuming it is sufficient.

[SkySkimmer]

The reduction could be provided by going through a sprop equality (using the uip flag).

[silene]

The reduction could be provided by going through a sprop equality (using the uip flag).

That is elegant. But wouldn't that still block due to the use of vm_compute in the first place?

[ppedrot]

FTR I've been advocating for replacing all primitive Prop-living axioms by an SProp variant, so that we recover canonicity in a systematic way.

[SkySkimmer]

That is elegant. But wouldn't that still block due to the use of vm_compute in the first place?

Yes

[vblot]

Sorry if this is a naive question, but why should we use uip or go to sprop ? I think reducing eqb_correct i i (eq_refl true) to eq_refl i as was done in original native coq is fine: it only chooses one equality proof, eq_refl, but doesn't prevent the existence of other equality proofs on int, and as such remains agnostic wrt uip/k.

[ppedrot]

@vblot this would need adding new primitive reductions to the various machines, including potential opcodes to the VM.

[vblot]

Yes, that is what I had in mind. Is this complicated?

[ppedrot]

It's fragile and ad-hoc, and increases the TCB.

[vblot]

I see. OTOH there are already many operations on int so one more seems harmless to me, but I understand the kernel is not something you want to change every day.

[silene]

it only chooses one equality proof, eq_refl, but doesn't prevent the existence of other equality proofs on int

Just to be clear, there is no other equality proof. And in the forsaken times of retro-knowledge, you could even prove it in Coq. Just because retro-knowledge was removed from Coq does not mean that int suddenly became some kind of magical type with several equality proofs. So, the use of SProp here makes a lot of sense. (Too bad it does not work. We really need to find some solution to this issue.)

[vblot]

Just to be clear, there is no other equality proof.

I think it depends on the semantics of "equality proof". If by that you mean a term (without axioms) of type equality then I agree, but if I'm not mistaken, when you do not have uip you have a sound system with:

Axiom e : 0=0.
Axiom e <> eq_refl.

while with uip you can prove False from the axioms above. Or am I missing something?

[ppedrot]

1. Decidable types have UIP.
2. What @silene means is that there is only one proof of equality in the empty context.

[silene]

Actually, I meant your point 1. At the time of retro-knowledge, int had a concrete definition, and thus UIP was provable. And nowadays, even if the type has become abstract, its values still deterministically fit onto a 63-bit vector, so nothing has changed from a theoretical point of view.

[vblot]

1. Decidable types have UIP.

Thanks! I had forgotten about that one... But then it seems counter-intuitive to require the uip flag, since int is decidable.

[ppedrot]

OK, I am being confusing, sorry about that. There are two meanings for UIP over a type A,

• first the fact that given any equality type (in Prop, in Type, in SProp, whatever) you can prove forall (x y : A) (p q : x = y), p = q
• second the fact that you can eliminate the SProp equality into it, which makes it into a strict set.

Colloquially we also refer as Definitional UIP the kernel flag that unconditionally allows the second thing, making the global assumption that all types are strict sets.

Third, In order to prove the first point you need to be able to eliminate from the considered equality. So, in practice that means that there is a loop in the reasoning that you must untie by explicitly allowing Definitional UIP for this type, otherwise you won't be able to do anything with the axiomatic SProp equality. So you have to be careful about how you express the boolean equality test and the fact it reflects the actual propositional equality of the theory.

[JasonGross]

having an additional opcode of type forall x y:int, option (x = y) makes sense to me, assuming it is sufficient.

This should be sufficient for defining the wrappers, yes.

[vblot]

OK, I am being confusing, sorry about that. There are two meanings for UIP over a type A,

* first the fact that given any equality type (in Prop, in Type, in SProp, whatever) you can prove `forall (x y : A) (p q : x = y), p = q`

* second the fact that you can eliminate the SProp equality into it, which makes it into a strict set.

Colloquially we also refer as Definitional UIP the kernel flag that unconditionally allows the second thing, making the global assumption that all types are strict sets.

Third, In order to prove the first point you need to be able to eliminate from the considered equality. So, in practice that means that there is a loop in the reasoning that you must untie by explicitly allowing Definitional UIP for this type, otherwise you won't be able to do anything with the axiomatic SProp equality. So you have to be careful about how you express the boolean equality test and the fact it reflects the actual propositional equality of the theory.

Thanks for the explanation, I think I'll have to read stuff about this.

[vblot]

having an additional opcode of type forall x y:int, option (x = y) makes sense to me, assuming it is sufficient.

This should be sufficient for defining the wrappers, yes.

And this would reduce to Some eq_refl when applied twice to the same int? If so then I think it would solve my use case, yes.

[JasonGross]

having an additional opcode of type forall x y:int, option (x = y) makes sense to me, assuming it is sufficient.

This should be sufficient for defining the wrappers, yes.

And this would reduce to Some eq_refl when applied twice to the same int? If so then I think it would solve my use case, yes.

Yes, and it would reduce to None when applied to two concrete ints that are not the same.

[vblot]

Please let us not replace a trivial opcode with a costly memory-allocating one. That said, having an additional opcode of type forall x y:int, option (x = y) makes sense to me, assuming it is sufficient.

One option would be to actually replace the current primitive eqb with an operator eq_option of type forall x y:int, option (x = y), and define eqb by fun x y => match eq_option x y with Some _ => true | None => false end. The related axiom would be forall x, eq_option x x = Some eq_refl, we could then prove eqb_correct by computation and prove eqb_refl using this new axiom. This has the advantage of not adding a new opcode and not increasing the TCB. However I don't know if there are performance issues.

[silene]

Please let us not replace a trivial opcode with a costly memory-allocating one.

One option would be to actually replace the current primitive eqb with an operator eq_option

That is exactly the option I am vetoing. Opcode eqb is allocation-free (assuming the inputs are closed terms). Opcode eq_option cannot be allocation-free. So, if you define eqb using eq_option, eqb is no longer allocation-free.

[vblot]

Please let us not replace a trivial opcode with a costly memory-allocating one.

One option would be to actually replace the current primitive eqb with an operator eq_option

That is exactly the option I am vetoing. Opcode eqb is allocation-free (assuming the inputs are closed terms). Opcode eq_option cannot be allocation-free. So, if you define eqb using eq_option, eqb is no longer allocation-free.

Right, so there is indeed a performance issue. Sorry for my misunderstanding and thanks for the explanation.

[SkySkimmer]

Opcode eq_option cannot be allocation-free

If I understand how the VM works correctly, we could allocate a global Some eq_refl since the non-constant subterms are parameters which don't appear in the VM representation, would that work?

[ppedrot]

Actually, we don't have to introduce an opcode for this. We could write an untyped program in the VM using the low-level equality and returning refl when the two arguments coincide. It's safer to write code in lambda than in C...

[silene]

It's safer to write code in lambda than in C...

I dispute this statement. When I had to debug a memory corruption due to cofixpoints in the VM, I would have much preferred if the code had been written in C. (As the idiom goes, writing code is the easy part, debugging it is the hard part.)

we could allocate a global Some eq_refl

That would work, yes. Obviously, we would still have to pay for destructuring this value (PUSHFIELDS and the like), but it would at least avoid a memory allocation.

[ppedrot]

When I had to debug a memory corruption due to cofixpoints in the VM

I don't remember what caused this problem, but cofixpoints rely on mutable memory which is very hard to get right. Here, I simply propose to write the lambda term fun x y => if uint32_eq x y then mkblock (0, [0]) else 0 or something like that, and let the VM compiler do the job for us.

[ppedrot]

Also, even if we add a gazillion of opcodes to the VM to handle all the specification primitives, it's not going to solve the canonicity issue for the other reductions, and we'll have to do something there as well. I believe that the SProp solution is cleaner conceptually, but an alternative in this precise case would simply be to allow to define a priori untyped terms for CIC definitions. Indeed, there is a clear program that does what we want, which is the Gallina equivalent of the lambda program above. If you can do this you get everything for free, including Cclosure, VM reduction, cbv, cbn, etc.

[silene]

there is a clear program that does what we want, which is the Gallina equivalent of the lambda program above.

This is exactly what I was about to write. I wonder what it would cost to be able to write something like Axiom Definition eqb_correct : ... := ... (with Axiom meaning that the definition does not go through the typechecker).

[ppedrot]

@silene In any case I don't think it should be exposed to the user, at least not in the Gallina syntax because everything goes through the pretyper, and only typed terms make sense. Also, you have to be careful with these special axioms, because you don't want the untyped definition to unfold unconditionally otherwise you'll break SR.

[silene]

you don't want the untyped definition to unfold unconditionally otherwise you'll break SR.

That is a good point. And it also means that the lambda expression has to be much more complicated than just fun x y => if uint32_eq x y then mkblock (0, [0]) else 0. Otherwise it would end up being unfolded in presence of accumulators.

[eponier]

I also encountered this limitation while wanting to perform a cast on primitive integers.

[eponier]

Hello, I am still interested in having an eqb_correct that computes. Has anything changed since last year's discussions that would allow to implement the feature in a nice way?

[eponier]

Hello, two years later, I am still interesting in having this. Any news?