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

Sampler examples refactor #14

Merged
merged 64 commits into from
Jan 25, 2024
Merged

Sampler examples refactor #14

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
64 commits
Select commit Hold shift + click to select a range
a7541a0
approximate bdd rejection sampler wip
markusdemedeiros Nov 6, 2023
5fd3771
approximate rejection sampler examples
markusdemedeiros Nov 6, 2023
d959a68
plans
markusdemedeiros Nov 8, 2023
8eb2ac9
clear some admits
markusdemedeiros Nov 13, 2023
62d1fa1
fix proof
markusdemedeiros Nov 13, 2023
6996448
refactor
markusdemedeiros Nov 13, 2023
e96694e
refactoring
markusdemedeiros Nov 13, 2023
642e264
eod changes
markusdemedeiros Nov 13, 2023
df417bc
error_limit lemma
markusdemedeiros Nov 14, 2023
b86b7e8
sketch a lemma for turning fin series into nat series
markusdemedeiros Nov 15, 2023
defb813
sketch incr_N_zero
markusdemedeiros Nov 15, 2023
0684b35
rewrite lift (fin _ -> fin _) -> (nat -> nat) function (uses proof ir…
markusdemedeiros Nov 15, 2023
8e2287b
use the lemmas in the proof, fewer admits
markusdemedeiros Nov 15, 2023
714c06d
fix final proof to use posreal
markusdemedeiros Nov 15, 2023
4063e2a
paste in higherorder
markusdemedeiros Nov 20, 2023
ce3bca8
cleanup parts of rand_sampling_scheme_spec
markusdemedeiros Nov 21, 2023
5d5c1d2
finish increment sum lemma
markusdemedeiros Nov 21, 2023
85c28df
fix the spec
markusdemedeiros Nov 22, 2023
2536c84
finish sample_err_mean
markusdemedeiros Nov 22, 2023
3eb2aba
remove extraneous unproven lemmas
markusdemedeiros Nov 22, 2023
4ad0912
progress on reindexing lemma
markusdemedeiros Nov 22, 2023
b00be19
reindex_fin_series
markusdemedeiros Nov 22, 2023
c00f61b
fill in all but one admit
markusdemedeiros Nov 23, 2023
8ec0cc0
start on flip2 sampler
markusdemedeiros Nov 23, 2023
0cb872f
flip2 wip
markusdemedeiros Nov 23, 2023
37b3f40
work on flip2
markusdemedeiros Nov 27, 2023
0424d85
reorganize the file
markusdemedeiros Nov 27, 2023
0ee2775
prove flip amplification
markusdemedeiros Nov 27, 2023
3b85e5e
flip2 sampling spec
markusdemedeiros Nov 27, 2023
b808925
flip_amplification
markusdemedeiros Nov 27, 2023
3f35ab6
tidy
markusdemedeiros Nov 27, 2023
3da235a
aggressively higher order spec
markusdemedeiros Nov 28, 2023
2913d0f
instantiate higher order spec for rand rejection sampler
markusdemedeiros Nov 29, 2023
ff146ef
aggressively higher order flip2
markusdemedeiros Nov 29, 2023
1248444
fix build
markusdemedeiros Jan 10, 2024
a1096dd
move from using app_rel tactics to ub tactics
markusdemedeiros Jan 10, 2024
d4d7ae9
update basic rejection sampler section
markusdemedeiros Jan 10, 2024
4272245
close proof of higher order bounded safety
markusdemedeiros Jan 10, 2024
fefe06c
prove safety for the unbounded higher-order samplers
markusdemedeiros Jan 10, 2024
ab90693
higher order rand
markusdemedeiros Jan 10, 2024
2107f0f
higher order flip2
markusdemedeiros Jan 10, 2024
c7ac62b
work towards resolving the admitted lemmas about fin types
markusdemedeiros Jan 11, 2024
f3ff80a
implement synchronized planner rule
markusdemedeiros Jan 11, 2024
1b25e9a
presampled flip2 example
markusdemedeiros Jan 15, 2024
53ce2c4
change to block padding lemma
markusdemedeiros Jan 15, 2024
69fab31
Fix compilation
markusdemedeiros Jan 15, 2024
24f1293
incremental higher order spec
markusdemedeiros Jan 17, 2024
b576812
value-level assignments for incremental SAT
markusdemedeiros Jan 18, 2024
0b7c394
fix incremental spec proof
markusdemedeiros Jan 19, 2024
fb7f755
sketch wp_resample_amplify
markusdemedeiros Jan 19, 2024
b0a9af2
progress lemma
markusdemedeiros Jan 22, 2024
2a163b2
close holes in resample_amplify
markusdemedeiros Jan 22, 2024
8b92e9c
coq-level and value-level evaluator wp's
markusdemedeiros Jan 22, 2024
f2cad5c
wp_check
markusdemedeiros Jan 22, 2024
b55e0c7
wp_sampler_done lemma
markusdemedeiros Jan 22, 2024
a394c5c
sketch for instance proof (spec needs to change)
markusdemedeiros Jan 23, 2024
16b3dd6
new incremental spec
markusdemedeiros Jan 24, 2024
d62c6dc
sketch integer_walk
markusdemedeiros Jan 24, 2024
d8ff25e
sketch int walk sampler
markusdemedeiros Jan 24, 2024
172591e
EOD comments
markusdemedeiros Jan 24, 2024
8afc316
re organize
markusdemedeiros Jan 25, 2024
378467b
nit
markusdemedeiros Jan 25, 2024
7ba73ae
CI nit
markusdemedeiros Jan 25, 2024
ed9d36e
CI nit
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