strengthen EssentialInterruptContinuationInvariantProperties, nix assume

* have EssentialInterruptContinuationInvariantProperties require the
   continuation to leave the bottom bit of SP clear, in agreement with
   the special-case return path from printInterruptHandlerReturn()
   (otherwise it returns to the usermode continuation)

 * use this in a proof, so that if the handler returned with the
   original (sane) SP, then we can't have taken a FIQ from supervisor
   mode

still not entirely comfortable with this approach, but it's probably
close to the best we can do given that the control flow is all in
trusted code anyway

verified/ARMdef.s.dfy

@@ -686,14 +686,19 @@ function havocUserRegs(nondet:int, us:UserState, regs:map<ARMReg, word>): map<AR
 // To be defined/established by "application" code (i.e. komodo exception handlers)
 // XXX: for soundness, application must prove the essential properties
 
+// essential properties for the usermode continuation (must return)
 predicate EssentialContinuationInvariantProperties(s:state, r:state)
 {
     (ValidState(s) ==> ValidState(r)) && (s.ok ==> r.ok)
 }
 
+// essential properties for the interrupt-handler continuation (might not return)
 predicate EssentialInterruptContinuationInvariantProperties(s:state, r:state)
 {
     EssentialContinuationInvariantProperties(s, r) && !interrupts_enabled(r)
+    // this is needed for the special-case return in printInterruptHandlerReturn
+    // (the continuation only returns if SP & 1 == 0)
+    && (ValidState(r) && r.ok ==> evalOBool(r, OCmp(OTstEq, OSP, OConst(1))))
 }
 
 predicate {:axiom} UsermodeContinuationPrecondition(s:state)
@@ -714,7 +719,7 @@ predicate {:axiom} InterruptContinuationInvariant(s:state, r:state)
         // B1.8.3 "Link values saved on exception entry"
         // these are necessary to get MOVS PC, LR to restore the same PC
         // (this is needed here, because we don't model the PC explicitly)
-        && OperandContents(r, OLR) == TruncateWord(OperandContents(s, OLR) - 4))
+        && (ValidState(r) ==> OperandContents(r, OLR) == TruncateWord(OperandContents(s, OLR) - 4)))
 
 //-----------------------------------------------------------------------------
 // Model of page tables for userspace execution
@@ -1055,7 +1060,7 @@ function evalOBool(s:state, o:obool):bool
 predicate evalGuard(s:state, o:obool, r:state)
     requires ValidState(s) && ValidOperand(o.o1) && ValidOperand(o.o2)
 {
-    // TODO: this is where we havoc the flags for the comparison, once we model them
+    // this is where we would havoc flags for comparisons, if we modelled them
     maybeHandleInterrupt(s, r)
 }
 

verified/exception_handlers.vad

@@ -42,14 +42,9 @@ CPSID_IAF(operand mod:word)
         this.conf.nondet == nondet_int(old(this).conf.nondet, NONDET_GENERATOR());
         this.conf.tlb_consistent == old(this).conf.tlb_consistent;
         this.rng == old(this).rng;
