bedrock2 stackalloc semanticsuse anybytes which is defined in terms of $@ but the ProgramLogic Ltac for discharging these goals still converts back to array ptsto for compatibility with existing proofs. For new proofs, we'd like to have an option where straightline on stackalloc creates $@ hypotheses and expects the same for deallocation. Supporting this would probably come down to adding an alternative match-goal-with case in dealloc and probably having an alternative straightine_stackalloc that we can use to override the existing one using Ltac redefinitions (::=).
@lukaszobernig or @miriampolzer, this might be a good task to get more experience working with guts of bedrock2. I can also do it myself, sometime.
bedrock2 stackalloc semanticsuse anybytes which is defined in terms of
$@but the ProgramLogic Ltac for discharging these goals still converts back toarray ptstofor compatibility with existing proofs. For new proofs, we'd like to have an option where straightline on stackalloc creates$@hypotheses and expects the same for deallocation. Supporting this would probably come down to adding an alternative match-goal-with case in dealloc and probably having an alternative straightine_stackalloc that we can use to override the existing one using Ltac redefinitions (::=).@lukaszobernig or @miriampolzer, this might be a good task to get more experience working with guts of bedrock2. I can also do it myself, sometime.