What you do is solve `\exists D: \forall arr: D(K(arr)) = arr` where `arr` is an arbitrary length array/bitstream. See paper [1]. There is also really old code you can browse at the bottom of my personal page linked in profile (doesn't compile anymore coz of deprecated dependencies.)
The arithmetic analogy break down when solving. So you're not explicitly computing `I - K`, but instead letting the constraint solver pick values that satisfy the equation (hence SMT solving.) Also, you are absolutely right that there is no reason to have their structure be related to identity: But, the "damage" done by `K` is encoded in the state at the interface to `D` and `D` better undo that state to get to identity, which is what the solver would exploit.
[1] Path-based Inductive Synthesis for Program Inversion http://saurabh-srivastava.com/pubs/pldi11-pins.pdf