lh-l4v

Author	SHA1	Message	Date
Rafal Kolanski	3a77d097c4	aarch64 refine: first pass through IpcCancel_R needed some changes to Schedule_R and VSpace_R Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>	2023-05-26 18:04:43 +10:00
Rafal Kolanski	904056868d	aarch64 refine: add state_hyp_refs_of' to valid_state' Somehow we missed this on the first pass. Adjusted existing proofs. Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>	2023-05-26 18:04:42 +10:00
Rafal Kolanski	a79e06f419	aarch64 refine: first run through VSpace_R This required a lot of adaptation from ARM_HYP, rearranging, and fixing. The VCPU lemmas are mostly now constrained to one area, making it theoretically possible to make a VCPU theory in the future. Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>	2023-05-26 18:04:42 +10:00
Rafal Kolanski	97ebd07298	aarch64 refine: start on VSpace_R Up to and including handleVMFault_corres which needed a major overhaul. Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>	2023-05-26 18:04:42 +10:00