Skip to content

pseudo random number generator effect #6

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
hehelego wants to merge 21 commits into
base: main
Choose a base branch
from
Open

pseudo random number generator effect #6

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
21 commits
Select commit Hold shift + click to select a range
e27c687
pseudo random number generator effect
hehelego Mar 30, 2026
107d9b7
update `_CoqProject` to include the PRNG effect reifier and the PRNG-…
hehelego Mar 30, 2026
a7612d6
fix PRNG lang evaluation order
hehelego Apr 2, 2026
1e29f6d
fix add back the missing head reduction for nat op expressions
hehelego Apr 2, 2026
cf94b0f
PRNG gitree combinators with continunation
hehelego Apr 3, 2026
4d898cb
fix PRNG SEED unfold tick counting
hehelego Apr 4, 2026
438b309
WIP: denotational interpretation of PRNG lang
hehelego Apr 2, 2026
8236621
GIT combinators for PRNG-SEED operator
hehelego Apr 4, 2026
d7b7093
Revert "fix PRNG SEED unfold tick counting"
hehelego Apr 4, 2026
fbbd2ef
fix PRNG-lang interpretation and soundness proof
hehelego Apr 4, 2026
52b9d2e
fix forbid the creation of PRNG location statically
hehelego Apr 5, 2026
f999caa
WIP: unary logical relation for safety and adeqaucy for PRNG lang
hehelego Apr 5, 2026
5ae59ad
make prng location value relation persistent
hehelego Apr 6, 2026
9bd28cd
prevent delete PRNG location as it is generally unsafe
hehelego Apr 6, 2026
13e1f0a
new ghost theory and Hoare triples for PRNG effects (deletion is not …
hehelego Apr 7, 2026
1e7ef20
fundamental lemma for PRNG lang logical relation
hehelego Apr 7, 2026
ce149c9
WIP: PRNG ghost theory
hehelego Apr 7, 2026
3bca8ad
finish PRNG ghost theory
hehelego Apr 9, 2026
c44c6cf
complete the adequacy and safety proofs for the PRNG lang
hehelego Apr 10, 2026
a3156eb
add an example GIT program with PRNG and its safety proof
hehelego Apr 11, 2026
c9a412d
PRNG lang gitree denotational semantics adequacy with respect to the …
hehelego Apr 14, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
8 changes: 8 additions & 0 deletions _CoqProject
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -39,6 +39,7 @@ theories/effects/exceptions.v
theories/effects/delim.v
theories/effects/fork.v
theories/effects/coroutines.v
theories/effects/prng.v

theories/lib/pairs.v
theories/lib/sums.v
Expand Down Expand Up @@ -87,6 +88,13 @@ theories/examples/heap_lang/notation.v
theories/examples/heap_lang/pretty.v
theories/examples/heap_lang/tactics.v

theories/examples/prng_lang/prng_seed_combinator.v
theories/examples/prng_lang/prng_examples.v
theories/examples/prng_lang/lang.v
theories/examples/prng_lang/interp.v
theories/examples/prng_lang/logpred.v
theories/examples/prng_lang/logrel.v

theories/utils/finite_sets.v
theories/utils/clwp.v
theories/utils/wbwp.v
Expand Down
Loading