Library Pip.Proof.Consistency

• Summary
  • The dataStructurePdSh1Sh2asRoot property defines the type of different values
  • The currentPartitionInPartitionsList property specifies that the
  • The currentPartitionIsNotDefaultPage t property specifies that the
  • The parentInPartitionList property specifies that the parent of a given
  • The partitionDescriptorEntry defines some properties of the partition descriptor.
  • The multiplexerWithoutParent specifies that the multiplexer is the root of
  • The noDupMappedPagesList requires that mapped pages of a single partition
  • The noDupConfigPagesList requires that configuation tables of
  • The accessibleVAIsNotPartitionDescriptor requires that accessible virtual
  • The accessibleChildPageIsAccessibleIntoParent requires that all accessible physical
  • The noCycleInPartitionTree requires that a partition and
  • The configTablesAreDifferent requires that configuation tables of different
  • The isChild specifies that a given partition should be a child of the
  • The isParent specifies that if we take any child into the children list of any
  • The isPresentNotDefaultIff specifies that if the present flag of a physical
  • The physicalPageNotDerived specifies that if a given physical
  • Conjunction of all consistency properties

Library Pip.Proof.DependentTypeLemmas

• Summary

Library Pip.Proof.InternalLemmas2

• Summary

Library Pip.Proof.InternalLemmas

• Summary

Library Pip.Proof.Isolation

• Summary

Library Pip.Proof.Lib

• Summary

Library Pip.Proof.rushby

Library Pip.Proof.StateLib

• Summary

Library Pip.Proof.WeakestPreconditions

• Summary

Library Pip.Proof.invariants.AddVAddr

• Summary

Library Pip.Proof.invariants.CheckChild

• Summary

Library Pip.Proof.invariants.Collect

• Summary

Library Pip.Proof.invariants.CountToMap

• Summary

Library Pip.Proof.invariants.CreatePartition

• Summary

Library Pip.Proof.invariants.DeletePartition

• Summary

Library Pip.Proof.invariants.GetTableAddr

• Summary

Library Pip.Proof.invariants.InitConfigPagesList

• Summary

Library Pip.Proof.invariants.InitFstShadow

• Summary

Library Pip.Proof.invariants.InitPEntryTable

• Summary

Library Pip.Proof.invariants.InitSndShadow

• Summary

Library Pip.Proof.invariants.InitVAddrTable

• Summary

Library Pip.Proof.invariants.InitVEntryTable

• Summary

Library Pip.Proof.invariants.InsertEntryIntoLL

• Summary

Library Pip.Proof.invariants.Invariants

• Summary

Library Pip.Proof.invariants.IWritePhysical

• Summary

Library Pip.Proof.invariants.LinkedListConfig

• Summary

Library Pip.Proof.invariants.mapInChild

• Summary

Library Pip.Proof.invariants.MapMMUPage

• Summary

Library Pip.Proof.invariants.Prepare

• Summary

Library Pip.Proof.invariants.PropagatedProperties

Library Pip.Proof.invariants.RemoveVAddr

• Summary

Library Pip.Proof.invariants.updateCurPartition

• Summary

Library Pip.Proof.invariants.UpdateMappedPageContent

• Summary

Library Pip.Proof.invariants.UpdatePartitionDescriptor

• Summary

Library Pip.Proof.invariants.UpdatePDFlagTrue

• all physical pages are not config pages (already into hypothesis)
• all physical pages are not mapped into any child
• all physical pages are not config pages (already into hypothesis)
• all physical pages are not config pages (already into hypothesis)
• all physical pages are not mapped into any child
• all physical pages are not config pages (already into hypothesis)

Library Pip.Proof.invariants.UpdateShadow1StructurePrepare

• Summary

Library Pip.Proof.invariants.UpdateShadow1Structure

• Summary

Library Pip.Proof.invariants.UpdateShadow2Structure

• Summary

Library Pip.Proof.invariants.WriteAccessibleFalse

• Summary

Library Pip.Proof.invariants.WriteAccessibleRecPrepare

• Summary

Library Pip.Proof.invariants.WriteAccessibleRec

• Summary

Library Pip.Proof.invariants.WriteAccessible

• Summary

Library Pip.Proof.invariants.WriteIndex

• Summary

Library Pip.Proof.invariants.WritePEntryRemoveVaddr

Library Pip.Proof.invariants.WritePhyEntryPrepareProperties

• Summary
  • eapply getTablePagesAddIndirection;try eassumption;trivial.
  • unfold s' in *.

Library Pip.Proof.invariants.WritePhyEntryPrepare

• Summary

Library Pip.Proof.invariants.WritePhyEntry

• Summary

Library Pip.Proof.invariants.writePhysical

• Summary

Library Pip.Core.Internal

• Summary

Library Pip.Core.Services

• Summary
  • The createPartition PIP service
  • The countToMap PIP service
  • The prepare PIP service
  • The addVAddr PIP service
  • The removeVAddr PIP service
  • The deletePartition PIP service
  • The collect PIP service

Library Pip.Model.ADT

• Summary

Library Pip.Model.Hardware

• Summary
  • The type constructor "LLI"
  • Two operations : "bind" to compose a sequence of monadic functions
  • "get" to get back the current state
  • "put" to update the current state
  • "m" is a monadic function
  • "P" is the precondition of the function "m", it is an unary predicate
  • "Q" is the postcondition of the function "m", it is a binary predicate

Library Pip.Model.IAL

Library Pip.Model.Lib

• Summary

Library Pip.Model.MALInternal

• Summary

Library Pip.Model.MAL

• Summary

Library Pip.Model.MMU

• Summary

Library Pip.Model.Simulation