Explain why the rule is strong enough as is before I prove the
(not really) stronger version yet again.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
The new corres method is similar to the corresK method and calculus,
but much less ambitious. Its main purpose is to automate boilerplate
proof steps in corres proofs and is specifically not trying to fully
automate corres proofs (although some few might be solved).
The idea is that the method will make some progress with obvious steps
and leave over a proof state the user can operate on further.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
This also renames most of the corres* methods to corresK* methods,
including corressimp -> corresKsimp.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Demonstrates use of corres_cases and corres_cases_both. Main intended
benefit is less thinking about safety of schematics, fewer mentions
of goal parameter names, and fewer manual guard instantiations.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Add safe datatype case distinction for corres -- wpc turns out to be
insufficient even after generalisation of the helper predicate.
- corres_cases_left: case distinction on abstract monad
- corres_cases_right: case distinction on concrete monad
- corres_cases: try first corres_cases_left, then corres_cases_right
- corres_cases_both: simultaneous (quadratic) case distinction on
both sides, with safe elimination of trivially contradictory cases.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
The implicit GITHUB_TOKEN does not trigger further push actions in
the same repo, but in this case we do want the push action to happen
on the `-rebased` branches, so we use an explicit auth token instead.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
This demonstrates some sanity checking, a standard iterate-rewrite-refl
deployment, and the three symbolic execution methods, with a lot of
commentary.
Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
While in many cases using an eta form with a bind (`f >>= (λrv. g rv)`)
does manage to preserve names, this was not true in general when working
with monadic_rewrite. An obvious case of this was when performing a
rewrite in the middle of a function, all bound variables on the way to
that point would get renamed to `x`.
In order to iterate over a chain of bind/bindE with a
monadic_rewrite_bind_tail-style rule such that bound names are
preserved, the rule's `f >>= (λrv. g rv)` must match up with the
relevant bound term `do x <- f'; g' x; ...` on the RHS/LHS and only on
that side:
* if the rule has an eta term on both sides and the goal a schematic on
any side, the schematic will match trivially producing the correct
name in the first subgoal only
* if the goal is not schematic and a tail rule applies, we need to
choose a side to get the name from (usually the left)
This means if the goal is schematic on the RHS, we need a tail rule with
an eta term on its LHS, and vice-versa.
Since a generic form of this is not possible, this commit introduces
transformation lemmas and updates the tactics to use them for stepping
on the left/right.
For stopping the iteration by applying a rule to the head of a bind, the
situation is reversed: to preserve the name of the bind in the tail, the
head rule must not have any eta terms. The bind[E]_head rules have been
updated to reflect this.
Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
- rename corres_pre set in CRefine to ccorres_pre
- rename internal corres_pre method in Corres_Method to corres_pre'
- use corres_pre instead of old wp_pre in refine
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Factor out pre_tac such that we can have separate theorem sets and
methods for wp_pre, monadic_rewrite_pre, corres_pre, and potentially
others in the future.
Leave everything in wp_pre that we expect to use wp or wpsimp on, in
particular no_fail.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
- document the wpc_helper predicate and setup for wpc
(but not the proof method internals at this point)
- add facilities for a second guard of predicate type
The current setup works well for judgements with one guard of type
predicate or set (valid, validE, etc), or with two guards where one is
a predicate and the other is a set (ccorres), but not for judgements
that have two predicate guards, i.e. plain corres. This commit adds a
second such guard, which can be ignored for the judgements that don't
need it in the same way that valid/validE currently ignore the set-type
guard.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
The action will abort when no clean rebase is possible, and force-push
the rebased branch when the rebase over origin/master was clean.
The push will trigger proof runs on the rebased branches.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
REFINE_QUICK_AND_DIRTY is already set correctly in proofs/Makefile,
so doesn't need to be set here.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
The Orphanage session is no longer conditional on L4V_ARCH_IS_ARM
(instead it is empty for those architectures that don't support it).
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
This adds sch_act_target/schActTarget accessor names for the
switch_thread/SwitchToThread constructor of the scheduler_action
datatype at the aspec and Haskell level, respectively
Signed-off-by: Michael McInerney <michael.mcinerney@proofcraft.systems>
CI is introducing an `L4V_PLAT` variable to support proof runs across
more platform configurations. This commit incorporates `L4V_PLAT` into
the paths generated by `export-kernel-builds.py`, to ensure that
exported builds can be disambiguated.
Signed-off-by: Matthew Brecknell <matt@kry10.com>
L4V_PLAT selects a platform variation within a L4V_ARCH. This mostly
affects which seL4 cmake config file is loaded when building config
data and the kernel C code. This in turn affects (and will rebuild)
ASpec, ExecSpec, and CSpec.
Examples:
L4V_ARCH=ARM L4V_FEATURES="" L4V_PLAT=""
will load `ARM_verified.cmake`
L4V_ARCH=ARM L4V_FEATURES="" L4V_PLAT=imx8mm
will load `ARM_imx8mm_verified.cmake`, and
L4V_ARCH=ARM L4V_FEATURES=MCS L4V_PLAT=imx8mm
will load `ARM_MCS_imx8mm_verified.cmake`
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Provide L4V_ARCH targets in the Haskell Makefile and constrain
run_tests to use only the current L4V_ARCH, to avoid building all
architectures in all tests.
A manual invocation of just `make` will still build all architectures
for easier checking.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Corey Lewis
Corey Lewis
Gerwin Klein
Rafal Kolanski
Michael McInerney
Matthew Brecknell