On GitHub, the output of external processes such as isabelle overtake
the stdout/stderr output of the test driver. Flushing stdout/stderr
in the right spots avoids that.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Add a folding group for verbose log output if running in a GitHub
context. GITHUB_REPOSITORY will be set for all GitHub contexts we're
interested in.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
This makes the full low-level logs available in the "Artifacts" tab of
the "Actions" screen.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
This completes the previous commit to run all proof tests on reasonably
high-powered AWS VMs instead of GitHub runners. All tests run in one
go for efficiency.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
This action triggers docker container deployment in the repo
seL4/ci-actions when the C parser changes here.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
* Add Style_pre.thy to contain helpful preliminary definitions.
* Change some style advice according to feedback from the team.
Co-authored-by: Corey Lewis <corlewis@gmail.com>
Co-authored-by: Matthew Brecknell <matthew@brecknell.net>
Signed-off-by: Mitchell Buckley <mitchell.alan.buckley@gmail.com>
The rules in this style guide should work towards achieving these
goals and form the basis for arguing whether a rule should be
there or not.
Signed-off-by: Gerwin Klein <kleing@unsw.edu.au>
Add docs/Style.thy.
This is a starting point for an isabelle style guide. Some of the
material is original and some is incorporated from confluence pages.
I believe that the basics are correct but it will need to be tweaked
and corrected by other proof engineers.
Signed-off-by: Mitchell Buckley <mitchell.alan.buckley@gmail.com>
Importing Init_R into ADT_H was causing EmptyFail_H to fail. Since
no other theories actually depend on Init_R we can instead include
it in the Refine session directly.
Signed-off-by: Mitchell Buckley <mitchell.alan.buckley@gmail.com>
Describe an extremely simple abstract kernel state, and haskell state
that obey the state relation. These states are `zeroed` in the sense
that they have empty heaps, and default values of 0, False, None, []
and similar in all fields.
These states do not satisfy invs or invs', and this is not as strong
a result as showing that kernel initial states satisfy the state
relation, but it is a good sanity check on the relation itself.
Signed-off-by: Mitchell Buckley <mitchell.buckley@data61.csiro.au>
This verifies a C kernel patch (seL4/seL4#409) which consolidates
translation between virtual and physical addresses, and makes it
consistent across architectures. In particular, we always use
`addrFromKPPtr`, even on architectures that don't use a distinct region
to map the kernel ELF. This will facilitate future improvements which
move the ELF mapping into a distinct virtual address region.
Signed-off-by: Matthew Brecknell <Matthew.Brecknell@data61.csiro.au>
Ideally all corres lemmas of the form
`corres rrel P P' my_abstract_function myHaskellFunction`
should be named `myHaskellFunction_corres`.
This commit renames over 200 lemmas to match this style.
Signed-off-by: Mitchell Buckley <mitchell.alan.buckley@gmail.com>
Co-authored-by: Victor Phan <Victor.Phan@data61.csiro.au>
search-replace.sh is a very simple script which takes a list of text
replacements and applies those replacements in all files in the current
directory. The README file contains more detailed information.
Signed-off-by: Mitchell Buckley <mitchell.alan.buckley@gmail.com>
* Import documentation: Haskell assertions
We import some documentation regarding the role of assertions in Haskell, and how we use assertions in Haskell to transport information from abstract invariants to Haskell-to-C refinement proofs.
The file is a Markdown-ified version of previous documentation hosted at UNSW and Data61.
Co-authored-by: Zoltan A. Kocsis <zoltan.kocsis@data61.csiro.au>
Co-authored-by: Matthew Brecknell <Matthew.Brecknell@data61.csiro.au>
Signed-off-by: Zoltan A. Kocsis <zoltan.kocsis@data61.csiro.au>
A previous update to C code added a disjunct to an `if` condition
outside the existing `unlikely` branch hint. This commit is the proof
update for a C patch that extends the branch hint to the full `if`
condition.
Signed-off-by: Matthew Brecknell <Matthew.Brecknell@data61.csiro.au>
* Add comments into proof.
* Unwind some automation to clarify how each subgoal is resolved.
* Remove some "in monad" lemmas about `premption_point`.
Signed-off-by: Mitchell Buckley <Mitchell.Buckley@data61.csiro.au>
Rafal Kolanski
Mitchell Buckley
Gerwin Klein
Gerwin Klein
Corey Lewis
Matthew Brecknell
Mitchell Buckley
Mitchell Buckley
Ryan Barry
Zoltan A. Kocsis