diff options
author | Yann Herklotz <git@yannherklotz.com> | 2023-05-18 23:22:32 +0100 |
---|---|---|
committer | Yann Herklotz <git@yannherklotz.com> | 2023-05-18 23:22:32 +0100 |
commit | bc2c535af4288e06f285658ef2844aa45da9b302 (patch) | |
tree | 9e373cce6014b6d2b268c2aa9c8aceacb1c2156a /doc | |
parent | 9403299d1a481ea4422524b6caa0d78e4c20fbaf (diff) | |
download | vericert-bc2c535af4288e06f285658ef2844aa45da9b302.tar.gz vericert-bc2c535af4288e06f285658ef2844aa45da9b302.zip |
Add new proofs about semantic identity
Diffstat (limited to 'doc')
-rw-r--r-- | doc/documentation.org | 41 |
1 files changed, 41 insertions, 0 deletions
diff --git a/doc/documentation.org b/doc/documentation.org index 85bc8fd..0087c4a 100644 --- a/doc/documentation.org +++ b/doc/documentation.org @@ -189,6 +189,47 @@ If-conversion is an optimisation which can turn code with simple control flow in Functions are currently only inlined in Vericert, however, we are working on a proper interface to integrate function calls into the hardware. +* Scheduling proof + +** Semantic identity properties + +This section corresponds to the proofs found in =src/hls/AbstrSemIdent.v=. + +*** =sem_merge_list= +:PROPERTIES: +:ID: f307d227-d0e9-49a0-823f-2d7e0db76972 +:END: + +This lemma proves that given a forest =f= that executes from an initial context +=ctx= to a state composed of =rs=, =ps= and =m=, that the evaluation of the +merged arguments from the forest is equivalent to retrieving the arguments +dynamically from the new state of the registers. This proves the correctness of +the combination of =merge= and =list_translation= to encode the list of +arguments. + +One interesting note about this lemma is that it passes the latest state of the +predicates from =f= into the function, i.e. =forest_preds f=. This allows one +to prove the theorem, however, using it later on is more problematic, as one +cannot easily reuse it in the middle of an induction. Instead, one would have +to prove that the future changes to the forest will not change the result of the +current evaluation of the register arguments. + +It does make sense that this has to be proven somewhere, however, it's not clear +if this results in the simplest proofs. However, one benefit is that this +function already has to be used for the forward translation proof, so it can +easily be reused for the backward execution proof. + +** Backward proof + +This corresponds to the proof found in =src/hls/GiblePargenproofBackward.v=. + +*** =abstr_seq_reverse_correct_fold= +:PROPERTIES: +:ID: 5e6486bb-fda2-4558-aed8-243a9698de85 +:END: + +This proof is mainly tricky because one needs to infer + * Coq Style Guide :PROPERTIES: :CUSTOM_ID: coq-style-guide |