Library Pip.Proof.invariants.WritePhyEntryPrepareProperties
Summary
This file contains the invariant of writePhyEntry. We prove that this instruction preserves the isolation propertyRequire Import Pip.Model.ADT Pip.Model.Hardware Pip.Model.Lib Pip.Model.MAL.
Require Import Pip.Core.Services.
Require Import Pip.Proof.Consistency Pip.Proof.DependentTypeLemmas Pip.Proof.InternalLemmas
Pip.Proof.InternalLemmas2 Pip.Proof.Isolation Pip.Proof.StateLib Pip.Proof.WeakestPreconditions.
Require Import Invariants GetTableAddr Lib MapMMUPage PropagatedProperties WriteAccessible WritePhyEntryPrepare.
Import Arith Bool Classical_Prop Coq.Logic.ProofIrrelevance Lia List ListNotations.
Lemma kernelDataIsolationAddIndirection
s indirection nextIndirection entry nbLgen pd idxroot
(vaToPrepare vaNextInd : vaddr) partition l
(currentPart currentPD ptMMUvaNextInd ptSh1VaNextInd: page) root r w e phyPDChild phyMMUaddr phySh1Child
phySh1addr phySh2Child phySh2addr lpred:
nextIndirectionsOR indirection nextIndirection phyPDChild phyMMUaddr phySh1Child
phySh1addr phySh2Child phySh2addr idxroot →
isWellFormedFstShadow lpred phySh1addr s →
StateLib.Level.pred l = Some lpred →
or3 idxroot →
(∀ parts, In parts (getPartitions multiplexer s) →
¬ In nextIndirection (getAccessibleMappedPages parts s)) →
kernelDataIsolation s →
lookup indirection (StateLib.getIndexOfAddr vaToPrepare l) (memory s) beqPage beqIndex = Some (PE entry) →
verticalSharing s →
partitionsIsolation s →
consistency s →
Some nbLgen = StateLib.getNbLevel →
indirectionDescription s partition indirection idxroot vaToPrepare l →
StateLib.readPhyEntry indirection (StateLib.getIndexOfAddr vaToPrepare l) (memory s) = Some defaultPage→
isWellFormedMMUTables phyMMUaddr s →
false = StateLib.Level.eqb l fstLevel →
nextEntryIsPP partition PDidx pd s →
writeAccessibleRecPreparePostcondition currentPart nextIndirection s →
In currentPart (getPartitions multiplexer s) →
getTableAddrRoot ptMMUvaNextInd PDidx currentPart vaNextInd s→
isPE ptMMUvaNextInd (StateLib.getIndexOfAddr vaNextInd fstLevel) s→
entryUserFlag ptMMUvaNextInd (StateLib.getIndexOfAddr vaNextInd fstLevel) false s →
entryPresentFlag ptMMUvaNextInd (StateLib.getIndexOfAddr vaNextInd fstLevel) true s →
nextEntryIsPP currentPart PDidx currentPD s →
(defaultPage =? ptMMUvaNextInd) = false →
isEntryPage ptMMUvaNextInd (StateLib.getIndexOfAddr vaNextInd fstLevel) nextIndirection s →
(defaultPage =? ptSh1VaNextInd) = false →
getTableAddrRoot ptSh1VaNextInd sh1idx currentPart vaNextInd s →
isVE ptSh1VaNextInd (StateLib.getIndexOfAddr vaNextInd fstLevel) s →
noDupPartitionTree s →
nextIndirection ≠ indirection →
partitionDescriptorEntry s →
In partition (getPartitions multiplexer s) →
noDupConfigPagesList s →
isPresentNotDefaultIff s →
configTablesAreDifferent s →
(defaultPage =? nextIndirection) = false →
nextEntryIsPP partition idxroot root s →
In indirection (getIndirections root s)→
isWellFormedTables phyMMUaddr phySh1addr phySh2addr lpred s →
kernelDataIsolation
{|
currentPartition := currentPartition s;
memory := add indirection (StateLib.getIndexOfAddr vaToPrepare l)
(PE
{|
read := r;
write := w;
exec := e;
present := true;
user := true;
pa := nextIndirection |}) (memory s) beqPage beqIndex |}.
Lemma toApplykernelDataIsolationAddIndirection indirection nextIndirection ptMMUTrdVA phySh2addr phySh1addr indMMUToPrepare ptMMUFstVA phyMMUaddr
phyPDChild currentShadow2 phySh2Child currentPD ptSh1TrdVA ptMMUSndVA
ptSh1SndVA ptSh1FstVA currentShadow1 descChildphy phySh1Child currentPart trdVA nextVA
vaToPrepare sndVA fstVA nbLgen l idxFstVA idxSndVA idxTrdVA zeroI lpred fstLL LLChildphy
lastLLTable e w r idxroot entry pdchild s:
(∀ part : page, In part (getPartitions multiplexer s) → ¬In nextIndirection (getConfigPages part s)) →
¬ In nextIndirection (getConfigPages descChildphy s) →
In indirection (getConfigPages descChildphy s) →
StateLib.readPhyEntry phyPDChild (StateLib.getIndexOfAddr vaToPrepare l) (memory s) = Some defaultPage →
nextIndirectionsOR indirection nextIndirection phyPDChild phyMMUaddr phySh1Child phySh1addr phySh2Child phySh2addr idxroot→
or3 idxroot →
insertEntryIntoLLPC s ptMMUTrdVA phySh2addr phySh1addr indMMUToPrepare ptMMUFstVA phyMMUaddr
lastLLTable phyPDChild currentShadow2 phySh2Child currentPD ptSh1TrdVA ptMMUSndVA
ptSh1SndVA ptSh1FstVA currentShadow1 descChildphy phySh1Child currentPart trdVA nextVA
vaToPrepare sndVA fstVA nbLgen l idxFstVA idxSndVA idxTrdVA zeroI lpred fstLL LLChildphy
lastLLTable (CIndex (CIndex (CIndex (CIndex 3 - 1) - 1) - 1)) true →
lookup indirection (StateLib.getIndexOfAddr vaToPrepare l) (memory s) beqPage beqIndex =
Some (PE entry) →
nextEntryIsPP descChildphy PDidx pdchild s →
(∀ parts : page,
In parts (getPartitions multiplexer s) → ¬In nextIndirection (getAccessibleMappedPages parts s)) →
kernelDataIsolation
{|
currentPartition := currentPartition s;
memory := add indirection (StateLib.getIndexOfAddr vaToPrepare l)
(PE {| read := r; write := w; exec := e; present := true; user := true; pa := nextIndirection |})
(memory s) beqPage beqIndex |}.
Lemma partitionsIsolationAddIndirection
s indirection nextIndirection entry nbLgen pd idxroot
(vaToPrepare vaNextInd : vaddr) phyDescChild l
(currentPart currentPD ptMMUvaNextInd ptSh1VaNextInd: page) root r w e phyPDChild phyMMUaddr phySh1Child
phySh1addr phySh2Child phySh2addr lpred:
newIndirectionsAreNotMappedInChildrenAll s currentPart phyMMUaddr phySh1addr phySh2addr →
partitionsIsolation s →
nextIndirectionsOR indirection nextIndirection phyPDChild phyMMUaddr phySh1Child
phySh1addr phySh2Child phySh2addr idxroot →
isWellFormedFstShadow lpred phySh1addr s →
StateLib.Level.pred l = Some lpred →
or3 idxroot →
(∀ parts, In parts (getPartitions multiplexer s) →
¬ In nextIndirection (getAccessibleMappedPages parts s)) →
kernelDataIsolation s →
initPEntryTablePreconditionToPropagatePreparePropertiesAll s phyMMUaddr phySh1addr phySh2addr →
lookup indirection (StateLib.getIndexOfAddr vaToPrepare l) (memory s) beqPage beqIndex = Some (PE entry) →
verticalSharing s →
In phyDescChild (getChildren currentPart s) →
consistency s →
Some nbLgen = StateLib.getNbLevel →
indirectionDescription s phyDescChild indirection idxroot vaToPrepare l →
StateLib.readPhyEntry indirection (StateLib.getIndexOfAddr vaToPrepare l) (memory s) = Some defaultPage→
isWellFormedMMUTables phyMMUaddr s →
false = StateLib.Level.eqb l fstLevel →
nextEntryIsPP phyDescChild PDidx pd s →
writeAccessibleRecPreparePostcondition currentPart nextIndirection s →
In currentPart (getPartitions multiplexer s) →
getTableAddrRoot ptMMUvaNextInd PDidx currentPart vaNextInd s→
isPE ptMMUvaNextInd (StateLib.getIndexOfAddr vaNextInd fstLevel) s→
entryUserFlag ptMMUvaNextInd (StateLib.getIndexOfAddr vaNextInd fstLevel) false s →
entryPresentFlag ptMMUvaNextInd (StateLib.getIndexOfAddr vaNextInd fstLevel) true s →
nextEntryIsPP currentPart PDidx currentPD s →
(defaultPage =? ptMMUvaNextInd) = false →
isEntryPage ptMMUvaNextInd (StateLib.getIndexOfAddr vaNextInd fstLevel) nextIndirection s →
(defaultPage =? ptSh1VaNextInd) = false →
getTableAddrRoot ptSh1VaNextInd sh1idx currentPart vaNextInd s →
isVE ptSh1VaNextInd (StateLib.getIndexOfAddr vaNextInd fstLevel) s →
noDupPartitionTree s →
nextIndirection ≠ indirection →
partitionDescriptorEntry s →
In phyDescChild (getPartitions multiplexer s) →
noDupConfigPagesList s →
isPresentNotDefaultIff s →
configTablesAreDifferent s →
(defaultPage =? nextIndirection) = false →
nextEntryIsPP phyDescChild idxroot root s →
In indirection (getIndirections root s)→
In indirection (getConfigPages phyDescChild s) →
isWellFormedTables phyMMUaddr phySh1addr phySh2addr lpred s →
partitionsIsolation
{|
currentPartition := currentPartition s;
memory := add indirection (StateLib.getIndexOfAddr vaToPrepare l)
(PE
{|
read := r;
write := w;
exec := e;
present := true;
user := true;
pa := nextIndirection |}) (memory s) beqPage beqIndex |}.
propagate new internal property: ~ In child (getMappedPages phyDescChild s)
propagate new internal property: ~In nextIndirection (getMappedPages phyDescChild s)
propagate new internal property: ~ In child (getMappedPages phyDescChild s)
propagate new internal property: ~In nextIndirection (getMappedPages phyDescChild s)
Lemma toApplyPartitionsIsolationAddIndirection indirection nextIndirection ptMMUTrdVA phySh2addr phySh1addr indMMUToPrepare ptMMUFstVA phyMMUaddr
phyPDChild currentShadow2 phySh2Child currentPD ptSh1TrdVA ptMMUSndVA
ptSh1SndVA ptSh1FstVA currentShadow1 descChildphy phySh1Child currentPart trdVA nextVA
vaToPrepare sndVA fstVA nbLgen l idxFstVA idxSndVA idxTrdVA zeroI lpred fstLL LLChildphy
lastLLTable e w r idxroot entry pdchild s:
(∀ part : page, In part (getPartitions multiplexer s) → ¬In nextIndirection (getConfigPages part s)) →
¬ In nextIndirection (getConfigPages descChildphy s) →
In indirection (getConfigPages descChildphy s) →
StateLib.readPhyEntry phyPDChild (StateLib.getIndexOfAddr vaToPrepare l) (memory s) = Some defaultPage →
nextIndirectionsOR indirection nextIndirection phyPDChild phyMMUaddr phySh1Child phySh1addr phySh2Child phySh2addr idxroot→
or3 idxroot →
insertEntryIntoLLPC s ptMMUTrdVA phySh2addr phySh1addr indMMUToPrepare ptMMUFstVA phyMMUaddr
lastLLTable phyPDChild currentShadow2 phySh2Child currentPD ptSh1TrdVA ptMMUSndVA
ptSh1SndVA ptSh1FstVA currentShadow1 descChildphy phySh1Child currentPart trdVA nextVA
vaToPrepare sndVA fstVA nbLgen l idxFstVA idxSndVA idxTrdVA zeroI lpred fstLL LLChildphy
lastLLTable (CIndex (CIndex (CIndex (CIndex 3 - 1) - 1) - 1)) true →
lookup indirection (StateLib.getIndexOfAddr vaToPrepare l) (memory s) beqPage beqIndex =
Some (PE entry) →
nextEntryIsPP descChildphy PDidx pdchild s →
(∀ parts : page,
In parts (getPartitions multiplexer s) → ¬In nextIndirection (getAccessibleMappedPages parts s)) →
In descChildphy (getChildren (currentPartition s) s) →
partitionsIsolation
{|
currentPartition := currentPartition s;
memory := add indirection (StateLib.getIndexOfAddr vaToPrepare l)
(PE {| read := r; write := w; exec := e; present := true; user := true; pa := nextIndirection |})
(memory s) beqPage beqIndex |}.
Lemma verticalSharingAddIndirection
s indirection nextIndirection entry nbLgen pd idxroot
(vaToPrepare vaNextInd : vaddr) phyDescChild l
(currentPart currentPD ptMMUvaNextInd ptSh1VaNextInd: page) root r w e phyPDChild phyMMUaddr phySh1Child
phySh1addr phySh2Child phySh2addr lpred:
newIndirectionsAreNotMappedInChildrenAll s currentPart phyMMUaddr phySh1addr phySh2addr →
verticalSharing s →
nextIndirectionsOR indirection nextIndirection phyPDChild phyMMUaddr phySh1Child
phySh1addr phySh2Child phySh2addr idxroot →
isWellFormedFstShadow lpred phySh1addr s →
StateLib.Level.pred l = Some lpred →
or3 idxroot →
(∀ parts, In parts (getPartitions multiplexer s) →
¬ In nextIndirection (getAccessibleMappedPages parts s)) →
kernelDataIsolation s →
initPEntryTablePreconditionToPropagatePreparePropertiesAll s phyMMUaddr phySh1addr phySh2addr →
lookup indirection (StateLib.getIndexOfAddr vaToPrepare l) (memory s) beqPage beqIndex = Some (PE entry) →
verticalSharing s →
In phyDescChild (getChildren currentPart s) →
consistency s →
Some nbLgen = StateLib.getNbLevel →
indirectionDescription s phyDescChild indirection idxroot vaToPrepare l →
StateLib.readPhyEntry indirection (StateLib.getIndexOfAddr vaToPrepare l) (memory s) = Some defaultPage→
isWellFormedMMUTables phyMMUaddr s →
false = StateLib.Level.eqb l fstLevel →
nextEntryIsPP phyDescChild PDidx pd s →
writeAccessibleRecPreparePostcondition currentPart nextIndirection s →
In currentPart (getPartitions multiplexer s) →
getTableAddrRoot ptMMUvaNextInd PDidx currentPart vaNextInd s→
isPE ptMMUvaNextInd (StateLib.getIndexOfAddr vaNextInd fstLevel) s→
entryUserFlag ptMMUvaNextInd (StateLib.getIndexOfAddr vaNextInd fstLevel) false s →
entryPresentFlag ptMMUvaNextInd (StateLib.getIndexOfAddr vaNextInd fstLevel) true s →
nextEntryIsPP currentPart PDidx currentPD s →
(defaultPage =? ptMMUvaNextInd) = false →
isEntryPage ptMMUvaNextInd (StateLib.getIndexOfAddr vaNextInd fstLevel) nextIndirection s →
(defaultPage =? ptSh1VaNextInd) = false →
getTableAddrRoot ptSh1VaNextInd sh1idx currentPart vaNextInd s →
isVE ptSh1VaNextInd (StateLib.getIndexOfAddr vaNextInd fstLevel) s →
noDupPartitionTree s →
nextIndirection ≠ indirection →
partitionDescriptorEntry s →
In phyDescChild (getPartitions multiplexer s) →
noDupConfigPagesList s →
isPresentNotDefaultIff s →
configTablesAreDifferent s →
(defaultPage =? nextIndirection) = false →
nextEntryIsPP phyDescChild idxroot root s →
In indirection (getIndirections root s)→
In indirection (getConfigPages phyDescChild s) →
isWellFormedTables phyMMUaddr phySh1addr phySh2addr lpred s →
verticalSharing
{|
currentPartition := currentPartition s;
memory := add indirection (StateLib.getIndexOfAddr vaToPrepare l)
(PE
{|
read := r;
write := w;
exec := e;
present := true;
user := true;
pa := nextIndirection |}) (memory s) beqPage beqIndex |}.
Lemma toApplyVerticalSharingAddIndirection indirection nextIndirection ptMMUTrdVA phySh2addr phySh1addr indMMUToPrepare ptMMUFstVA phyMMUaddr
phyPDChild currentShadow2 phySh2Child currentPD ptSh1TrdVA ptMMUSndVA
ptSh1SndVA ptSh1FstVA currentShadow1 descChildphy phySh1Child currentPart trdVA nextVA
vaToPrepare sndVA fstVA nbLgen l idxFstVA idxSndVA idxTrdVA zeroI lpred fstLL LLChildphy
lastLLTable e w r idxroot entry pdchild s:
(∀ part : page, In part (getPartitions multiplexer s) → ¬In nextIndirection (getConfigPages part s)) →
¬ In nextIndirection (getConfigPages descChildphy s) →
In indirection (getConfigPages descChildphy s) →
StateLib.readPhyEntry phyPDChild (StateLib.getIndexOfAddr vaToPrepare l) (memory s) = Some defaultPage →
nextIndirectionsOR indirection nextIndirection phyPDChild phyMMUaddr phySh1Child phySh1addr phySh2Child phySh2addr idxroot→
or3 idxroot →
insertEntryIntoLLPC s ptMMUTrdVA phySh2addr phySh1addr indMMUToPrepare ptMMUFstVA phyMMUaddr
lastLLTable phyPDChild currentShadow2 phySh2Child currentPD ptSh1TrdVA ptMMUSndVA
ptSh1SndVA ptSh1FstVA currentShadow1 descChildphy phySh1Child currentPart trdVA nextVA
vaToPrepare sndVA fstVA nbLgen l idxFstVA idxSndVA idxTrdVA zeroI lpred fstLL LLChildphy
lastLLTable (CIndex (CIndex (CIndex (CIndex 3 - 1) - 1) - 1)) true →
lookup indirection (StateLib.getIndexOfAddr vaToPrepare l) (memory s) beqPage beqIndex =
Some (PE entry) →
nextEntryIsPP descChildphy PDidx pdchild s →
(∀ parts : page,
In parts (getPartitions multiplexer s) → ¬In nextIndirection (getAccessibleMappedPages parts s)) →
In descChildphy (getChildren (currentPartition s) s) →
verticalSharing
{|
currentPartition := currentPartition s;
memory := add indirection (StateLib.getIndexOfAddr vaToPrepare l)
(PE {| read := r; write := w; exec := e; present := true; user := true; pa := nextIndirection |})
(memory s) beqPage beqIndex |}.
Lemma partitionDescriptorEntryAddIndirection
s indirection nextIndirection idxroot entry nbLgen pd vaToPrepare partition l lpred r w e
phyPDChild phyMMUaddr phySh1Child phySh1addr phySh2Child phySh2addr :
partitionDescriptorEntry s→
nextIndirectionsOR indirection nextIndirection phyPDChild phyMMUaddr phySh1Child phySh1addr phySh2Child phySh2addr idxroot →
isWellFormedFstShadow lpred phySh1addr s →
StateLib.Level.pred l = Some lpred →
or3 idxroot →
lookup indirection (StateLib.getIndexOfAddr vaToPrepare l) (memory s) beqPage beqIndex = Some (PE entry) →
Some nbLgen = StateLib.getNbLevel →
indirectionDescription s partition indirection idxroot vaToPrepare l →
isWellFormedMMUTables phyMMUaddr s →
false = StateLib.Level.eqb l fstLevel →
nextEntryIsPP partition idxroot pd s →
In indirection (getIndirections pd s) →
StateLib.readPhyEntry indirection (StateLib.getIndexOfAddr vaToPrepare l) (memory s) = Some defaultPage →
noDupPartitionTree s →
nextIndirection ≠ indirection →
partitionDescriptorEntry s →
In partition (getPartitions multiplexer s) →
noDupConfigPagesList s →
isPresentNotDefaultIff s →
configTablesAreDifferent s →
(defaultPage =? nextIndirection) = false →
partitionDescriptorEntry
{|
currentPartition := currentPartition s;
memory := add indirection (StateLib.getIndexOfAddr vaToPrepare l)
(PE
{|
read := r;
write := w;
exec := e;
present := true;
user := true;
pa := nextIndirection |}) (memory s) beqPage beqIndex |}.
Lemma wellFormedRootDataStructAddIndirection indirection idx s phyMMUaddr x e r w level partition (va:vaddr) pd entry idxroot stop indirection0:
let s':= {|
currentPartition := currentPartition s;
memory := add indirection x
(PE
{|
read := r;
write := w;
exec := e;
present := true;
user := true;
pa := phyMMUaddr |}) (memory s) beqPage beqIndex |} in
lookup indirection x (memory s) beqPage beqIndex =
Some (PE entry) →
Some level = StateLib.getNbLevel →
In partition (getPartitions multiplexer s) →
nextEntryIsPP partition idxroot pd s →
dataStructurePdSh1Sh2asRoot idxroot s →
getIndirection pd va level stop s = Some indirection0 →
indirection ≠ defaultPage →
PCWellFormedRootDataStruct stop level indirection0 idx s' idxroot.
Lemma wellFormedMMUAddIndirection n indirection idx s phyMMUaddr m e r w level entry :
let s':= {|
currentPartition := currentPartition s;
memory := add indirection m
(PE
{|
read := r;
write := w;
exec := e;
present := true;
user := true;
pa := phyMMUaddr |}) (memory s) beqPage beqIndex |} in
isWellFormedMMUTables phyMMUaddr s →
lookup indirection m (memory s) beqPage beqIndex =
Some (PE entry) →
(defaultPage =? phyMMUaddr) = false →
PCWellFormedRootDataStruct n level phyMMUaddr idx s' PDidx.
Lemma getIndirectionEqAddIndirectionIndirectionIsRoot p va l0 stop s phyMMUaddr e r w vaToPrepare l indirection entry partition :
let s' := {|
currentPartition := currentPartition s;
memory := add indirection (StateLib.getIndexOfAddr vaToPrepare l)
(PE
{|
read := r;
write := w;
exec := e;
present := true;
user := true;
pa := phyMMUaddr |}) (memory s) beqPage beqIndex |} in
lookup indirection (StateLib.getIndexOfAddr vaToPrepare l) (memory s) beqPage beqIndex =
Some (PE entry) →
false = StateLib.Level.eqb l fstLevel →
StateLib.readPhyEntry indirection (StateLib.getIndexOfAddr va l) (memory s) = Some p →
(defaultPage =? p) = false →
StateLib.Level.pred l = Some l0 →
nextEntryIsPP partition PDidx indirection s →
Some l = StateLib.getNbLevel →
indirection ≠ defaultPage→
NoDup (getIndirectionsAux indirection s nbLevel) →
getIndirection p va l0 stop s' = getIndirection p va l0 stop s.
Lemma getIndirectionEqAddIndirectionIndirectionIsRoot' p va l0 stop s phyMMUaddr e r w
l indirection entry partition m idxroot:
let s' := {|
currentPartition := currentPartition s;
memory := add indirection m
(PE
{|
read := r;
write := w;
exec := e;
present := true;
user := true;
pa := phyMMUaddr |}) (memory s) beqPage beqIndex |} in
lookup indirection m (memory s) beqPage beqIndex =
Some (PE entry) →
false = StateLib.Level.eqb l fstLevel →
StateLib.readPhyEntry indirection (StateLib.getIndexOfAddr va l) (memory s) = Some p →
(defaultPage =? p) = false →
StateLib.Level.pred l = Some l0 →
nextEntryIsPP partition idxroot indirection s →
Some l = StateLib.getNbLevel →
indirection ≠ defaultPage→
NoDup (getIndirectionsAux indirection s nbLevel) →
getIndirection p va l0 stop s' = getIndirection p va l0 stop s.
Lemma PCWellFormedDataStructAddIndirection stop indirection0 idx s phyMMUaddr e r w m
l va indirection entry partition lpred:
let s' := {|
currentPartition := currentPartition s;
memory := add indirection m
(PE {| read := r; write := w; exec := e; present := true; user := true; pa := phyMMUaddr |})
(memory s) beqPage beqIndex |} in
getIndirection indirection va l stop s' = Some indirection0 →
lookup indirection m (memory s) beqPage beqIndex =
Some (PE entry) →
In partition (getPartitions multiplexer s) →
nextEntryIsPP partition PDidx indirection s →
Some l = StateLib.getNbLevel →
false = StateLib.Level.eqb l fstLevel →
StateLib.Level.pred l = Some lpred →
(defaultPage =? phyMMUaddr) = false →
dataStructurePdSh1Sh2asRoot PDidx s →
isWellFormedMMUTables phyMMUaddr s →
phyMMUaddr ≠ indirection →
indirection ≠ defaultPage →
NoDup (getIndirectionsAux indirection s nbLevel) →
PCWellFormedRootDataStruct stop l indirection0 idx s' PDidx.
Lemma wellFormedSh1AddIndirection l indirection0 vaToPrepare m va stop indirection idx s phySh1addr e r w level entry lpred :
let s':= {|
currentPartition := currentPartition s;
memory := add indirection (StateLib.getIndexOfAddr vaToPrepare m)
(PE
{|
read := r;
write := w;
exec := e;
present := true;
user := true;
pa := phySh1addr |}) (memory s) beqPage beqIndex |} in
phySh1addr ≠ indirection →
isWellFormedFstShadow lpred phySh1addr s →
lookup indirection (StateLib.getIndexOfAddr vaToPrepare m) (memory s) beqPage beqIndex =
Some (PE entry) →
(defaultPage =? phySh1addr) = false →
false = StateLib.Level.eqb level fstLevel →
StateLib.Level.pred level = Some lpred →
StateLib.readPhyEntry indirection (StateLib.getIndexOfAddr va l)
(add indirection (StateLib.getIndexOfAddr va l)
(PE {| read := r; write := w; exec := e; present := true; user := true; pa := phySh1addr |}) (memory s) beqPage beqIndex) =
Some phySh1addr →
getIndirection phySh1addr va lpred stop s' = Some indirection0→
PCWellFormedRootDataStruct (S stop) level indirection0 idx s' sh1idx.
Lemma wellFormedSh2AddIndirection l indirection0 vaToPrepare m va stop indirection idx s phySh2addr e r w level entry lpred :
let s':= {|
currentPartition := currentPartition s;
memory := add indirection (StateLib.getIndexOfAddr vaToPrepare m)
(PE
{|
read := r;
write := w;
exec := e;
present := true;
user := true;
pa := phySh2addr |}) (memory s) beqPage beqIndex |} in
phySh2addr ≠ indirection →
isWellFormedSndShadow lpred phySh2addr s →
lookup indirection (StateLib.getIndexOfAddr vaToPrepare m) (memory s) beqPage beqIndex =
Some (PE entry) →
(defaultPage =? phySh2addr) = false →
false = StateLib.Level.eqb level fstLevel →
StateLib.Level.pred level = Some lpred →
StateLib.readPhyEntry indirection (StateLib.getIndexOfAddr va l)
(add indirection (StateLib.getIndexOfAddr va l)
(PE {| read := r; write := w; exec := e; present := true; user := true; pa := phySh2addr |}) (memory s) beqPage beqIndex) =
Some phySh2addr →
getIndirection phySh2addr va lpred stop s' = Some indirection0→
PCWellFormedRootDataStruct (S stop) level indirection0 idx s' sh2idx.
Lemma PCWellFormedDataStructAddIndirectionsh1 stop indirection0 idx s phySh1addr e r w m
l va indirection entry partition lpred:
let s' := {|
currentPartition := currentPartition s;
memory := add indirection m
(PE {| read := r; write := w; exec := e; present := true; user := true; pa := phySh1addr |})
(memory s) beqPage beqIndex |} in
getIndirection indirection va l stop s' = Some indirection0 →
lookup indirection m (memory s) beqPage beqIndex =
Some (PE entry) →
In partition (getPartitions multiplexer s) →
nextEntryIsPP partition sh1idx indirection s →
Some l = StateLib.getNbLevel →
false = StateLib.Level.eqb l fstLevel →
StateLib.Level.pred l = Some lpred →
(defaultPage =? phySh1addr) = false →
dataStructurePdSh1Sh2asRoot sh1idx s →
isWellFormedFstShadow lpred phySh1addr s →
phySh1addr ≠ indirection →
indirection ≠ defaultPage →
NoDup (getIndirectionsAux indirection s nbLevel) →
PCWellFormedRootDataStruct stop l indirection0 idx s' sh1idx.
Lemma PCWellFormedDataStructAddIndirectionsh2 stop indirection0 idx s phySh2addr e r w m
l va indirection entry partition lpred:
let s' := {|
currentPartition := currentPartition s;
memory := add indirection m
(PE {| read := r; write := w; exec := e; present := true; user := true; pa := phySh2addr |})
(memory s) beqPage beqIndex |} in
getIndirection indirection va l stop s' = Some indirection0 →
lookup indirection m (memory s) beqPage beqIndex =
Some (PE entry) →
In partition (getPartitions multiplexer s) →
nextEntryIsPP partition sh2idx indirection s →
Some l = StateLib.getNbLevel →
false = StateLib.Level.eqb l fstLevel →
StateLib.Level.pred l = Some lpred →
(defaultPage =? phySh2addr) = false →
dataStructurePdSh1Sh2asRoot sh2idx s →
isWellFormedSndShadow lpred phySh2addr s →
phySh2addr ≠ indirection →
indirection ≠ defaultPage →
NoDup (getIndirectionsAux indirection s nbLevel) →
PCWellFormedRootDataStruct stop l indirection0 idx s' sh2idx.
Lemma getIndirectionEqAddIndirectionIndirectionIsMiddle indirection s phyMMUaddr e r w vaToPrepare l pd level
va stop entry sstop indirection0 :
let s' := {|
currentPartition := currentPartition s;
memory := add indirection (StateLib.getIndexOfAddr vaToPrepare l)
(PE
{|
read := r;
write := w;
exec := e;
present := true;
user := true;
pa := phyMMUaddr |}) (memory s) beqPage beqIndex |} in
NoDup (getIndirectionsAux pd s nbLevel) →
lookup indirection (StateLib.getIndexOfAddr vaToPrepare l) (memory s) beqPage beqIndex =
Some (PE entry) →
indirection ≠ defaultPage→
Some level = StateLib.getNbLevel →
sstop ≤ level →
pd ≠ defaultPage →
getIndirection pd vaToPrepare level sstop s = Some indirection →
sstop > 0 →
StateLib.checkVAddrsEqualityWOOffset sstop vaToPrepare va level = false →
stop ≥ sstop →
indirection0 ≠ defaultPage →
getIndirection pd va level stop s' = Some indirection0 →
getIndirection pd va level stop s' = getIndirection pd va level stop s.
Lemma PCWellFormedRootDataStructAddIndirection pd vaToPrepare (level lpred:level) sstop s indirection idx
va indirection0 stop phyMMUaddr r w e entry partition:
let s' := {|
currentPartition := currentPartition s;
memory := add indirection (StateLib.getIndexOfAddr vaToPrepare (CLevel (level - sstop)))
(PE
{| read := r; write := w; exec := e; present := true; user := true; pa := phyMMUaddr |})
(memory s) beqPage beqIndex |} in
NoDup (getIndirectionsAux pd s nbLevel) →
lookup indirection (StateLib.getIndexOfAddr vaToPrepare (CLevel (level - sstop)))
(memory s) beqPage beqIndex = Some (PE entry) →
isWellFormedMMUTables phyMMUaddr s →
dataStructurePdSh1Sh2asRoot PDidx s →
Some level = StateLib.getNbLevel →
In partition (getPartitions multiplexer s) →
getIndirection pd vaToPrepare level sstop s = Some indirection →
getIndirection pd va level stop s' = Some indirection0 →
stop ≤ nbLevel - 1 →
sstop ≤ level →
stop ≥ sstop →
sstop > 0 →
isPE indirection idx s →
indirection ≠ defaultPage →
false = StateLib.Level.eqb (CLevel (level - sstop)) fstLevel →
(defaultPage =? phyMMUaddr) = false →
StateLib.Level.pred (CLevel (level - sstop)) = Some lpred →
nextEntryIsPP partition PDidx pd s →
indirection0 ≠ defaultPage →
pd ≠ defaultPage →
phyMMUaddr ≠ indirection →
PCWellFormedRootDataStruct stop level indirection0 idx s' PDidx.
Lemma dataStructurePdSh1Sh2asRootMMUAddIndirection
s indirection nextIndirection idxroot entry nbLgen pd vaToPrepare partition l lpred r w e
phyPDChild phyMMUaddr phySh1Child phySh1addr phySh2Child phySh2addr :
dataStructurePdSh1Sh2asRoot PDidx s→
nextIndirectionsOR indirection nextIndirection phyPDChild phyMMUaddr phySh1Child phySh1addr phySh2Child phySh2addr idxroot →
isWellFormedFstShadow lpred phySh1addr s →
StateLib.Level.pred l = Some lpred →
or3 idxroot →
lookup indirection (StateLib.getIndexOfAddr vaToPrepare l) (memory s) beqPage beqIndex = Some (PE entry) →
Some nbLgen = StateLib.getNbLevel →
indirectionDescription s partition indirection idxroot vaToPrepare l →
isWellFormedMMUTables phyMMUaddr s →
false = StateLib.Level.eqb l fstLevel →
nextEntryIsPP partition idxroot pd s →
In indirection (getIndirections pd s) →
In partition (getPartitions multiplexer s) →
(defaultPage =? nextIndirection) = false →
StateLib.readPhyEntry indirection (StateLib.getIndexOfAddr vaToPrepare l) (memory s) = Some defaultPage →
noDupPartitionTree s →
nextIndirection ≠ indirection →
partitionDescriptorEntry s →
noDupConfigPagesList s →
isPresentNotDefaultIff s →
configTablesAreDifferent s →
consistency s →
dataStructurePdSh1Sh2asRoot PDidx
{|
currentPartition := currentPartition s;
memory := add indirection (StateLib.getIndexOfAddr vaToPrepare l)
(PE
{|
read := r;
write := w;
exec := e;
present := true;
user := true;
pa := nextIndirection |}) (memory s) beqPage beqIndex |}.
Lemma getIndirectionUpdateLastIndirectionSh1 lpred sstop s indirection va phySh1addr r w e entry :
∀ (stop : nat) (level : level),
let s' :=
{|
currentPartition := currentPartition s;
memory := add indirection (StateLib.getIndexOfAddr va (CLevel (level - sstop)))
(PE {| read := r; write := w; exec := e; present := true; user := true; pa := phySh1addr |})
(memory s) beqPage beqIndex |} in
∀ pd : page,
isWellFormedFstShadow lpred phySh1addr s' →
lookup indirection (StateLib.getIndexOfAddr va (CLevel (level - sstop))) (memory s) beqPage beqIndex =
Some (PE entry) →
¬ In indirection (getIndirectionsAux pd s sstop) →
(defaultPage =? phySh1addr) = false →
phySh1addr ≠ indirection →
getIndirection pd va level stop s' = Some indirection →
getIndirection pd va level sstop s = Some indirection →
level ≤ stop → indirection ≠ defaultPage → sstop ≥ level.
Lemma getIndirectionUpdateLastIndirectionSh2 lpred sstop s indirection va phySh1addr r w e entry :
∀ (stop : nat) (level : level),
let s' :=
{|
currentPartition := currentPartition s;
memory := add indirection (StateLib.getIndexOfAddr va (CLevel (level - sstop)))
(PE {| read := r; write := w; exec := e; present := true; user := true; pa := phySh1addr |})
(memory s) beqPage beqIndex |} in
∀ pd : page,
isWellFormedSndShadow lpred phySh1addr s' →
lookup indirection (StateLib.getIndexOfAddr va (CLevel (level - sstop))) (memory s) beqPage beqIndex =
Some (PE entry) →
¬ In indirection (getIndirectionsAux pd s sstop) →
(defaultPage =? phySh1addr) = false →
phySh1addr ≠ indirection →
getIndirection pd va level stop s' = Some indirection →
getIndirection pd va level sstop s = Some indirection →
level ≤ stop → indirection ≠ defaultPage → sstop ≥ level.
Lemma PCWellFormedRootDataStructSh1AddIndirection stop (level:level) phySh1addr idx s e w r
sstop vaToPrepare indirection lpred entry pd va :
let s':= {|
currentPartition := currentPartition s;
memory := add indirection (StateLib.getIndexOfAddr vaToPrepare (CLevel (level - sstop)))
(PE
{|
read := r;
write := w;
exec := e;
present := true;
user := true;
pa := phySh1addr |}) (memory s) beqPage beqIndex |} in
lookup indirection (StateLib.getIndexOfAddr vaToPrepare (CLevel (level - sstop)))
(memory s) beqPage beqIndex = Some (PE entry) →
isWellFormedFstShadow lpred phySh1addr s →
phySh1addr ≠ defaultPage →
phySh1addr ≠ indirection →
stop ≤ level →
false = StateLib.Level.eqb (CLevel (level - sstop)) fstLevel →
StateLib.Level.pred (CLevel (level - sstop)) = Some lpred →
getIndirection pd va level sstop s = Some indirection →
getIndirection pd va level sstop s' = getIndirection pd va level sstop s →
indirection ≠ defaultPage →
StateLib.getIndexOfAddr va (CLevel (level - sstop)) =
StateLib.getIndexOfAddr vaToPrepare (CLevel (level - sstop)) →
StateLib.readPhyEntry indirection (StateLib.getIndexOfAddr vaToPrepare (CLevel (level - sstop)))
(add indirection (StateLib.getIndexOfAddr vaToPrepare (CLevel (level - sstop)))
(PE {| read := r; write := w; exec := e; present := true; user := true; pa := phySh1addr |})
(memory s) beqPage beqIndex) = Some phySh1addr →
getIndirection pd va level stop s' = Some phySh1addr →
pd ≠ defaultPage →
stop > sstop →
PCWellFormedRootDataStruct stop level phySh1addr idx s' sh1idx.
NoDup (getIndirectionsAux pd s' nbLevel) (stop+1 = level+1 = nbLevel)
Lemma PCWellFormedRootDataStructSh2AddIndirection stop (level:level) phySh2addr idx s e w r
sstop vaToPrepare indirection lpred entry pd va :
let s':= {|
currentPartition := currentPartition s;
memory := add indirection (StateLib.getIndexOfAddr vaToPrepare (CLevel (level - sstop)))
(PE
{|
read := r;
write := w;
exec := e;
present := true;
user := true;
pa := phySh2addr |}) (memory s) beqPage beqIndex |} in
lookup indirection (StateLib.getIndexOfAddr vaToPrepare (CLevel (level - sstop)))
(memory s) beqPage beqIndex = Some (PE entry) →
isWellFormedSndShadow lpred phySh2addr s →
phySh2addr ≠ defaultPage →
phySh2addr ≠ indirection →
stop ≤ level →
false = StateLib.Level.eqb (CLevel (level - sstop)) fstLevel →
StateLib.Level.pred (CLevel (level - sstop)) = Some lpred →
getIndirection pd va level sstop s = Some indirection →
getIndirection pd va level sstop s' = getIndirection pd va level sstop s →
indirection ≠ defaultPage →
StateLib.getIndexOfAddr va (CLevel (level - sstop)) =
StateLib.getIndexOfAddr vaToPrepare (CLevel (level - sstop)) →
StateLib.readPhyEntry indirection (StateLib.getIndexOfAddr vaToPrepare (CLevel (level - sstop)))
(add indirection (StateLib.getIndexOfAddr vaToPrepare (CLevel (level - sstop)))
(PE {| read := r; write := w; exec := e; present := true; user := true; pa := phySh2addr |})
(memory s) beqPage beqIndex) = Some phySh2addr →
getIndirection pd va level stop s' = Some phySh2addr →
pd ≠ defaultPage →
stop > sstop →
PCWellFormedRootDataStruct stop level phySh2addr idx s' sh2idx.
NoDup (getIndirectionsAux pd s' nbLevel) (stop+1 = level+1 = nbLevel)
Lemma PCWellFormedRootDataStructAddIndirectionSh1 pd vaToPrepare (level lpred:level) sstop s indirection idx
va indirection0 stop phySh1addr r w e entry partition:
let s' := {|
currentPartition := currentPartition s;
memory := add indirection (StateLib.getIndexOfAddr vaToPrepare (CLevel (level - sstop)))
(PE
{| read := r; write := w; exec := e; present := true; user := true; pa := phySh1addr |})
(memory s) beqPage beqIndex |} in
NoDup (getIndirectionsAux pd s nbLevel) →
lookup indirection (StateLib.getIndexOfAddr vaToPrepare (CLevel (level - sstop)))
(memory s) beqPage beqIndex = Some (PE entry) →
isWellFormedFstShadow lpred phySh1addr s →
dataStructurePdSh1Sh2asRoot sh1idx s →
Some level = StateLib.getNbLevel →
In partition (getPartitions multiplexer s) →
getIndirection pd vaToPrepare level sstop s = Some indirection →
getIndirection pd va level stop s' = Some indirection0 →
stop ≤ nbLevel - 1 →
sstop ≤ level →
stop > sstop →
sstop > 0 →
indirection ≠ defaultPage →
false = StateLib.Level.eqb (CLevel (level - sstop)) fstLevel →
(defaultPage =? phySh1addr) = false →
StateLib.Level.pred (CLevel (level - sstop)) = Some lpred →
nextEntryIsPP partition sh1idx pd s →
indirection0 ≠ defaultPage →
pd ≠ defaultPage →
phySh1addr ≠ indirection →
PCWellFormedRootDataStruct stop level indirection0 idx s' sh1idx.
Lemma PCWellFormedRootDataStructAddIndirectionSh2 pd vaToPrepare (level lpred:level) sstop s indirection idx
va indirection0 stop phySh2addr r w e entry partition:
let s' := {|
currentPartition := currentPartition s;
memory := add indirection (StateLib.getIndexOfAddr vaToPrepare (CLevel (level - sstop)))
(PE
{| read := r; write := w; exec := e; present := true; user := true; pa := phySh2addr |})
(memory s) beqPage beqIndex |} in
NoDup (getIndirectionsAux pd s nbLevel) →
lookup indirection (StateLib.getIndexOfAddr vaToPrepare (CLevel (level - sstop)))
(memory s) beqPage beqIndex = Some (PE entry) →
isWellFormedSndShadow lpred phySh2addr s →
dataStructurePdSh1Sh2asRoot sh2idx s →
Some level = StateLib.getNbLevel →
In partition (getPartitions multiplexer s) →
getIndirection pd vaToPrepare level sstop s = Some indirection →
getIndirection pd va level stop s' = Some indirection0 →
stop ≤ nbLevel - 1 →
sstop ≤ level →
stop > sstop →
sstop > 0 →
indirection ≠ defaultPage →
false = StateLib.Level.eqb (CLevel (level - sstop)) fstLevel →
(defaultPage =? phySh2addr) = false →
StateLib.Level.pred (CLevel (level - sstop)) = Some lpred →
nextEntryIsPP partition sh2idx pd s →
indirection0 ≠ defaultPage →
pd ≠ defaultPage →
phySh2addr ≠ indirection →
PCWellFormedRootDataStruct stop level indirection0 idx s' sh2idx.
Lemma dataStructurePdSh1Sh2asRootSh1AddIndirection
s indirection nextIndirection idxroot entry nbLgen pd vaToPrepare partition l lpred r w e
phyPDChild phyMMUaddr phySh1Child phySh1addr phySh2Child phySh2addr :
dataStructurePdSh1Sh2asRoot sh1idx s→
nextIndirectionsOR indirection nextIndirection phyPDChild phyMMUaddr phySh1Child phySh1addr phySh2Child phySh2addr idxroot →
isWellFormedFstShadow lpred phySh1addr s →
StateLib.Level.pred l = Some lpred →
or3 idxroot →
lookup indirection (StateLib.getIndexOfAddr vaToPrepare l) (memory s) beqPage beqIndex = Some (PE entry) →
Some nbLgen = StateLib.getNbLevel →
indirectionDescription s partition indirection idxroot vaToPrepare l →
isWellFormedMMUTables phyMMUaddr s →
false = StateLib.Level.eqb l fstLevel →
nextEntryIsPP partition idxroot pd s →
In indirection (getIndirections pd s) →
In partition (getPartitions multiplexer s) →
(defaultPage =? nextIndirection) = false →
StateLib.readPhyEntry indirection (StateLib.getIndexOfAddr vaToPrepare l) (memory s) = Some defaultPage →
noDupPartitionTree s →
nextIndirection ≠ indirection →
partitionDescriptorEntry s →
noDupConfigPagesList s →
isPresentNotDefaultIff s →
configTablesAreDifferent s →
consistency s →
dataStructurePdSh1Sh2asRoot sh1idx
{|
currentPartition := currentPartition s;
memory := add indirection (StateLib.getIndexOfAddr vaToPrepare l)
(PE
{|
read := r;
write := w;
exec := e;
present := true;
user := true;
pa := nextIndirection |}) (memory s) beqPage beqIndex |}.
Lemma dataStructurePdSh1Sh2asRootSh2AddIndirection
s indirection nextIndirection idxroot entry nbLgen pd vaToPrepare partition l lpred r w e
phyPDChild phyMMUaddr phySh1Child phySh1addr phySh2Child phySh2addr :
dataStructurePdSh1Sh2asRoot sh2idx s→
nextIndirectionsOR indirection nextIndirection phyPDChild phyMMUaddr phySh1Child phySh1addr phySh2Child phySh2addr idxroot →
isWellFormedFstShadow lpred phySh1addr s →
StateLib.Level.pred l = Some lpred →
or3 idxroot →
lookup indirection (StateLib.getIndexOfAddr vaToPrepare l) (memory s) beqPage beqIndex = Some (PE entry) →
Some nbLgen = StateLib.getNbLevel →
indirectionDescription s partition indirection idxroot vaToPrepare l →
isWellFormedMMUTables phyMMUaddr s →
false = StateLib.Level.eqb l fstLevel →
nextEntryIsPP partition idxroot pd s →
In indirection (getIndirections pd s) →
In partition (getPartitions multiplexer s) →
(defaultPage =? nextIndirection) = false →
StateLib.readPhyEntry indirection (StateLib.getIndexOfAddr vaToPrepare l) (memory s) = Some defaultPage →
noDupPartitionTree s →
nextIndirection ≠ indirection →
partitionDescriptorEntry s →
noDupConfigPagesList s →
isPresentNotDefaultIff s →
configTablesAreDifferent s →
consistency s →
isWellFormedSndShadow lpred phySh2addr s →
dataStructurePdSh1Sh2asRoot sh2idx
{|
currentPartition := currentPartition s;
memory := add indirection (StateLib.getIndexOfAddr vaToPrepare l)
(PE
{|
read := r;
write := w;
exec := e;
present := true;
user := true;
pa := nextIndirection |}) (memory s) beqPage beqIndex |}.
Lemma currentPartitionInPartitionsListAddIndirection
s indirection nextIndirection idxroot entry nbLgen pd vaToPrepare partition l lpred r w e
phyPDChild phyMMUaddr phySh1Child phySh1addr phySh2Child phySh2addr :
nextIndirectionsOR indirection nextIndirection phyPDChild phyMMUaddr phySh1Child phySh1addr phySh2Child phySh2addr idxroot →
isWellFormedFstShadow lpred phySh1addr s →
StateLib.Level.pred l = Some lpred →
or3 idxroot →
lookup indirection (StateLib.getIndexOfAddr vaToPrepare l) (memory s) beqPage beqIndex = Some (PE entry) →
Some nbLgen = StateLib.getNbLevel →
indirectionDescription s partition indirection idxroot vaToPrepare l →
isWellFormedMMUTables phyMMUaddr s →
false = StateLib.Level.eqb l fstLevel →
nextEntryIsPP partition idxroot pd s →
In indirection (getIndirections pd s) →
StateLib.readPhyEntry indirection (StateLib.getIndexOfAddr vaToPrepare l) (memory s) = Some defaultPage →
noDupPartitionTree s →
nextIndirection ≠ indirection →
partitionDescriptorEntry s →
In partition (getPartitions multiplexer s) →
noDupConfigPagesList s →
isPresentNotDefaultIff s →
configTablesAreDifferent s →
(defaultPage =? nextIndirection) = false →
currentPartitionInPartitionsList s →
currentPartitionInPartitionsList
{|
currentPartition := currentPartition s;
memory := add indirection (StateLib.getIndexOfAddr vaToPrepare l)
(PE
{|
read := r;
write := w;
exec := e;
present := true;
user := true;
pa := nextIndirection |}) (memory s) beqPage beqIndex |}.
Lemma getMappedPagesAuxAddIndirectionEq s indirection nextIndirection entry nbLgen valist pd vaToPrepare partition l r w e root idxroot
phyPDChild phyMMUaddr phySh1Child phySh1addr phySh2Child phySh2addr:
or3 idxroot →
nextIndirectionsOR indirection nextIndirection phyPDChild phyMMUaddr phySh1Child phySh1addr phySh2Child phySh2addr idxroot →
lookup indirection (StateLib.getIndexOfAddr vaToPrepare l) (memory s) beqPage beqIndex = Some (PE entry) →
Some nbLgen = StateLib.getNbLevel →
indirectionDescription s partition indirection idxroot vaToPrepare l →
StateLib.readPhyEntry indirection (StateLib.getIndexOfAddr vaToPrepare l) (memory s) = Some defaultPage →
isWellFormedMMUTables phyMMUaddr s →
false = StateLib.Level.eqb l fstLevel →
noDupConfigPagesList s →
partitionDescriptorEntry s →
nextEntryIsPP partition idxroot root s →
In indirection (getIndirections root s) →
In partition (getPartitions multiplexer s) →
isPresentNotDefaultIff s →
configTablesAreDifferent s →
(defaultPage =? nextIndirection) = false →
nextEntryIsPP partition PDidx pd s →
nextIndirection ≠ indirection →
(getMappedPagesAux pd valist s) =
(getMappedPagesAux pd valist {|
currentPartition := currentPartition s;
memory := add indirection (StateLib.getIndexOfAddr vaToPrepare l)
(PE
{|
read := r;
write := w;
exec := e;
present := true;
user := true;
pa := nextIndirection |}) (memory s) beqPage beqIndex |}).
Lemma getMappedPagesAuxAddIndirectionSamePartEq s indirection nextIndirection entry nbLgen valist pd vaToPrepare partition l r w e
idxroot
phyPDChild phyMMUaddr phySh1Child phySh1addr phySh2Child phySh2addr root:
or3 idxroot →
nextIndirectionsOR indirection nextIndirection phyPDChild phyMMUaddr phySh1Child phySh1addr phySh2Child phySh2addr idxroot →
lookup indirection (StateLib.getIndexOfAddr vaToPrepare l) (memory s) beqPage beqIndex = Some (PE entry) →
Some nbLgen = StateLib.getNbLevel →
indirectionDescription s partition indirection idxroot vaToPrepare l →
StateLib.readPhyEntry indirection (StateLib.getIndexOfAddr vaToPrepare l) (memory s) = Some defaultPage →
isWellFormedMMUTables phyMMUaddr s →
false = StateLib.Level.eqb l fstLevel →
noDupConfigPagesList s →
nextEntryIsPP partition idxroot root s →
In indirection (getIndirections root s) →
partitionDescriptorEntry s →
In partition (getPartitions multiplexer s) →
isPresentNotDefaultIff s →
configTablesAreDifferent s →
(defaultPage =? nextIndirection) = false →
nextEntryIsPP partition PDidx pd s →
nextIndirection ≠ indirection →
(getMappedPagesAux pd valist s) =
(getMappedPagesAux pd valist {|
currentPartition := currentPartition s;
memory := add indirection (StateLib.getIndexOfAddr vaToPrepare l)
(PE
{|
read := r;
write := w;
exec := e;
present := true;
user := true;
pa := nextIndirection |}) (memory s) beqPage beqIndex |}).
Lemma getMappedPagesAddIndirectionSamePartEq s indirection nextIndirection entry nbLgen vaToPrepare partition l r w e
idxroot
phyPDChild phyMMUaddr phySh1Child phySh1addr phySh2Child phySh2addr root:
or3 idxroot →
nextIndirectionsOR indirection nextIndirection phyPDChild phyMMUaddr phySh1Child phySh1addr phySh2Child phySh2addr idxroot →
lookup indirection (StateLib.getIndexOfAddr vaToPrepare l) (memory s) beqPage beqIndex = Some (PE entry) →
Some nbLgen = StateLib.getNbLevel →
indirectionDescription s partition indirection idxroot vaToPrepare l →
StateLib.readPhyEntry indirection (StateLib.getIndexOfAddr vaToPrepare l) (memory s) = Some defaultPage →
isWellFormedMMUTables phyMMUaddr s →
false = StateLib.Level.eqb l fstLevel →
noDupConfigPagesList s →
nextEntryIsPP partition idxroot root s →
In indirection (getIndirections root s) →
partitionDescriptorEntry s →
In partition (getPartitions multiplexer s) →
isPresentNotDefaultIff s →
configTablesAreDifferent s →
(defaultPage =? nextIndirection) = false →
nextIndirection ≠ indirection →
(getMappedPages partition s)=
(getMappedPages partition {|
currentPartition := currentPartition s;
memory := add indirection (StateLib.getIndexOfAddr vaToPrepare l)
(PE
{|
read := r;
write := w;
exec := e;
present := true;
user := true;
pa := nextIndirection |}) (memory s) beqPage beqIndex |}).
Lemma noDupConfigPagesListAddIndirection
s indirection nextIndirection idxroot entry nbLgen root vaToPrepare partition l lpred r w e
phyPDChild phyMMUaddr phySh1Child phySh1addr phySh2Child phySh2addr :
nextIndirectionsOR indirection nextIndirection phyPDChild phyMMUaddr phySh1Child phySh1addr phySh2Child phySh2addr idxroot →
isWellFormedFstShadow lpred phySh1addr s →
StateLib.Level.pred l = Some lpred →
or3 idxroot →
lookup indirection (StateLib.getIndexOfAddr vaToPrepare l) (memory s) beqPage beqIndex = Some (PE entry) →
Some nbLgen = StateLib.getNbLevel →
indirectionDescription s partition indirection idxroot vaToPrepare l →
isWellFormedMMUTables phyMMUaddr s →
false = StateLib.Level.eqb l fstLevel →
nextEntryIsPP partition idxroot root s →
In indirection (getIndirections root s) →
StateLib.readPhyEntry indirection (StateLib.getIndexOfAddr vaToPrepare l) (memory s) = Some defaultPage →
noDupPartitionTree s →
nextIndirection ≠ indirection →
partitionDescriptorEntry s →
In partition (getPartitions multiplexer s) →
noDupConfigPagesList s →
isPresentNotDefaultIff s →
configTablesAreDifferent s →
(defaultPage =? nextIndirection) = false →
isWellFormedTables phyMMUaddr phySh1addr phySh2addr lpred s →
noDupConfigPagesList s →
noDupConfigPagesList
{|
currentPartition := currentPartition s;
memory := add indirection (StateLib.getIndexOfAddr vaToPrepare l)
(PE
{|
read := r;
write := w;
exec := e;
present := true;
user := true;
pa := nextIndirection |}) (memory s) beqPage beqIndex |}.
******* with induction ****
induction nbLevel;simpl;intros; try now contradict Hinind.
apply not_or_and in Hinindnot as (Hx & Hinindnot).
destruct Hinind as Hinind | Hinind;subst;try now contradict Hx.
apply NoDup_cons.
++
rewrite in_flat_map.
apply NoDup_cons_iff in Hnodup1.
destruct Hnodup1 as (Hnodup1 & Hnodup2).
unfold not;intros Hfalse.
destruct Hfalse as (x0 & Hx0 & Hx00).
contradict Hx00.
rewrite in_flat_map in Hnodup1.
contradict Hnodup1.
assert(Hor: x0 = nextIndirection \/ x0 <> nextIndirection) by apply pageDecOrNot.
destruct Hor as Hor | Hor.
subst.
rewrite in_flat_map in Hinindnot.
assert(Hkeyi: (getIndirectionsAux nextIndirection s' n) = nil). admit.
rewrite Hkeyi in *.
now contradict Hnodup1.
exists x0.
split.
clear Hnodup1.
eapply getTablePagesAddIndirection;try eassumption;trivial.
unfold s' in *.
eapply getIndirectionsAuxAddIndirectionSameStructure; try eassumption;trivial. intuition. ++ destruct Hi2 as Hi2 | Hi2. subst. admit. rewrite in_flat_map in Hi2. destruct Hi2 as (x1 & Hx1 & Hx11). assert((getTablePages pd tableSize s') = (getTablePages pd tableSize s)) by admit. rewrite H. clear H. admit.
Lemma consistencyAddIndirection
s indirection nextIndirection entry nbLgen pd idxroot
(vaToPrepare vaNextInd : vaddr) phyDescChild l
(currentPart currentPD ptMMUvaNextInd ptSh1VaNextInd: page) root r w e phyPDChild phyMMUaddr phySh1Child
phySh1addr phySh2Child phySh2addr lpred:
newIndirectionsAreNotMappedInChildrenAll s currentPart phyMMUaddr phySh1addr phySh2addr →
consistency s →
nextIndirectionsOR indirection nextIndirection phyPDChild phyMMUaddr phySh1Child
phySh1addr phySh2Child phySh2addr idxroot →
isWellFormedSndShadow lpred phySh1addr s →
StateLib.Level.pred l = Some lpred →
or3 idxroot →
(∀ parts, In parts (getPartitions multiplexer s) →
¬ In nextIndirection (getAccessibleMappedPages parts s)) →
kernelDataIsolation s →
initPEntryTablePreconditionToPropagatePreparePropertiesAll s phyMMUaddr phySh1addr phySh2addr →
lookup indirection (StateLib.getIndexOfAddr vaToPrepare l) (memory s) beqPage beqIndex = Some (PE entry) →
verticalSharing s →
In phyDescChild (getChildren currentPart s) →
Some nbLgen = StateLib.getNbLevel →
indirectionDescription s phyDescChild indirection idxroot vaToPrepare l →
StateLib.readPhyEntry indirection (StateLib.getIndexOfAddr vaToPrepare l) (memory s) = Some defaultPage→
isWellFormedMMUTables phyMMUaddr s →
false = StateLib.Level.eqb l fstLevel →
nextEntryIsPP phyDescChild PDidx pd s →
writeAccessibleRecPreparePostcondition currentPart nextIndirection s →
In currentPart (getPartitions multiplexer s) →
getTableAddrRoot ptMMUvaNextInd PDidx currentPart vaNextInd s→
isPE ptMMUvaNextInd (StateLib.getIndexOfAddr vaNextInd fstLevel) s→
entryUserFlag ptMMUvaNextInd (StateLib.getIndexOfAddr vaNextInd fstLevel) false s →
entryPresentFlag ptMMUvaNextInd (StateLib.getIndexOfAddr vaNextInd fstLevel) true s →
nextEntryIsPP currentPart PDidx currentPD s →
(defaultPage =? ptMMUvaNextInd) = false →
isEntryPage ptMMUvaNextInd (StateLib.getIndexOfAddr vaNextInd fstLevel) nextIndirection s →
(defaultPage =? ptSh1VaNextInd) = false →
getTableAddrRoot ptSh1VaNextInd sh1idx currentPart vaNextInd s →
isVE ptSh1VaNextInd (StateLib.getIndexOfAddr vaNextInd fstLevel) s →
noDupPartitionTree s →
nextIndirection ≠ indirection →
partitionDescriptorEntry s →
In phyDescChild (getPartitions multiplexer s) →
noDupConfigPagesList s →
isPresentNotDefaultIff s →
configTablesAreDifferent s →
(defaultPage =? nextIndirection) = false →
nextEntryIsPP phyDescChild idxroot root s →
In indirection (getIndirections root s)→
In indirection (getConfigPages phyDescChild s) →
isWellFormedTables phyMMUaddr phySh1addr phySh2addr lpred s →
consistency
{|
currentPartition := currentPartition s;
memory := add indirection (StateLib.getIndexOfAddr vaToPrepare l)
(PE
{|
read := r;
write := w;
exec := e;
present := true;
user := true;
pa := nextIndirection |}) (memory s) beqPage beqIndex |}.
Lemma insertEntryIntoLLPCAddIndirection indirection nextIndirection ptMMUTrdVA phySh2addr phySh1addr indMMUToPrepare ptMMUFstVA phyMMUaddr
phyPDChild currentShadow2 phySh2Child currentPD ptSh1TrdVA ptMMUSndVA
ptSh1SndVA ptSh1FstVA currentShadow1 descChildphy phySh1Child currentPart trdVA nextVA
vaToPrepare sndVA fstVA nbLgen l idxFstVA idxSndVA idxTrdVA zeroI lpred fstLL LLChildphy
lastLLTable e w r idxroot:
nextIndirectionsOR indirection nextIndirection phyPDChild phyMMUaddr phySh1Child phySh1addr phySh2Child phySh2addr idxroot→
or3 idxroot →
∀ s : state,
insertEntryIntoLLPC s ptMMUTrdVA phySh2addr phySh1addr indMMUToPrepare ptMMUFstVA phyMMUaddr
lastLLTable phyPDChild currentShadow2 phySh2Child currentPD ptSh1TrdVA ptMMUSndVA
ptSh1SndVA ptSh1FstVA currentShadow1 descChildphy phySh1Child currentPart trdVA nextVA
vaToPrepare sndVA fstVA nbLgen l idxFstVA idxSndVA idxTrdVA zeroI lpred fstLL LLChildphy
lastLLTable (CIndex (CIndex (CIndex (CIndex 3 - 1) - 1) - 1)) true →
insertEntryIntoLLPC
{|
currentPartition := currentPartition s;
memory := add indirection (StateLib.getIndexOfAddr vaToPrepare l)
(PE
{|
read := r;
write := w;
exec := e;
present := true;
user := true;
pa := nextIndirection |}) (memory s) beqPage beqIndex |} ptMMUTrdVA phySh2addr
phySh1addr phyMMUaddr ptMMUFstVA phyMMUaddr lastLLTable phyPDChild currentShadow2
phySh2Child currentPD ptSh1TrdVA ptMMUSndVA ptSh1SndVA ptSh1FstVA currentShadow1
descChildphy phySh1Child currentPart trdVA nextVA vaToPrepare sndVA fstVA nbLgen l
idxFstVA idxSndVA idxTrdVA zeroI lpred fstLL LLChildphy lastLLTable
(CIndex (CIndex (CIndex (CIndex 3 - 1) - 1) - 1)) false.
Lemma writePhyEntryAddIndirection ptMMUTrdVA phySh2addr phySh1addr indMMUToPrepare ptMMUFstVA
phyMMUaddr phyPDChild currentShadow2 phySh2Child currentPD ptSh1TrdVA
ptMMUSndVA ptSh1SndVA ptSh1FstVA currentShadow1 descChildphy phySh1Child currentPart
trdVA nextVA vaToPrepare sndVA fstVA nbLgen l idxFstVA idxSndVA idxTrdVA zeroI lpred
fstLL LLChildphy lastLLTable idxToPrepare :
{{ fun s : state ⇒
insertEntryIntoLLPC s ptMMUTrdVA phySh2addr phySh1addr indMMUToPrepare ptMMUFstVA
phyMMUaddr lastLLTable phyPDChild currentShadow2 phySh2Child currentPD ptSh1TrdVA
ptMMUSndVA ptSh1SndVA ptSh1FstVA currentShadow1 descChildphy phySh1Child currentPart
trdVA nextVA vaToPrepare sndVA fstVA nbLgen l idxFstVA idxSndVA idxTrdVA zeroI lpred
fstLL LLChildphy lastLLTable (CIndex (CIndex (CIndex (CIndex 3 - 1) - 1) - 1)) true}}
MAL.writePhyEntry phyPDChild idxToPrepare phyMMUaddr true true true true true
{{ fun _ s ⇒ insertEntryIntoLLPC s ptMMUTrdVA phySh2addr phySh1addr phyMMUaddr ptMMUFstVA
phyMMUaddr lastLLTable phyPDChild currentShadow2 phySh2Child currentPD ptSh1TrdVA
ptMMUSndVA ptSh1SndVA ptSh1FstVA currentShadow1 descChildphy phySh1Child currentPart
trdVA nextVA vaToPrepare sndVA fstVA nbLgen l idxFstVA idxSndVA idxTrdVA zeroI lpred
fstLL LLChildphy lastLLTable (CIndex (CIndex (CIndex (CIndex 3 - 1) - 1) - 1)) false}}.
s indirection nextIndirection entry nbLgen pd idxroot
(vaToPrepare vaNextInd : vaddr) phyDescChild l
(currentPart currentPD ptMMUvaNextInd ptSh1VaNextInd: page) root r w e phyPDChild phyMMUaddr phySh1Child
phySh1addr phySh2Child phySh2addr lpred:
newIndirectionsAreNotMappedInChildrenAll s currentPart phyMMUaddr phySh1addr phySh2addr →
consistency s →
nextIndirectionsOR indirection nextIndirection phyPDChild phyMMUaddr phySh1Child
phySh1addr phySh2Child phySh2addr idxroot →
isWellFormedSndShadow lpred phySh1addr s →
StateLib.Level.pred l = Some lpred →
or3 idxroot →
(∀ parts, In parts (getPartitions multiplexer s) →
¬ In nextIndirection (getAccessibleMappedPages parts s)) →
kernelDataIsolation s →
initPEntryTablePreconditionToPropagatePreparePropertiesAll s phyMMUaddr phySh1addr phySh2addr →
lookup indirection (StateLib.getIndexOfAddr vaToPrepare l) (memory s) beqPage beqIndex = Some (PE entry) →
verticalSharing s →
In phyDescChild (getChildren currentPart s) →
Some nbLgen = StateLib.getNbLevel →
indirectionDescription s phyDescChild indirection idxroot vaToPrepare l →
StateLib.readPhyEntry indirection (StateLib.getIndexOfAddr vaToPrepare l) (memory s) = Some defaultPage→
isWellFormedMMUTables phyMMUaddr s →
false = StateLib.Level.eqb l fstLevel →
nextEntryIsPP phyDescChild PDidx pd s →
writeAccessibleRecPreparePostcondition currentPart nextIndirection s →
In currentPart (getPartitions multiplexer s) →
getTableAddrRoot ptMMUvaNextInd PDidx currentPart vaNextInd s→
isPE ptMMUvaNextInd (StateLib.getIndexOfAddr vaNextInd fstLevel) s→
entryUserFlag ptMMUvaNextInd (StateLib.getIndexOfAddr vaNextInd fstLevel) false s →
entryPresentFlag ptMMUvaNextInd (StateLib.getIndexOfAddr vaNextInd fstLevel) true s →
nextEntryIsPP currentPart PDidx currentPD s →
(defaultPage =? ptMMUvaNextInd) = false →
isEntryPage ptMMUvaNextInd (StateLib.getIndexOfAddr vaNextInd fstLevel) nextIndirection s →
(defaultPage =? ptSh1VaNextInd) = false →
getTableAddrRoot ptSh1VaNextInd sh1idx currentPart vaNextInd s →
isVE ptSh1VaNextInd (StateLib.getIndexOfAddr vaNextInd fstLevel) s →
noDupPartitionTree s →
nextIndirection ≠ indirection →
partitionDescriptorEntry s →
In phyDescChild (getPartitions multiplexer s) →
noDupConfigPagesList s →
isPresentNotDefaultIff s →
configTablesAreDifferent s →
(defaultPage =? nextIndirection) = false →
nextEntryIsPP phyDescChild idxroot root s →
In indirection (getIndirections root s)→
In indirection (getConfigPages phyDescChild s) →
isWellFormedTables phyMMUaddr phySh1addr phySh2addr lpred s →
consistency
{|
currentPartition := currentPartition s;
memory := add indirection (StateLib.getIndexOfAddr vaToPrepare l)
(PE
{|
read := r;
write := w;
exec := e;
present := true;
user := true;
pa := nextIndirection |}) (memory s) beqPage beqIndex |}.
Lemma insertEntryIntoLLPCAddIndirection indirection nextIndirection ptMMUTrdVA phySh2addr phySh1addr indMMUToPrepare ptMMUFstVA phyMMUaddr
phyPDChild currentShadow2 phySh2Child currentPD ptSh1TrdVA ptMMUSndVA
ptSh1SndVA ptSh1FstVA currentShadow1 descChildphy phySh1Child currentPart trdVA nextVA
vaToPrepare sndVA fstVA nbLgen l idxFstVA idxSndVA idxTrdVA zeroI lpred fstLL LLChildphy
lastLLTable e w r idxroot:
nextIndirectionsOR indirection nextIndirection phyPDChild phyMMUaddr phySh1Child phySh1addr phySh2Child phySh2addr idxroot→
or3 idxroot →
∀ s : state,
insertEntryIntoLLPC s ptMMUTrdVA phySh2addr phySh1addr indMMUToPrepare ptMMUFstVA phyMMUaddr
lastLLTable phyPDChild currentShadow2 phySh2Child currentPD ptSh1TrdVA ptMMUSndVA
ptSh1SndVA ptSh1FstVA currentShadow1 descChildphy phySh1Child currentPart trdVA nextVA
vaToPrepare sndVA fstVA nbLgen l idxFstVA idxSndVA idxTrdVA zeroI lpred fstLL LLChildphy
lastLLTable (CIndex (CIndex (CIndex (CIndex 3 - 1) - 1) - 1)) true →
insertEntryIntoLLPC
{|
currentPartition := currentPartition s;
memory := add indirection (StateLib.getIndexOfAddr vaToPrepare l)
(PE
{|
read := r;
write := w;
exec := e;
present := true;
user := true;
pa := nextIndirection |}) (memory s) beqPage beqIndex |} ptMMUTrdVA phySh2addr
phySh1addr phyMMUaddr ptMMUFstVA phyMMUaddr lastLLTable phyPDChild currentShadow2
phySh2Child currentPD ptSh1TrdVA ptMMUSndVA ptSh1SndVA ptSh1FstVA currentShadow1
descChildphy phySh1Child currentPart trdVA nextVA vaToPrepare sndVA fstVA nbLgen l
idxFstVA idxSndVA idxTrdVA zeroI lpred fstLL LLChildphy lastLLTable
(CIndex (CIndex (CIndex (CIndex 3 - 1) - 1) - 1)) false.
Lemma writePhyEntryAddIndirection ptMMUTrdVA phySh2addr phySh1addr indMMUToPrepare ptMMUFstVA
phyMMUaddr phyPDChild currentShadow2 phySh2Child currentPD ptSh1TrdVA
ptMMUSndVA ptSh1SndVA ptSh1FstVA currentShadow1 descChildphy phySh1Child currentPart
trdVA nextVA vaToPrepare sndVA fstVA nbLgen l idxFstVA idxSndVA idxTrdVA zeroI lpred
fstLL LLChildphy lastLLTable idxToPrepare :
{{ fun s : state ⇒
insertEntryIntoLLPC s ptMMUTrdVA phySh2addr phySh1addr indMMUToPrepare ptMMUFstVA
phyMMUaddr lastLLTable phyPDChild currentShadow2 phySh2Child currentPD ptSh1TrdVA
ptMMUSndVA ptSh1SndVA ptSh1FstVA currentShadow1 descChildphy phySh1Child currentPart
trdVA nextVA vaToPrepare sndVA fstVA nbLgen l idxFstVA idxSndVA idxTrdVA zeroI lpred
fstLL LLChildphy lastLLTable (CIndex (CIndex (CIndex (CIndex 3 - 1) - 1) - 1)) true}}
MAL.writePhyEntry phyPDChild idxToPrepare phyMMUaddr true true true true true
{{ fun _ s ⇒ insertEntryIntoLLPC s ptMMUTrdVA phySh2addr phySh1addr phyMMUaddr ptMMUFstVA
phyMMUaddr lastLLTable phyPDChild currentShadow2 phySh2Child currentPD ptSh1TrdVA
ptMMUSndVA ptSh1SndVA ptSh1FstVA currentShadow1 descChildphy phySh1Child currentPart
trdVA nextVA vaToPrepare sndVA fstVA nbLgen l idxFstVA idxSndVA idxTrdVA zeroI lpred
fstLL LLChildphy lastLLTable (CIndex (CIndex (CIndex (CIndex 3 - 1) - 1) - 1)) false}}.