Experiment with nonterminating programs - #481

Draft

OwenConoly wants to merge 82 commits into

mit-plv:masterfrom

OwenConoly:nontermination4

Commits on Aug 24, 2025

mls
OwenConoly
committed
6018db5
mor mls
OwenConoly
committed
450128f
prove the eventual_one_printer
OwenConoly
committed
6112e10
mls bug
OwenConoly
committed
5bc378d
flatimp
OwenConoly
committed
04940d2
flattenexpr
OwenConoly
committed
eb49ee6
started fixing quitting semantics
OwenConoly
committed
9ebb60b
still haven't got loop semantics right
OwenConoly
committed
4be8111
maybe fix loop semantics?
OwenConoly
committed
8a3b16b
flatimp compiles
OwenConoly
committed
19db3ef
alomsot finish flattenexpr
OwenConoly
committed
e9968cd
aha
OwenConoly
committed
1f07c11
done flattening, surely
OwenConoly
committed
faa5c37
regalloc too
OwenConoly
committed
ffb4855
start spilling
OwenConoly
committed
a6b1a3b
up to loop case in spilling
OwenConoly
committed
2fa7ecc
loops, leakage, and quitting...
OwenConoly
committed
bca432d
give up on proving the stronger spec for leakage---it is not true.
OwenConoly
committed
740dbfc
basically done with spilling, surely
OwenConoly
committed
fcf6546
finish spilling_correct (it's a bit ugly)
OwenConoly
committed
ad7f470
start proving relations between versions of small-step omnisemantics
OwenConoly
committed
1f8910a
more
OwenConoly
committed
a2357c1
more small-step stuff
OwenConoly
committed
3700339
start FlatToRiscv
OwenConoly
committed
3ead7d2
finish flattoriscv functions (has quitting now)
OwenConoly
committed
1576541
start making functions say things about aeps
OwenConoly
committed
d30ccae
add nontermination stuff to flattoriscv
OwenConoly
committed
e23c256
oops fix spilling
OwenConoly
committed
5542628
lowerpipeline
OwenConoly
committed
1d5d4d9
work on intersection lemma
OwenConoly
committed
f4f06dc
oops let's just do induction on the program
OwenConoly
committed
c31f8c5
aha loop case
OwenConoly
committed
3cac2a1
finish intersection lemma
OwenConoly
committed
bd46f5c
trying again with det_invert
OwenConoly
committed
acca98e
more lemmas to prove?
OwenConoly
committed
68f6076
prove inversion lemma that is maybe not terrible to use
OwenConoly
committed
7638eb4
finish useimmediate
OwenConoly
committed
34fce93
sketch better version of inversion
OwenConoly
committed
a149a50
compiler_correct
OwenConoly
committed
4c418d2
version of compiler_correct useful for nonterminating prorams
OwenConoly
committed
2e80013
start trying to do one_printer example. stuck on MMIO.v.
OwenConoly
committed
b9c18a7
prove better inversion lemma. use it in useimmediate.
OwenConoly
committed
dc2a4ac
remove unneeded junk from useimmediate
OwenConoly
committed
139e7ea
mmio
OwenConoly
committed
6f7141e
start one_printer example
OwenConoly
committed
43483f4
prove low-level spec of one_printer
OwenConoly
committed
24ceffe
think about trace predicates
OwenConoly
committed
8e6fb9b
finite prefixes
OwenConoly
committed
4005b23
thing
OwenConoly
committed
7ada28f
m
OwenConoly
committed
2d20a67
m
OwenConoly
committed
5eb7cfe
progress
OwenConoly
committed
86d3989
interp_aep
OwenConoly
committed
d85975e
not much
OwenConoly
committed
eb75e50
something
OwenConoly
committed
8bb54ae
linterp_iff_linterp_lol
OwenConoly
committed
8a0946c
aep_of_lformula
OwenConoly
committed
1dcd6f8
figure out aep_enough'
OwenConoly
committed
123124c
get stuck because i don't have (sp ex -> OK ex)
OwenConoly
committed
7402583
a bit of progress
OwenConoly
committed
51fbab7
more
OwenConoly
committed
39e388e
qed fail?
OwenConoly
committed
e6459b2
aep_enough'
OwenConoly
committed
302fd83
eh
OwenConoly
committed
9b7e38b
aep_enough
OwenConoly
committed
fb2cf9e
put some stuff together, and sketch a conclusion
OwenConoly
committed
162e5d2
start AEP_A_forall
OwenConoly
committed
a0c7ace
not much
OwenConoly
committed
b9adee9
proof about nonterminating guys
OwenConoly
committed
fa2e94d
sinterp_to_omni_aep
OwenConoly
committed
312465b
oops fixed itX
OwenConoly
committed
26aec8a
progress towards talking about terminating programs? slightly confused
OwenConoly
committed
44a3fc1
make it say stuff about terminating programs too
OwenConoly
committed
3c7ba22
slight prettification etc
OwenConoly
committed
f5c12a9
make things more (explicitly) constructive
OwenConoly
committed
6b288b2
remove duplicate stuff
OwenConoly
committed
3cd60ab
delete more duplicated stuff, and prettify the one printer
OwenConoly
committed
e5054d4
prettify one_printer source
OwenConoly
committed
e76c4f0

Commits on Aug 28, 2025

Commits on Aug 30, 2025

stop doing inversion the dumb way
OwenConoly
committed
3d910d0

Commits on Aug 31, 2025

use stdlib streams
OwenConoly
committed
e5d0456