From 8512e742a62c2bcde73186c92eb045505b4e88c8 Mon Sep 17 00:00:00 2001
From: Andrew Baumann <Andrew.Baumann@microsoft.com>
Date: Thu, 5 Oct 2017 20:31:44 -0700
Subject: [PATCH] final tidying

---
 verified/exhandler_state.i.dfy | 8 ++++----
 verified/main.dfy              | 4 ++--
 2 files changed, 6 insertions(+), 6 deletions(-)

diff --git a/verified/exhandler_state.i.dfy b/verified/exhandler_state.i.dfy
index 9884a7f..4eff808 100644
--- a/verified/exhandler_state.i.dfy
+++ b/verified/exhandler_state.i.dfy
@@ -167,7 +167,8 @@ lemma lemma_SVCFIQNestedExceptionIsCorrect(s0:state, s1:state, s2:state, r:state
     ensures mode_of_state(s2) != User && SaneMem(s2.m)
     ensures priv_of_mode(spsr_of_state(s2).m) == PL1
     ensures exists p0, dp:PageNr :: validPageDb(p0) && pageDbCorresponds(s2.m, p0)
-        && finalDispatcher(p0, dp) && KomInterruptHandlerInvariant(s2, p0, r, dp)
+            && finalDispatcher(p0, dp) && KomExceptionHandlerInvariant(s2, p0, r, dp)
+    ensures !evalOBool(r, OCmp(OTstEq, OSP, OConst(1)))
 {
     var pagedb, dispPg := lemma_UsermodeContinuationPreconditionDef(s0);
     lemma_PrivExceptionStateSideEffects(s1, s2, ExFIQ, pagedb, dispPg);
@@ -175,7 +176,6 @@ lemma lemma_SVCFIQNestedExceptionIsCorrect(s0:state, s1:state, s2:state, r:state
     var block := va_CCons(exHandler(ExFIQ), va_CNil());
     assert va_eval(Block(block), s2, r) by { assert evalBlock(block, s2, r); }
     var _, _, _ := va_lemma_interrupt_handler(block, s2, r, ExFIQ, s1, pagedb, dispPg);
-    assert KomInterruptHandlerInvariant(s2, pagedb, r, dispPg);
 }
 
 lemma lemma_PrivModeExceptionHandlersAreCorrect(s0:state, ex:exception, s1:state, r:state)
@@ -189,7 +189,7 @@ lemma lemma_PrivModeExceptionHandlersAreCorrect(s0:state, ex:exception, s1:state
     ensures mode_of_state(s1) != User && SaneMem(s1.m)
     ensures priv_of_mode(spsr_of_state(s1).m) == PL1
     ensures spsr_of_state(s1).m != Supervisor
-    ensures exists p0, dp:PageNr :: KomInterruptHandlerInvariant(s1, p0, r, dp)
+    ensures KomInterruptHandlerInvariant(s1, r)
 {
     var pagedb, dispPg := lemma_UsermodeContinuationPreconditionDef(s0);
     lemma_PrivExceptionStateSideEffects(s0, s1, ex, pagedb, dispPg);
@@ -198,5 +198,5 @@ lemma lemma_PrivModeExceptionHandlersAreCorrect(s0:state, ex:exception, s1:state
     assert va_eval(Block(block), s1, r) by { assert evalBlock(block, s1, r); }
     var dummy:state :| true; // irrelevant
     var _, _, _ := va_lemma_interrupt_handler(block, s1, r, ex, dummy, pagedb, dispPg);
-    assert KomInterruptHandlerInvariant(s1, pagedb, r, dispPg);
+    assert KomInterruptHandlerInvariant(s1, r);
 }
diff --git a/verified/main.dfy b/verified/main.dfy
index c9523d9..788f02c 100644
--- a/verified/main.dfy
+++ b/verified/main.dfy
@@ -30,7 +30,7 @@ method Main()
         && (ex == ExFIQ || ex == ExIRQ)
         && evalExceptionTaken(s0, ex, nondet_word(s0.conf.nondet, NONDET_PC()), s1)
         && evalCode(exHandler(ex), s1, r)
-        ensures exists p0, dp :: KomInterruptHandlerInvariant(s1, p0, r, dp)
+        ensures KomInterruptHandlerInvariant(s1, r)
     { lemma_PrivModeExceptionHandlersAreCorrect(s0, ex, s1, r); }
 
     // prove the special-case User -> SVC -> FIQ nested interrupt path
@@ -41,7 +41,7 @@ method Main()
         && (exists upc:word :: evalExceptionTaken(s0, ExSVC, upc, s1))
         && evalExceptionTaken(s1, ExFIQ, nondet_word(s1.conf.nondet, NONDET_PC()), s2)
         && evalCode(exHandler(ExFIQ), s2, r)
-        ensures exists p0, dp :: KomInterruptHandlerInvariant(s2, p0, r, dp)
+        ensures exists p0, dp :: KomExceptionHandlerInvariant(s2, p0, r, dp)
     { lemma_SVCFIQNestedExceptionIsCorrect(s0, s1, s2, r); }
 
     printAll();