-        (mode_of_state(old(this)) == Supervisor) ==> !stateTakesFiq(old(this));
+        mode_of_state(old(this)) == Supervisor ==> !stateTakesFiq(old(this));
 {
     reveal va_eval;
-    ghost if (mode_of_state(old(this)) == Supervisor) {
-        // TODO: if we're executing here after the instruction, it can only be
-        // because we didn't take a FIQ. But how to prove this?
-        assume !stateTakesFiq(old(this));
-    }
     exists s' :: maybeHandleInterrupt(old(this), s') && evalIns'(CPSID_IAF(@mod), s', this);
     lemma_PrivInterruptInvariants(old(this), s');
     assert mode_of_state(s') == mode_of_state(old(this))
@@ -621,7 +616,11 @@ procedure {:frame false} {:timeLimitMultiplier 2} interrupt_handler(
             && decode_psr(spsr_svc).m == User
             && !decode_psr(spsr_svc).f && !decode_psr(spsr_svc).i);
     ensures
-        KomInterruptHandlerInvariant(old(this), pagedb_in, this, dispPg);
+        if spsr_of_state(old(this)).m == User
+            then KomExceptionHandlerInvariant(old(this), pagedb_in, this, dispPg)
+        else if spsr_of_state(old(this)).m == Supervisor
+            then KomExceptionHandlerInvariant(prior_exstate, pagedb_in, this, dispPg)
+        else KomInterruptHandlerInvariant(old(this), this);
         validPageDb(pagedb);
         pageDbCorresponds(this.m, pagedb);
 {
@@ -744,6 +743,6 @@ procedure {:frame false} {:timeLimitMultiplier 2} interrupt_handler(
             TruncateWord(old(lr) - 4);
             TruncateWord(OperandContents(old(this), OLR) - 4);
         }
-        assert KomInterruptHandlerInvariant(old(this), pagedb_in, this, dispPg);
+        assert KomInterruptHandlerInvariant(old(this), this);
     }
 }

verified/exceptions.i.dfy

@@ -1,13 +1,19 @@
 include "kom_common.i.dfy"
 include "entry.i.dfy"
 
-predicate InterruptContinuationPreconditionDefInner()
-{
 // for now, we only take interrupts at the beginning of another exception handler
 // when the user-entry precondition still holds, so this is simplest...
+predicate KomInterruptHandlerPrecondition(s:state)
+{
+    ValidState(s)
+        && exists pagedb, dispPg:PageNr :: KomUserEntryPrecondition(s, pagedb, dispPg)
+}
+
+predicate InterruptContinuationPreconditionDefInner()
+{
     forall s:state {:trigger InterruptContinuationPrecondition(s)} ::
         ValidState(s) && InterruptContinuationPrecondition(s)
-        <==> (exists pagedb, dispPg:PageNr :: KomUserEntryPrecondition(s, pagedb, dispPg))
+        <==> KomInterruptHandlerPrecondition(s)
 }
 
 // XXX: the charade of inner/outer def and lemmas here are workarounds
@@ -38,26 +44,20 @@ lemma lemma_Establish_InterruptContinuationPrecondition(s:state, pagedb:PageDb,
     lemma_InterruptContinuationPreconditionDefInner();
 }
 
-function {:opaque} dummyPageDb(): PageDb { imap[] }
+predicate KomInterruptHandlerInvariant(s:state, r:state)
-function {:opaque} dummyPageNr(): PageNr { 0 }
-
-predicate KomInterruptHandlerInvariant(s:state, sd:PageDb, r:state, dispPg:PageNr)
     requires ValidState(s) && mode_of_state(s) != User && SaneMem(s.m)
     requires s.conf.ex == ExFIQ || s.conf.ex == ExIRQ
-    requires (priv_of_mode(spsr_of_state(s).m) == PL0
-              || spsr_of_state(s).m == Supervisor) ==> (
-        validPageDb(sd) && pageDbCorresponds(s.m, sd)
-        && finalDispatcher(sd, dispPg))
 {
-    ValidState(r) && (s.ok ==> r.ok)
+    // this definition tells us nothing about interrupts from user or svc modes,
+    // except that they set the low bit of SP
+    if spsr_of_state(s).m == User || spsr_of_state(s).m == Supervisor
+    then ValidState(r) ==> !evalOBool(r, OCmp(OTstEq, OSP, OConst(1)))
+    else ValidState(r) && (s.ok ==> r.ok)
     && SaneStateAfterException(r)
     && ParentStackPreserving(s, r)
     && GlobalsPreservingExcept(s, r, {PendingInterruptOp()})
     && s.conf.ttbr0 == r.conf.ttbr0 && s.conf.scr == r.conf.scr
-    && if (priv_of_mode(spsr_of_state(s).m) == PL1
+    && mode_of_state(r) == mode_of_state(s)
-          && spsr_of_state(s).m != Supervisor) then (
-        // if interrupted in privileged !SVC mode, we just set the pending flag
-        mode_of_state(r) == mode_of_state(s)
     && spsr_of_state(r) == spsr_of_state(s)
     && CoreRegPreservingExcept(s, r, {OLR})
     // see B1.8.3 "Link values saved on exception entry"
@@ -68,23 +68,26 @@ predicate KomInterruptHandlerInvariant(s:state, sd:PageDb, r:state, dispPg:PageN
     && s.conf.nondet == r.conf.nondet
     && s.conf.tlb_consistent == r.conf.tlb_consistent
     && s.rng == r.rng
-    ) else if (spsr_of_state(s).m == Supervisor) then (
-        exists s':state :: ValidState(s') && evalExceptionTaken(s', ExFIQ, nondet_word(s'.conf.nondet, NONDET_PC()), s)
-        && mode_of_state(s') != User && KomExceptionHandlerInvariant(s', sd, r, dispPg)
-    ) else (
-        KomExceptionHandlerInvariant(s, sd, r, dispPg)
-    )
 }
 
-// this lemma is trivial, but justifies the soundness of the ARMdef assumptions
+// this lemma justifies the ARMdef-level assumptions
-// ("EssentialInterruptContinuationInvariantProperties") about the handler
+// ("EssentialInterruptContinuationInvariantProperties") about the
+// state after the handler returns
 lemma lemma_KomInterruptHandlerInvariant_soundness(s:state, r:state)
     requires ValidState(s) && mode_of_state(s) != User && SaneMem(s.m)
     requires s.conf.ex == ExFIQ || s.conf.ex == ExIRQ
     requires priv_of_mode(spsr_of_state(s).m) == PL1 && spsr_of_state(s).m != Supervisor
-    requires KomInterruptHandlerInvariant(s, dummyPageDb(), r, dummyPageNr())
+    requires KomInterruptHandlerInvariant(s, r)
     ensures EssentialInterruptContinuationInvariantProperties(s, r)
 {
+    var sp := OperandContents(r, OSP);
+    assert sp == OperandContents(s, OSP);
+    assert WordAligned(sp);
+    assert BitsAsWord(1) == 1 && BitsAsWord(2) == 2 by { reveal BitsAsWord(); }
+    lemma_BitsAndWordConversions();
+    assert BitMod(WordAsBits(sp), 2) == 0
+        by { reveal WordAligned(); lemma_BitModEquiv(sp, 2); }
+    assert BitwiseAnd(sp, 1) == 0 by { reveal BitAnd(); reveal BitMod(); }
 }
 
 predicate {:opaque} InterruptContinuationInvariantDef()
@@ -93,40 +96,34 @@ predicate {:opaque} InterruptContinuationInvariantDef()
     forall s:state, r:state
         | ValidState(s) && mode_of_state(s) != User && SaneMem(s.m)
           && (s.conf.ex == ExFIQ || s.conf.ex == ExIRQ)
-          && priv_of_mode(spsr_of_state(s).m) == PL1
-          && spsr_of_state(s).m != Supervisor
         :: InterruptContinuationInvariant(s, r)
-        ==> KomInterruptHandlerInvariant(s, dummyPageDb(), r, dummyPageNr())
+        ==> KomInterruptHandlerInvariant(s, r)
 }
 
 lemma lemma_InterruptContinuationInvariantDef(s:state, r:state)
     requires InterruptContinuationInvariantDef()
     requires ValidState(s) && mode_of_state(s) != User && SaneMem(s.m)
     requires s.conf.ex == ExFIQ || s.conf.ex == ExIRQ
