Having recently looked at this, the construction is really cool but you don't yet have a solution for the proofs that (a) avoids time correlation between requests on the blinded token vs requests on the unblinded token, or (b) avoids requiring receiver to contact mint, right?

In an ideal world you could take a DLEQ (C'->B', A->G) and convert it (without mint's interaction) into a proof for C->Y instead ... the more naive ways of trying to do that involve making the DLEQ's security broken, I don't think it works. But in principle I think some (rather involved) ZKP, just using the discrete log primitives, *might* be possible. Essentially the sender claiming "Here is C, x, (and Y) and here is a ZKP that: I know a value r such that (C+rA)/(Y + rG) == A/G" without revealing r (all else is known/given to receiver).

Again, I'm not sure but, if it is indeed possible then I think it ticks all the boxes you're looking for.