I was checking for bypr instances in the stdlib, and found a number that are used to discharge judgments of the form for abstract S:
pre = (glob S) = (glob S){m} /\ arg = (skt, ct)
S.decaps
[=] Pr[S.decaps(skt, ct) @ &m : res = kt]
post = res = kt
The full proof pattern here is to use bypr to reduce this down to an equality of probabilities, which is then discharged trivially by byequiv. I feel, somewhat strongly, that this is not an OK amount of gymnastics for something that should be "by semantics of the judgment", and for which, if needed, we can produce the proof tree automatically.
I'd like to discuss what the right way of correcting this is.
We already treat equiv [M.f ~ M.f: ={arg, glob M} ==> ={res, glob M}] as a tautology for abstract M. I want to note that this then places a constraint on the instantiation of M (i.e. that it writes its locals before reading them); treating the phoare one as tautological for abstract S would not place any further constraints on instantiations of abstract modules.
Out of this, I think we should just detect the above (perhaps up to framing and conseq?) and reduce it to true in the same way. Are there obstacles to this?
I was checking for
byprinstances in the stdlib, and found a number that are used to discharge judgments of the form for abstractS:The full proof pattern here is to use
byprto reduce this down to an equality of probabilities, which is then discharged trivially bybyequiv. I feel, somewhat strongly, that this is not an OK amount of gymnastics for something that should be "by semantics of the judgment", and for which, if needed, we can produce the proof tree automatically.I'd like to discuss what the right way of correcting this is.
We already treat
equiv [M.f ~ M.f: ={arg, glob M} ==> ={res, glob M}]as a tautology for abstractM. I want to note that this then places a constraint on the instantiation ofM(i.e. that it writes its locals before reading them); treating thephoareone as tautological for abstractSwould not place any further constraints on instantiations of abstract modules.Out of this, I think we should just detect the above (perhaps up to framing and
conseq?) and reduce it totruein the same way. Are there obstacles to this?