Library Pip.Model.IAL
Require Import Pip.Model.ADT Pip.Model.Lib Pip.Model.Hardware Pip.Model.MALInternal Pip.Model.MAL.
Require Import Bool Arith List.
Import List.ListNotations.
Module Vint.
Definition ltb (a b : vint) : LLI bool := ret (a <? b).
End Vint.
The 'getMaxVint' function returns the maximum interruption level
Definition getMaxVint : LLI vint:=
ret maxVint.
Definition checkIndexPropertyLTB (userIndex : userValue) : LLI bool :=
ret (Nat.ltb userIndex tableSize).
Definition checkVidtIndex (saveIndex : index) : LLI bool :=
ret (saveIndex <=? maxVint).
Program Definition userValueToIndex (userIndex : userValue) : LLI index :=
if lt_dec userIndex tableSize
then
ret (Build_index userIndex _ )
else undefined 85.
Definition FAIL_INVALID_INT_LEVEL := FAIL_INVALID_INT_LEVEL_Cons.
Definition FAIL_INVALID_CTX_SAVE_INDEX := FAIL_INVALID_CTX_SAVE_INDEX_Cons.
Definition FAIL_CALLER_CONTEXT_SAVE := FAIL_CALLER_CONTEXT_SAVE_Cons.
Definition FAIL_UNAVAILABLE_TARGET_VIDT := FAIL_UNAVAILABLE_TARGET_VIDT_Cons.
Definition FAIL_UNAVAILABLE_TARGET_CTX := FAIL_UNAVAILABLE_TARGET_CTX_Cons.
Definition FAIL_UNAVAILABLE_CALLER_VIDT := FAIL_UNAVAILABLE_CALLER_VIDT_Cons.
Definition FAIL_ROOT_CALLER := FAIL_ROOT_CALLER_Cons.
Definition FAIL_INVALID_CHILD := FAIL_INVALID_CHILD_Cons.
Definition FAIL_MASKED_INTERRUPT := FAIL_MASKED_INTERRUPT_Cons.
Definition SUCCESS := SUCCESS_Cons.
Definition loadContext (contextToLoad : contextAddr) (enforce_interrupt : bool) : LLI unit :=
ret tt.
Definition contextSizeMinusOne := contextSize-1.
Definition setInterruptMask (mask : interruptMask) : LLI unit :=
ret tt.
Definition readInterruptMask (childVidt : page) : LLI interruptMask :=
ret int_mask_d.
Definition isInterruptMasked (intMask : interruptMask) (interrupt : vint) : LLI bool :=
ret false.
Definition vaddrToContextAddr (va : vaddr) : LLI contextAddr :=
ret 0.
Definition writeContext (callingContextAddr : contextAddr) (contextSaveAddr : vaddr) (flagsOnWake : interruptMask)
: LLI unit := ret tt.
Definition updateMMURoot(pageDir : page)
: LLI unit := ret tt.
Definition getNthVAddrFrom (start : vaddr) (range : nat) : LLI vaddr :=
ret (getNthVAddrFromAux start range).
Definition getInterruptMaskFromCtx (context : contextAddr) : LLI interruptMask :=
ret int_mask_d.
Definition noInterruptRequest (flags : interruptMask) : LLI bool :=
ret true.
Program Definition firstVAddrGreaterThanSecond (first second : vaddr) : LLI bool :=
ret (firstVAddrGreaterThanSecondAux first second _).
ret maxVint.
Definition checkIndexPropertyLTB (userIndex : userValue) : LLI bool :=
ret (Nat.ltb userIndex tableSize).
Definition checkVidtIndex (saveIndex : index) : LLI bool :=
ret (saveIndex <=? maxVint).
Program Definition userValueToIndex (userIndex : userValue) : LLI index :=
if lt_dec userIndex tableSize
then
ret (Build_index userIndex _ )
else undefined 85.
Definition FAIL_INVALID_INT_LEVEL := FAIL_INVALID_INT_LEVEL_Cons.
Definition FAIL_INVALID_CTX_SAVE_INDEX := FAIL_INVALID_CTX_SAVE_INDEX_Cons.
Definition FAIL_CALLER_CONTEXT_SAVE := FAIL_CALLER_CONTEXT_SAVE_Cons.
Definition FAIL_UNAVAILABLE_TARGET_VIDT := FAIL_UNAVAILABLE_TARGET_VIDT_Cons.
Definition FAIL_UNAVAILABLE_TARGET_CTX := FAIL_UNAVAILABLE_TARGET_CTX_Cons.
Definition FAIL_UNAVAILABLE_CALLER_VIDT := FAIL_UNAVAILABLE_CALLER_VIDT_Cons.
Definition FAIL_ROOT_CALLER := FAIL_ROOT_CALLER_Cons.
Definition FAIL_INVALID_CHILD := FAIL_INVALID_CHILD_Cons.
Definition FAIL_MASKED_INTERRUPT := FAIL_MASKED_INTERRUPT_Cons.
Definition SUCCESS := SUCCESS_Cons.
Definition loadContext (contextToLoad : contextAddr) (enforce_interrupt : bool) : LLI unit :=
ret tt.
Definition contextSizeMinusOne := contextSize-1.
Definition setInterruptMask (mask : interruptMask) : LLI unit :=
ret tt.
Definition readInterruptMask (childVidt : page) : LLI interruptMask :=
ret int_mask_d.
Definition isInterruptMasked (intMask : interruptMask) (interrupt : vint) : LLI bool :=
ret false.
Definition vaddrToContextAddr (va : vaddr) : LLI contextAddr :=
ret 0.
Definition writeContext (callingContextAddr : contextAddr) (contextSaveAddr : vaddr) (flagsOnWake : interruptMask)
: LLI unit := ret tt.
Definition updateMMURoot(pageDir : page)
: LLI unit := ret tt.
Definition getNthVAddrFrom (start : vaddr) (range : nat) : LLI vaddr :=
ret (getNthVAddrFromAux start range).
Definition getInterruptMaskFromCtx (context : contextAddr) : LLI interruptMask :=
ret int_mask_d.
Definition noInterruptRequest (flags : interruptMask) : LLI bool :=
ret true.
Program Definition firstVAddrGreaterThanSecond (first second : vaddr) : LLI bool :=
ret (firstVAddrGreaterThanSecondAux first second _).