compiler proof: Fixed the uabsfuns declaration #406
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Cheunglo
force-pushed
the
uabsfuns-decl-fix
branch
2 times, most recently
from
a9e626e
to
c38c5c7
Compare
This commit fixes the declaration of the uabsfuns, i.e. the xi_0 and xi_1 terms in the corres theorems. These are now declared as Isabelle constants, which users can overload later on whilst theorems using these constants will still remain true. One minor fix is fixing the make file for the system-abstract-verif example. It now copies the typing table to a file that Isabelle expects to exist.
This commit contains a general for loop that can be accessed through the
FFI. The core files relating to the refinement proofs are:
* RepeatUpdate.thy: contains the embedding of the for loop in the
update semantics and proofs about preservation, early termination
and invariants.
* RepeatValue.thy: contains the embedding of the for loop in the
value semantics and proofs about preservation
* RepeatCorres.thy: contains the refinement proof between the C and
update semantics for the for loop. Note that this proof is
specific to this example.
* RepeatCorrespondence.thy contains the correspondence and upward
propagation proof for the general for loop.
This commit includes the monomorphisation proof for the general for loop "repeat". The embeddings in the update and value semantics were modified so that this could be proved, and the other proofs were updated to account for these changes.
Changes:
* added some general helper lemmas
* rearranged the layout of some files
* added wrapper theorems about the repeat loop for
preservation, mono-correspondence, and monomorphisation
Two new files were added. These are "UpdateSemHelper.thy" and "ValueSemHelper.thy". These two files contain helper lemmas and definitions that are not specific to repeat. Proofs showing that the update and value semantics are deterministic if the abstract functions are deterministic were added. Proofs showing that evaluation and preservation of abstract functions in the update and value semantics are occurs for the same expressions and arguments for an abstract function environment (xi) if it occurs for a smaller abstract function environment were added. Similarly, proofs for corres and correspondence of abstract functions (for certain cases) were also added.
This commit contains a generalised proof about correspondence between the generated C code for repeat and its update semantics embedding. This commit also reorders and generalised the theorems for less than and determinism on relations.
This commit adds the fixes from upd-abstyping-fix and also adds the abstract typing context to the abstyping and value relation for abstract types. This enables the abstyping and value relation to use the abstyping and value relations of any of its parent locales.
… proofs The first change allows users to pass values and types to the heap relation and value relation generation to either add or ignore those types and values for the generation. Proofs for preservation (update and value semantics), correspondence and upward propagation between the update and value, and monomorphisation for them length, get and put methods for word arrays have been added. Additional proofs about typing, value typing, monomorphisation and correspondence in general were also added.
Cheunglo
force-pushed
the
uabsfuns-decl-fix
branch
from
76ac6ee
to
3d0f3fa
Compare
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This commit fixes the declaration of the uabsfuns, i.e. the xi_0 and
xi_1 terms in the corres theorems. These are now declared as Isabelle
constants, which users can overload later on whilst theorems using these
constants will still remain true.
One minor fix is fixing the make file for the system-abstract-verif
example. It now copies the typing table to a file that Isabelle expects
to exist.