pseudo random number generator effect

[hehelego]

Summary:

• a PRNG effect (LCG with a set of fixed parameters) effects/prng.v
• example programs and proofs with the PRNG effect: examples/prng_lang/prng_examples.v
• a programming language with PRNG effect: examples/prng_lang/lang.v
• interpretation of PRNG language programs in guarded interaction trees: examples/prng_lang/interp.v and examples/prng_lang/prng_seed_combinator.v
• soundness of the interpretation with respect to the operational semantics: examples/prng_lang/interp.v
• safety of the GItree interpretation of a well-typed PRNG language program: examples/prng_lang/logpred.v
• adequacy of the GItrees interpretation with respect to the operational semantics: examples/prng_lang/logrel.v

Work in progress:

• documentation for the new effect
• interpretation and safety of the combination of PRNG+IO tape

Maybe out of scope:

• a language using PRNG + IO tape. (difficulties in state projection).
• take an arbitrary guarded interaction tree as the state update function on PRNG state creation.