-    requires priv_of_mode(spsr_of_state(s).m) == PL1 && spsr_of_state(s).m != Supervisor
     requires InterruptContinuationInvariant(s, r)
-    ensures KomInterruptHandlerInvariant(s, dummyPageDb(), r, dummyPageNr())
+    ensures KomInterruptHandlerInvariant(s, r)
-    ensures s.conf.nondet == r.conf.nondet
+    //ensures s.conf.nondet == r.conf.nondet
-    ensures s.conf.tlb_consistent == r.conf.tlb_consistent
+    //ensures s.conf.tlb_consistent == r.conf.tlb_consistent
 {
     reveal InterruptContinuationInvariantDef();
-    if priv_of_mode(spsr_of_state(s).m) == PL1 {
-        assert s.conf.nondet == r.conf.nondet;
-    }
 }
 
 lemma lemma_PrivInterruptInvariants(s:state, r:state)
     requires InterruptContinuationInvariantDef()
-    requires ValidState(s) && SaneMem(s.m)
+    requires ValidState(s) && SaneMem(s.m) && s.ok
     requires priv_of_state(s) == PL1
-    requires (mode_of_state(s) == Supervisor) ==> s.conf.cpsr.i && !stateTakesFiq(s)
+    requires (mode_of_state(s) == Supervisor) ==> s.conf.cpsr.i
     requires maybeHandleInterrupt(s, r)
     requires SaneStack(s)
     ensures mode_of_state(r) == mode_of_state(s)
     ensures r.conf.ttbr0 == s.conf.ttbr0 && r.conf.scr == s.conf.scr
     ensures r.conf.tlb_consistent == s.conf.tlb_consistent
     ensures r.rng == s.rng
-    ensures SaneStack(r)
+    ensures ValidState(r) && SaneStack(r)
     ensures StackPreserving(s, r)
     ensures NonStackMemPreserving(s, r)
     ensures GlobalsPreservingExcept(s, r, {PendingInterruptOp()})
@@ -137,6 +134,7 @@ lemma lemma_PrivInterruptInvariants(s:state, r:state)
                 && s.regs[SP(m)] == r.regs[SP(m)]
     ensures interrupts_enabled(s) ==>
         r.conf.nondet == nondet_int(s.conf.nondet, NONDET_GENERATOR())
+    ensures (mode_of_state(s) == Supervisor) ==> !stateTakesFiq(s)
 {
     var nondet := nondet_word(s.conf.nondet, NONDET_EX());
     if !interrupts_enabled(s) {
@@ -151,6 +149,22 @@ lemma lemma_PrivInterruptInvariants(s:state, r:state)
             && evalMOVSPCLR(s2, r);
         lemma_evalExceptionTaken_Mode(s', ex, expc, s1);
         lemma_InterruptContinuationInvariantDef(s1, s2);
+
+        if mode_of_state(s) == Supervisor && stateTakesFiq(s) {
+            // proof by contradiction that if the handler returned, then we
+            // mustn't have taken a FIQ, so we don't need to consider that case
+            assert ex == ExFIQ;
+            assert InterruptContinuationPrecondition(s');
+            assert spsr_of_state(s1).m == Supervisor;
+            assert !evalOBool(s2, OCmp(OTstEq, OSP, OConst(1)));
+            assert EssentialInterruptContinuationInvariantProperties(s1, s2);
+            assert ValidState(s2);
+            assert s1.ok;
+            assert s2.ok;
+            assert evalOBool(s2, OCmp(OTstEq, OSP, OConst(1)));
+            assert false;
+        }
+
         forall m | m != mode_of_exception(s'.conf, ex)
             ensures s.regs[LR(m)] == r.regs[LR(m)]
             ensures s.regs[SP(m)] == r.regs[SP(m)]