Coding the universe into a real over better core models

Question

One of the most incredible results in modern set theory, due to Jensen, is that given any model of $\sf ZFC$, there is a class forcing which adds a real number $r$ and in the extension $V=L[r]$. Moreover, if we assume some basic things like $\sf GCH$, then cardinals are not collapsed, so in particular things like inaccessible cardinals are preserved.

So in Jensen's result the "coding model" is $L$. But $L[x]$ is somewhat of a dull model. It doesn't have any sharps, measurable cardinals, or larger cardinals. Even those with reasonably canonical inner models.

Question. Given any reasonably canonical core model $K$, can we code the universe into a real over $K$ while preserving large cardinals that are captured by $K$?

In other words, can we code the universe into a real while preserving measurable cardinals? Can we code the universe into a real while preserving strong, Woodin, etc.?

And the obvious follow-up question, what is the bare minimum needed from an inner model $M$ to be a coding model?

Answer 1

For measurable cardinals, the answer is yes and is due to Sy Friedman. See Coding Over a Measurable Cardinal.

There is some difficulty to extend the result to the context of Woodin cardinals, see Genericiy and large cardinals.

For strong cardinals, this is open, though for some simple sets, say the collection of Prikry sequences for the Prikry product, the answer is yes, see Killing the GCH everywhere with a single real.

See also Coding over core models