pseudo random number generator effect - #6

Open

hehelego wants to merge 22 commits into

logsem:mainfrom

Commits on Apr 2, 2026

Commits on Apr 3, 2026

PRNG gitree combinators with continunation
hehelego
committed
cf94b0f

Commits on Apr 4, 2026

Commits on Apr 5, 2026

fix forbid the creation of PRNG location statically
hehelego
committed
52b9d2e
WIP: unary logical relation for safety and adeqaucy for PRNG lang
hehelego
committed
f999caa

Commits on Apr 6, 2026

make prng location value relation persistent
hehelego
committed
5ae59ad
prevent delete PRNG location as it is generally unsafe
hehelego
committed
9bd28cd

Commits on Apr 7, 2026

new ghost theory and Hoare triples for PRNG effects (deletion is not allowed)
hehelego
committed
13e1f0a
fundamental lemma for PRNG lang logical relation
hehelego
committed
1e7ef20
WIP: PRNG ghost theory
hehelego
committed
ce149c9

Commits on Apr 9, 2026

finish PRNG ghost theory
hehelego
committed
3bca8ad

Commits on Apr 10, 2026

complete the adequacy and safety proofs for the PRNG lang
hehelego
committed
c44c6cf

Commits on Apr 11, 2026

add an example GIT program with PRNG and its safety proof
hehelego
committed
a3156eb

Commits on Apr 17, 2026

PRNG lang gitree denotational semantics adequacy with respect to the operational semantics
hehelego
committed
c9a412d

Commits on May 1, 2026

parameterized over a PRNG typeclass (default seed, state update, read out, and seeding)
hehelego
committed
df2994e