ecancel_assumption failure

[RasmusHoldsbjergCSAU]

I am currently attempting to use Bedrock2 for cryptographic applications that use field arithmetic generated by Fiat Crypto.
I am however having a bit of trouble with the ecancel_assumption tactic.
It is my understanding that the purpose of this tactic is to solve goals like the one below, by recognizing the hypothesis H10 in the context, and instantiating the existential variables as appropriate, but i get a "No applicable tactic" failure when trying to apply the tactic here.
I was hoping that @andres-erbsen, @samuelgruetter or anyone else with insight could comment on this : )

[andres-erbsen]

Yes, this is the intended use case. It looks like H10 has more bignums than the goal, though, so I would expect this goal is not provable. Perhaps you forgot something in a specificaiton that would leave a frame (* ?R) in the goal?

Edit: you could also try to debug this situation as you would if the tactic was broken -- by inlining it. If my guess above is right, this would get you to a goal where you are trying to prove that having bignums at pxr, pxi, pyr, pyi is the same as having no memory, but it's in general what I do if I have an unexplained tactic failure. I recently learned how to make multi-success tactics have nicer error messages so I am hoping I'll get to applying that trick to bedrock2 shortly...

[RasmusHoldsbjergCSAU]

Thanks! Adding the (* ?R) frame to the postcondition in the function specification solved the problem.

I am not entirely sure about the purpose of this R variable though.
As I understand, the separating conjuction, *, takes as arguments predicates on memory, and states that the memory can be parted into two disjoint parts each satisfying one of the predicates.
So shouldn't a goal of the form
Goal: (P1 * P2)%sep m
not from a hypothesis of the form
H: (P1 * P2 * P3)%sep m ?

Do you mean that the goal is not solvable by the ecancel_assumption tactic, or that it is not solvable in general?

In most examples i have seen, this variable, R, is used, but I noticed that it isn't here:
https://github.com/mit-plv/fiat-crypto/blob/master/src/Bedrock/Field/Synthesis/Examples/LadderStep.v#L134

Also, with respect to debugging by inlining the tactics; this was my initial approach, as it often provides useful insight, but in this case i ran into some trouble with not being able to instantiate existential variables with auto generated names, so the rabbit hole got fairly deep.
If you have any suggestions for circumventing this situation that would be very helpful as well : )

[samuelgruetter]

There are two kinds of separation logics: Garbage-collected (also called affine) and malloc/free (also called linear). In malloc/free separation logics (such as bedrock2), you can't just drop sep clauses (that would correspond to a memory leak), so (P1 * P2)%sep m does not follow from (P1 * P2 * P3)%sep m (whereas in garbage-collected separation logics, it does).

My guess is that the absence of a frame R in the ladderstep is just an oversight that has not yet been detected because noone has tried to call the ladderstep function yet.

And yes, the "state of the art" of debugging tactics is to inline them. To debug an ltac invocation foo arg1 arg2, where Ltac foo x y := body, I usually write let x := arg1 in let y := arg2 in copy-pasted-body, and then comment out or modify parts of copy-pasted-body, and continue recursively, until I understand what's going on.