Skip to content
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

Approximate rejection sampler examples #9

Closed
wants to merge 61 commits into from
Closed

Approximate rejection sampler examples #9

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
61 commits
Select commit Hold shift + click to select a range
00cf979
approximate bdd rejection sampler wip
markusdemedeiros Nov 6, 2023
9731f56
approximate rejection sampler examples
markusdemedeiros Nov 6, 2023
6980208
plans
markusdemedeiros Nov 8, 2023
9f989fa
clear some admits
markusdemedeiros Nov 13, 2023
df961d2
fix proof
markusdemedeiros Nov 13, 2023
f6383ed
refactor
markusdemedeiros Nov 13, 2023
ee7da29
refactoring
markusdemedeiros Nov 13, 2023
0192a35
eod changes
markusdemedeiros Nov 13, 2023
d0083c2
error_limit lemma
markusdemedeiros Nov 14, 2023
8e238df
sketch a lemma for turning fin series into nat series
markusdemedeiros Nov 15, 2023
0d73f91
sketch incr_N_zero
markusdemedeiros Nov 15, 2023
2cede4a
rewrite lift (fin _ -> fin _) -> (nat -> nat) function (uses proof ir…
markusdemedeiros Nov 15, 2023
f99100f
use the lemmas in the proof, fewer admits
markusdemedeiros Nov 15, 2023
2c89d5c
fix final proof to use posreal
markusdemedeiros Nov 15, 2023
332d222
paste in higherorder
markusdemedeiros Nov 20, 2023
a27aef3
cleanup parts of rand_sampling_scheme_spec
markusdemedeiros Nov 21, 2023
f41b622
finish increment sum lemma
markusdemedeiros Nov 21, 2023
eb94786
fix the spec
markusdemedeiros Nov 22, 2023
ebe7c28
finish sample_err_mean
markusdemedeiros Nov 22, 2023
f67715d
remove extraneous unproven lemmas
markusdemedeiros Nov 22, 2023
a2be816
progress on reindexing lemma
markusdemedeiros Nov 22, 2023
d41e507
reindex_fin_series
markusdemedeiros Nov 22, 2023
82fe4b1
fill in all but one admit
markusdemedeiros Nov 23, 2023
b22d933
start on flip2 sampler
markusdemedeiros Nov 23, 2023
b363fdc
flip2 wip
markusdemedeiros Nov 23, 2023
beb853b
work on flip2
markusdemedeiros Nov 27, 2023
1fc476b
reorganize the file
markusdemedeiros Nov 27, 2023
cc990cd
prove flip amplification
markusdemedeiros Nov 27, 2023
aa71a7e
flip2 sampling spec
markusdemedeiros Nov 27, 2023
efd075e
flip_amplification
markusdemedeiros Nov 27, 2023
9de5b24
tidy
markusdemedeiros Nov 27, 2023
100085f
aggressively higher order spec
markusdemedeiros Nov 28, 2023
c51549c
instantiate higher order spec for rand rejection sampler
markusdemedeiros Nov 29, 2023
7cb8fe4
aggressively higher order flip2
markusdemedeiros Nov 29, 2023
204df0f
fix build
markusdemedeiros Jan 10, 2024
4d988df
move from using app_rel tactics to ub tactics
markusdemedeiros Jan 10, 2024
8296a54
update basic rejection sampler section
markusdemedeiros Jan 10, 2024
3e2be39
close proof of higher order bounded safety
markusdemedeiros Jan 10, 2024
55892c6
prove safety for the unbounded higher-order samplers
markusdemedeiros Jan 10, 2024
89a3d88
higher order rand
markusdemedeiros Jan 10, 2024
f3111c8
higher order flip2
markusdemedeiros Jan 10, 2024
85422b3
work towards resolving the admitted lemmas about fin types
markusdemedeiros Jan 11, 2024
1493c57
implement synchronized planner rule
markusdemedeiros Jan 11, 2024
003ac8b
presampled flip2 example
markusdemedeiros Jan 15, 2024
5d53414
change to block padding lemma
markusdemedeiros Jan 15, 2024
e5fbe8d
Fix compilation
markusdemedeiros Jan 15, 2024
3e7aeeb
incremental higher order spec
markusdemedeiros Jan 17, 2024
4fe694c
value-level assignments for incremental SAT
markusdemedeiros Jan 18, 2024
e5abd50
fix incremental spec proof
markusdemedeiros Jan 19, 2024
070d5b9
sketch wp_resample_amplify
markusdemedeiros Jan 19, 2024
8c61904
progress lemma
markusdemedeiros Jan 22, 2024
ce24259
close holes in resample_amplify
markusdemedeiros Jan 22, 2024
c9728f4
coq-level and value-level evaluator wp's
markusdemedeiros Jan 22, 2024
e68c607
wp_check
markusdemedeiros Jan 22, 2024
22c2bca
wp_sampler_done lemma
markusdemedeiros Jan 22, 2024
ecb0c4f
sketch for instance proof (spec needs to change)
markusdemedeiros Jan 23, 2024
1ee7aea
new incremental spec
markusdemedeiros Jan 24, 2024
b73b6d5
sketch integer_walk
markusdemedeiros Jan 24, 2024
e091621
sketch int walk sampler
markusdemedeiros Jan 24, 2024
fd6e88f
EOD comments
markusdemedeiros Jan 24, 2024
b9d54bf
Merge branch 'logsem:main' into approximate-rejection-sampler-examples
markusdemedeiros Jan 25, 2024
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
Loading
Loading