arch-split Refine + EmptyFail_H, add Refine toplevel, clean up small theories - #1041
Conversation
Xaphiosis
added
the
arch-split
| axiomatization where | ||
| ckernel_init_valid_duplicates': | ||
| "\<forall>((tc,s),x) \<in> Init_H. vs_valid_duplicates' (ksPSpace s)" |
There was a problem hiding this comment.
I assume that is the one that ARM also has but the other ones do not. I think assuming this generically is fine, just want to point out that technically this means we have an unnecessary for some architectures. The axiom just assumes "True" in the end, so it's Ok, but we should be aware that we're doing this.
There was a problem hiding this comment.
Should I put in a comment then? Since the assumption is there for all architectures, but trivial for some, it doesn't harm anything... but not sure what would clear it up.
There was a problem hiding this comment.
I think a comment would be good, yes. At least that clears up that we are aware that it's an axiom that is not strictly necessary everywhere, and also that this is harmless.
| (* FIXME arch-split: is this type signature sane? *) | ||
| definition full_invs :: "(('a \<times> det_ext state) \<times> mode \<times> event option) set" where |
There was a problem hiding this comment.
It is, but I have forgotten (not for the first time) what tc is. Possibly worth a comment here when we find out, since it is ignored in this definition.
There was a problem hiding this comment.
I think tc is user_context in the main place that this is used. I guess it maybe stands for 'thread context'?
There was a problem hiding this comment.
So should I change 'a to user_context, or what? I feel bad leaving it as 'a
There was a problem hiding this comment.
but tc appears free in both full_invs and full_invs' ... hmm
There was a problem hiding this comment.
If I'm right then I think changing it to user_context makes sense. I haven't looked at how they're used in CRefine though.
There was a problem hiding this comment.
I'd be fine leaving it as 'a, but adding a comment that this is the user context, which the invariants don't constrain.
There was a problem hiding this comment.
Somewhere between the two of you is calling it 'user_context, which clearly indicates what it is, but also that it's free. Would that work?
| lemma ckernel_invariant: | ||
| "ADT_H uop \<Turnstile> full_invs'" |
There was a problem hiding this comment.
I wonder if it is worth it spelling out these top-level theorems again manually in the top-level Refine theory. Just without name and proved by fact from the locale interpretation. Doesn't really do anything apart from confirming without doubt that the top-level theorem holds without hidden assumptions in the way we want it.
There was a problem hiding this comment.
I am not opposed to the principle, but don't feel very motivated to do the execution :)
Feel free anytime after this is merged.
lsf37
left a comment
lsf37
left a comment
There was a problem hiding this comment.
Excellent! Congratulations on reaching the end of Refine 🎉 🎉
I don't have any complaints this this time, looks all very good.
Things to consider for future: do we get rid of LevityCatch by distributing it into later theories?
That would be nice to do, yes. It's not really needed any longer and everything in there is there because it should be distributed.
Having both [Arch]EmptyFail.thy and [Arch]EmptyFail_H.thy is confusing, but the latter isn't imported for CRefine, which provides a very small time save.
I'd be fine with either option: leaving them as is or integrating them into one and take a small time hit for CRefine. The latter is potentially less error prone for the future because it collects everything in one place and we won't have these situations any more where we've included the wrong EmptyFail and something isn't visible because of that. There is a chance that integrating them fails in first instance because they build on different contexts.
| apply (clarsimp simp: device_mem_def device_mem'_def pointerInUserData_relation | ||
| pointerInDeviceData_relation) | ||
| done | ||
| lemmas [simp] = valid_sched_init[simplified] |
There was a problem hiding this comment.
This seems a little bit unexpected, why do we need the simplified version in simp now?
There was a problem hiding this comment.
This one is super annoying. When you take valid_sched (init_A_st :: det_state) and simplify it, it explodes with valid_sched_2 ......... ...... .. ...... ....... Not something I'd want to type out, but also not in simp normal form.
I don't know why exactly it blows up, and not sure now's the time to fix it, but I agree this is unexpected.
I will attempt to make the interface assumption [simplified, simp] and add a comment.
There was a problem hiding this comment.
Similar things happen a lot in MCS and there it is due to scheduler_action s = resume_current_thread being in the assumptions, and so the scheduler_action s field of valid_sched_2 will be rewritten since valid_sched is an abbreviation. Maybe this or something similar is happening for you. It's really annoying, since then the elim rules for valid_sched won't fire and unfolding the definition takes a very long time. So we made schact_is_rct a definition to avoid this particular case and it's worked well.
There was a problem hiding this comment.
Right, it's because sched_act_init: scheduler_action init_A_st = resume_cur_thread is in the simpset, meaning that:
valid_sched (init_A_st :: det_state)
is rewritten to
valid_sched_2 (ready_queues init_A_st) (etcbs_of init_A_st) resume_cur_thread (cur_domain init_A_st) (kheap init_A_st) (cur_thread init_A_st) (idle_thread init_A_st)
There was a problem hiding this comment.
Yeah, I have to move the sched_act_init assumption up a bit, and then we end up with:
assumes sched_act_init[simp]:
"scheduler_action (init_A_st :: det_state) = resume_cur_thread"
(* sched_act_init being in the simpset automatically expands this to a no-longer-abbreviated
valid_sched_2 term we don't want to type out, but it's still used to simplify the proofs *)
assumes valid_sched_init[simplified, simp]:
"valid_sched (init_A_st :: det_state)"
There was a problem hiding this comment.
@michaelmcinerney yeah, I think this is not ideal since it foot-guns itself directly with sched_act_init being put into simp, and then valid_sched_init ending up in non-simp-form because of it. if we ever do work in this file again, might be worth unscrambling
| lemma device_update_invs': | ||
| "\<lbrace>invs'\<rbrace>doMachineOp (device_memory_update ds) | ||
| \<lbrace>\<lambda>_. invs'\<rbrace>" |
There was a problem hiding this comment.
Not new but while we're cleaning so much else up here, fixing this style would be good.
| (m = IdleMode \<longrightarrow> ct_idle' s) \<and> | ||
| (e \<noteq> None \<and> e \<noteq> Some Interrupt \<longrightarrow> ct_running' s) \<and> | ||
| 0 < ksDomainTime s}" | ||
| "full_invs' \<equiv> {((tc,s),m,e). |
There was a problem hiding this comment.
Adding a type_signature to full_invs was a good idea, should we do the same here?
There was a problem hiding this comment.
Will do, but this has the same 'a problem in the type signature as with full_invs, see earlier comments in this PR
| rule: doUserOp_def) (* FIXME: crunch can't find the rule of locale-defined constant *) | ||
| rule: doUserOp_def) (* crunch can't find the rule of locale-defined constant *) |
There was a problem hiding this comment.
I think you accidentally reverted this FIXME in a rebase.
There was a problem hiding this comment.
Many thanks for finding this. I got a huge conflict in the rebase and couldn't figure out what the actual issue was. This line! Will put the FIXME back
| apply (drule_tac sz=sz and n="(p && mask (pageBitsForSize sz)) >> pageBits" | ||
| in typ_at_ADeviceDataI[where s=s and s'=s']) |
There was a problem hiding this comment.
I think the second line should be indented one more?
| lemmas finalise_spec_empty_fail_induct = finaliseSlot'.induct[where P= | ||
| "\<lambda>sl exp s. spec_empty_fail (finaliseSlot' sl exp) s"] |
There was a problem hiding this comment.
I think this was just moved but style could be improved.
| (* FIXME arch-split: if we adopt lowercase arch_ naming for these, then the fact that we also | ||
| adopted Arch_ prefix for design-spec abbreviations to assist crunch becomes inconsistent *) | ||
| assumes Arch_finaliseCap_empty_fail[intro!, wp, simp]: | ||
| "\<And>x y. empty_fail (Arch.finaliseCap x y)" |
There was a problem hiding this comment.
It would be good to come to a consensus on this now, or, since this doesn't make that much difference, at least make an arbitrary decision so that we can start working towards consistency.
In my mind, the Arch_ prefix for constant names is consistent with and comes from the Haskell code using Arch. to qualify a lot of its names of arch functions. Since I don't think we're going to change the Haskell, it makes sense to me to keep Arch_ for prefixing abbreviations in Refine.
The next question is whether we're more annoyed about lemma names starting with a capital or with lemma names not matching the constants that they are about. I personally don't have a strong preference either direction beyond a desire for consistency.
There was a problem hiding this comment.
Talked this over with @lsf37 as well, and it seems we have a three-way consensus. The Arch. to Arch_ for naming makes some sense, but I don't think any of us much like lemma names starting with caps. So I will make this lowercase here, but sadly I did not do this in past bits of Refine arch-split, so might have to go back for that during cleanup.
There was a problem hiding this comment.
Sounds like a plan. No rush for that cleanup but should we make an issue so that we don't forget this decision that we've just made?
|
Minor commit suggestion: for "refine: remove InitLemmas" I think it should either be "Content was generic" or "Contents were generic" |
I was leaning towards combining them but a quick experiment suggests that it might be more work than we want to do now to sort out the dependencies. Parts of Refine depends on lemmas in [Arch]EmptyFail, while some of the more complicated [Arch]EmptyFail_H proofs use lemmas from Refine. That means we can't easily consolidate all of the |
corlewis
left a comment
corlewis
left a comment
There was a problem hiding this comment.
Amazing to see the end of Refine, and with so much still being able to made generic in these last files! Just a few minor comments and questions from my side.
Will go with "were", thank you! Also thanks for looking at the EmptyFail situation. That does suck a bit, unsure where that leaves us for future situations. Maybe the bits of Refine these depend on can be migrated upstream to EmptyFail also, but without looking deeper I don't know. Anyway, looks like not a near future cleanup. |
ac25a6c to
587b7d6
Compare
|
Squashed and rebased. Will do a final read over the commits and merge once tests pass. |
This lemma was accidentally copied from AARCH64 during arch-split, and isn't needed on non-VCPU architectures. Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
This theory file is identical on all arches except for header. Use the ARM version which appears to be the original. Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
It makes sense to have the same set of axioms on all architectures, and is very convenient when it comes to phrasing top-level theorems. Because of this, the axioms include ckernel_init_valid_duplicates' on all architectures, even though vs_valid_duplicates' is trivially true on architectures that don't have page table duplicates (i.e. not 32-bit Arm). Having an axiom that is trivially satisfiable is redundant on these architectures, but harmless. Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
In preparation for arch-split. Create Refine.thy and update import hierarchy. PageTableDuplicates import remains in Arch theory, in preparation for removal on non-Arm-32 architectures. Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
We previously removed everything from these theories. Now we can remove them as they are only included from ArchRefine.thy on ARM and ARM_HYP. Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
Contents were generic and identical on all architectures, now integrated into Refine.thy Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
Includes everything previously included in the ROOT file, except for [Arch]Refine.thy itself, which is included via EmptyFail_H. Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
Refine previously contained the entire abstract-to-design refinement theorem, but arch-split resulted in its instantiations being in ArchRefine. Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
The proofs in RAB_FN now work on all architectures and can be made generic. AARCH64 had moved resolveAddressBitsFn_real_cte_at' to Fastpath_Equiv, which is now no longer necessary. Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
In preparation for arch-split. Create EmptyFail_H.thy and update import hierarchy. Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
4 participants
🦆🦆🦆 This is the last of arch-split Refine pass 1, except LevityCatch which I'll deal with as part of cleanup. There are quite a few commits in this one, due to dealing with the smaller theories. The main action is in Refine.thy and EmptyFail_H.thy, which follow the usual arch-split copy-AARCH64-REST process. Review commit-by-commit.
Things to consider for future: do we get rid of LevityCatch by distributing it into later theories? Having both [Arch]EmptyFail.thy and [Arch]EmptyFail_H.thy is confusing, but the latter isn't imported for CRefine, which provides a very small time save.
Commits tagged [fake] are generated to make PR review easier.
For Refine and EmptyFail_H we have:
Apart from those, we have:
refine riscv64+x64: remove archThreadSet_if_live': cleanup, thanks @corlewis for pointing this outrefine: make IncKernelInit.thy generic, use ARM versionrefine: make KernelInit_R generic, use ARM versionrefine: remove PageTableDuplicates on 64-bit architecturesrefine: remove InitLemmasrefine: add new RefineToplevel_R to Refine session, plus commits updating include hierachyrefine+crefine: make RAB_FN genericStats: 56 files changed, 2294 insertions(+), 6739 deletions(-)
Total: 4445 lines removed