3 ms·

Your `D(K(..))` notation is better than mine. Email me, and I will send you a gift card. What you do is solve `\exists D: \forall arr: D(K(arr)) = arr` where `

Your `D(K(..))` notation is better than mine. Email me, and I will send you a gift card. 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 http://saurabh-srivastava.com/pubs/pldi11-pins.pdf

westoncb 8y ago
> So you're not explicitly computing `I - K`, but instead letting the constraint solver pick values that satisfy the equation Ah—makes sense. I wonder if attempts at going in the other direction have been made, and initially constraining the structures of the known parts so that you could do something like a subtraction to get the unknown (probably a crazy dead-end idea I realize :). > 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. Interesting. So because we know it's an inversion scenario beforehand we can modify the solver to not be so general, and only bother considering solutions which modify the state in an inverse manner to our original program... Cool. I'll be keeping this at the back of my mind to see if any ideas come up. Thanks and good luck!
- saurabh20n 8y ago
  Look up Nate's work [1], specifically Boomerang [2] that aims for bidirectional programming. Be crazy :) [1] Nate Foster: http://www.cs.cornell.edu/~jnfoster/ http://www.cs.cornell.edu/~jnfoster/ [2] Boomerang http://www.seas.upenn.edu/~harmony/ http://www.seas.upenn.edu/~harmony/

westoncb 8y ago

> So you're not explicitly computing `I - K`, but instead letting the constraint solver pick values that satisfy the equation Ah—makes sense. I wonder if attempts at going in the other direction have been made, and initially constraining the structures of the known parts so that you could do something like a subtraction to get the unknown (probably a crazy dead-end idea I realize :). > 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. Interesting. So because we know it's an inversion scenario beforehand we can modify the solver to not be so general, and only bother considering solutions which modify the state in an inverse manner to our original program... Cool. I'll be keeping this at the back of my mind to see if any ideas come up. Thanks and good luck!

saurabh20n 8y ago
Look up Nate's work [1], specifically Boomerang [2] that aims for bidirectional programming. Be crazy :) [1] Nate Foster: http://www.cs.cornell.edu/~jnfoster/ http://www.cs.cornell.edu/~jnfoster/ [2] Boomerang http://www.seas.upenn.edu/~harmony/ http://www.seas.upenn.edu/~harmony/