Gerwin Klein 24c0c5c390 spec+proof: use generated config constants ... This includes replacing previous ASpec names for such constants with the names used in Haskell/ExecSpec to avoid duplication. This also makes some of the proofs slightly more generic. Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>		2021-12-23 14:54:13 +11:00
..
ArchADT_IF.thy	various: resolve some new fixmes	2021-11-12 09:39:16 +11:00
ArchArch_IF.thy	various: resolve some new fixmes	2021-11-12 09:39:16 +11:00
ArchCNode_IF.thy	arm infoflow: update proofs	2021-11-12 09:39:16 +11:00
ArchDecode_IF.thy	infoflow: Decode arch split	2021-10-05 08:46:11 +11:00
ArchFinalCaps.thy	infoflow: FinalCaps arch split	2021-10-05 08:46:11 +11:00
ArchFinalise_IF.thy	various: resolve some new fixmes	2021-11-12 09:39:16 +11:00
ArchIRQMasks_IF.thy	infoflow: IRQMasks arch split	2021-10-05 08:46:11 +11:00
ArchInfoFlow.thy	infoflow: InfoFlow arch split	2021-10-05 08:46:11 +11:00
ArchInfoFlow_IF.thy	infoflow: InfoFlow arch split	2021-10-05 08:46:11 +11:00
ArchInterrupt_IF.thy	infoflow: replace valid_ko_at_arch with valid_arch_state	2021-10-05 08:46:11 +11:00
ArchIpc_IF.thy	infoflow: replace valid_ko_at_arch with valid_arch_state	2021-10-05 08:46:11 +11:00
ArchNoninterference.thy	various: resolve some new fixmes	2021-11-12 09:39:16 +11:00
ArchPasUpdates.thy	infoflow: PasUpdates arch split	2021-10-05 08:46:11 +11:00
ArchRetype_IF.thy	spec+proof: use generated config constants	2021-12-23 14:54:13 +11:00
ArchScheduler_IF.thy	infoflow: replace valid_ko_at_arch with valid_arch_state	2021-10-05 08:46:11 +11:00
ArchSyscall_IF.thy	arm infoflow: update proofs	2021-11-12 09:39:16 +11:00
ArchTcb_IF.thy	infoflow: replace valid_ko_at_arch with valid_arch_state	2021-10-05 08:46:11 +11:00
ArchUserOp_IF.thy	arm infoflow: update proofs	2021-11-12 09:39:16 +11:00
Example_Valid_State.thy	infoflow: remove dependency on domains > 1	2021-12-22 23:50:22 +11:00