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.

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

Cf div io #609

Merged
merged 117 commits into from Jan 25, 2019

Conversation

Projects
None yet
4 participants
@fogity
Copy link
Contributor

fogity commented Jan 22, 2019

The work on introducing divergence reasoning to cf up to this point, cheat free.
Should work for proving pure divergence, work on divergence with IO still in progress.
Merge suggested by @myreen

myreen and others added some commits Jun 9, 2018

Start sketch of CF for proofs of non-terminating programs
This is based on discussions Johannes and I have had over the last few
days. This commit is only a first sketch -- there are known problems
with the current formulation of the Div case.
Next version of CF for non-terminating programs
Currently, the only thing of interest in the final limit state st' of
the Div (diverge) case is the io_events. This focus on only one
component in the state is (I think) unavoidable because there is no
limit state for the oracle state or reference store.

It is clear that this use of the ffi state requires the io_events list
to be an llist, but there might be problems with the current
definition of the IO (those problems can probably be solved).
Yet another CF setup for non-terminating programs
The previous version had the problem that a "limit state" had to fit
into the state type of the source semantics. A quick experiment where
types where the type of io_events in ffiTheory was changed to io_event
llist showed that representing limit states in the source would be
very messy (e.g. involving changing all compiler IL semantics
functions) and lead to some ugly cases in the source semantics.

This latest attempt (this commit) rephrases the CF setup so that limit
states are only represented in the heap type of CF. This approach
makes the changes local to CF: only the CF setup needs to be able to
represent "limit states".

Context: Johannes and I are trying to setup CF so that diverging
programs are verified w.r.t. a postcondition that talks about a state
that comes at the end of an infinite number of states in the
non-terminating program. In these commit messages, I call these
imaginary final states "limit states".
Add POSTd_def
With Henrik
Change POSTd into regular definition
Add missing type annotation to POSTD
Added automatic rewrites for POSTd/POSTD.
Extended automatic rewrite of POSTv/POSTe/POST to cover Div.

Renamed Qd to Hd as to follow convention.
Merge remote-tracking branch 'origin/cf-ffidiv' into cf-div
Removed POSTD in favour of adding condition to POST

Renamed Hd to Qd to actually keep convention

Updated POST* rewrite rules for all cases
Add POSTve postcondition injection
This is a fairly common pairing
Add inverted postcondition implications for Val and Exn
Apply it to cf definitions, not yet considering divergence cases
Add criteria to prevent false divergence post-conditions.
Might be a start to forumlate such a criteria for IO, or might need to be replaced with something else.
Redefined POST* in terms of POST.
Small impact change only affecting this theory.
Is a bit cleaner, and might allow better rewrites.
Added DivN to res to represent non-termination given a limited clock.
Introduced to help with the central cf-div lemma.

IlmariReissumies and others added some commits Dec 18, 2018

Prove the particular case of app_opapp_intro we need
The more general form would probably come in handy once we extend this
to handle functions with multiple arguments. In the meantime, rather
than go through the pain of working out how to structure the inductive
argument for this kind of reduction, let's move on with our lives.
Make a previously local function local again
No need to use it in POSTd proofs if we improve the automation.
Add io_events_mono to evaluate_minimal_clock and related lemmas.
Move evaluate_set_init_clock to evaluatePropsTheory.
Replace an xlet_auto with a manual xlet
This should be solvable by xlet_auto, but for some reason it appears to not fully specialize the used theorem

@xrchz xrchz added the test failing label Jan 22, 2019

@myreen myreen removed the test failing label Jan 22, 2019

fogity added some commits Jan 23, 2019

Add additional cases to cf tactics postcondition cleanup
This also serve as a better fix for readerProgScript

@xrchz xrchz merged commit 0f7cba8 into master Jan 25, 2019

1 check was pending

cakeml-regression-test regression test in progress
Details

@myreen myreen deleted the cf-div-io branch Jan 25, 2019

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment