Formally justifying our sets of values abstraction: porting guarantees to concrete instantiation

[catalin-hritcu]

Once we proved a specification for the set of outcomes semantics of a generator, what exactly can we deduce about the concrete semantics?

[catalin-hritcu]

This is probably similar to "Computational Soundness" proofs in cryptographic protocols. There one also abstracts away from things like probabilities and computational complexity, does proofs in an idealized model, while still hoping that the proofs mean something in the more realistic and complex model ... at least under some "realistic assumptions" (which often turn out to be very strong).

[catalin-hritcu]

Maxime thinks this might use ideas from his refinement framework / parametricity.

[zoep]

In the "axiom-free" version we have that

 forall A (g : G A) (x : A),
     semGen g x <-> exists size seed, run g seed size = x.

which I guess is pretty much the connection we need about the set of outcomes and the concrete semantics.

[catalin-hritcu]

This seems good enough for me. Closing this.