move ironfleet set lemmas out to common file

verified/Sets.dfy

@@ -0,0 +1,32 @@
+// lifted from ironfleet/src/Dafny/Distributed/Common/Collections/Sets.i.dfy
+
+function SetOfNumbersInRightExclusiveRange(a:int, b:int):set<int>
+    requires a <= b;
+    ensures forall opn :: a <= opn < b ==> opn in SetOfNumbersInRightExclusiveRange(a, b);
+    ensures forall opn :: opn in SetOfNumbersInRightExclusiveRange(a, b) ==> a <= opn < b;
+    ensures |SetOfNumbersInRightExclusiveRange(a, b)| == b-a;
+    decreases b-a;
+{
+    if a == b then {} else {a} + SetOfNumbersInRightExclusiveRange(a+1, b)
+}
+
+lemma ThingsIKnowAboutSubset<T>(x:set<T>, y:set<T>)
+    requires x<y;
+    ensures |x|<|y|;
+{
+    if (x!={}) {
+        var e :| e in x;
+        ThingsIKnowAboutSubset(x-{e}, y-{e});
+    }
+}
+
+lemma SubsetCardinality<T>(x:set<T>, y:set<T>)
+    ensures x<y ==> |x|<|y|;
+    ensures x<=y ==> |x|<=|y|;
+{
+    if (x<y) {
+        ThingsIKnowAboutSubset(x, y);
+    }
+    if (x==y) { // OBSERVE the other case
+    }
+}

verified/pagedb.s.dfy

@@ -1,5 +1,6 @@
 include "kev_common.s.dfy"
 include "Maybe.dfy"
+include "Sets.dfy"
 include "ARMdef.dfy"
 
 type PageNr = int
@@ -172,17 +173,6 @@ predicate addrspaceL1Unique(d: PageDb, n: PageNr)
         ==> !d[p].entry.L1PTable?
 }
 
-// taken from ironclad set libraries
-function SetOfNumbersInRightExclusiveRange(a:int, b:int):set<int>
-    requires a <= b;
-    ensures forall opn :: a <= opn < b ==> opn in SetOfNumbersInRightExclusiveRange(a, b);
-    ensures forall opn :: opn in SetOfNumbersInRightExclusiveRange(a, b) ==> a <= opn < b;
-    ensures |SetOfNumbersInRightExclusiveRange(a, b)| == b-a;
-    decreases b-a;
-{
-    if a == b then {} else {a} + SetOfNumbersInRightExclusiveRange(a+1, b)
-}
-
 function {:opaque} validPageNrs(): set<PageNr>
     ensures forall n :: n in validPageNrs() <==> validPageNr(n)
 {

verified/smc_handler.sdfy

@@ -28,29 +28,6 @@ lemma PageDbCorrespondsImpliesEntryCorresponds(s:memstate, d:PageDb, n:PageNr)
     reveal_pageDbClosedRefs();
 }
 
-// XXX: lifted from ironfleet/src/Dafny/Distributed/Common/Collections/Sets.i.dfy
-lemma ThingsIKnowAboutSubset<T>(x:set<T>, y:set<T>)
-    requires x<y;
-    ensures |x|<|y|;
-{
-    if (x!={}) {
-        var e :| e in x;
-        ThingsIKnowAboutSubset(x-{e}, y-{e});
-    }
-}
-
-// XXX: lifted from ironfleet/src/Dafny/Distributed/Common/Collections/Sets.i.dfy
-lemma SubsetCardinality<T>(x:set<T>, y:set<T>)
-    ensures x<y ==> |x|<|y|;
-    ensures x<=y ==> |x|<=|y|;
-{
-    if (x<y) {
-        ThingsIKnowAboutSubset(x, y);
-    }
-    if (x==y) { // OBSERVE the other case
-    }
-}
-
 lemma BoundedAddrspaceRefs(d:PageDb, n:PageNr)
     requires validPageDb(d)
     requires isAddrspace(d, n)

verified/subdir.mk

@@ -5,7 +5,7 @@ SPARTANFLAGS = #-assumeUpdates 1
 ARMSPARTAN_NAMES = ARMdef ARMprint ARMspartan
 ARMSPARTAN_DEPS = $(foreach n,$(ARMSPARTAN_NAMES),$(dir)/$(n).verified)
 ARMSPARTAN_INCLUDES = $(foreach n,$(ARMSPARTAN_NAMES),-i $(n).dfy)
-KEVLAR_NAMES = kev_common.i pagedb.i smcapi.i abstate.s entry.s
+KEVLAR_NAMES = kev_common.i pagedb.i smcapi.i abstate.s entry.s Sets
 KEVLAR_DEPS = $(foreach n,$(KEVLAR_NAMES),$(dir)/$(n).verified)
 KEVLAR_INCLUDES = $(foreach n,$(KEVLAR_NAMES),-i $(n).dfy)
 SDFY_INCLUDES =  $(dir)/ARMdecls.sdfy $(dir)/kev_utils.sdfy
@@ -25,7 +25,7 @@ SDFY_INCLUDES =  $(dir)/ARMdecls.sdfy $(dir)/kev_utils.sdfy
 #	$(SDFY_INCLUDES) $< && touch $@
 
 # Mindy can't handle these files, so we must use vanilla Dafny
-DAFNY_ONLY = ARMspartan Seq kev_common.s pagedb.s
+DAFNY_ONLY = ARMspartan Seq Sets kev_common.s
 $(foreach n,$(DAFNY_ONLY),$(dir)/$(n).verified): %.verified: %.dfy
 	$(DAFNY) $(DAFNYFLAGS) /compile:0 $< && touch $@
 
@@ -60,7 +60,7 @@ $(dir)/ARMdef.verified: $(dir)/assembly.s.verified $(dir)/Maybe.verified $(dir)/
 $(dir)/ARMprint.verified: $(dir)/ARMdef.verified
 $(dir)/ARMspartan.verified: $(dir)/ARMdef.verified
 $(dir)/kev_common.s.verified: $(dir)/ARMdef.verified
-$(dir)/pagedb.s.verified: $(dir)/kev_common.s.verified $(dir)/Maybe.verified
+$(dir)/pagedb.s.verified: $(dir)/kev_common.s.verified $(dir)/Maybe.verified $(dir)/Sets.verified
 $(dir)/kev_common.i.verified: $(dir)/ARMspartan.verified $(dir)/kev_common.s.verified $(dir)/pagedb.s.verified
 $(dir)/smcapi.s.verified: $(dir)/kev_common.s.verified $(dir)/pagedb.s.verified
 $(dir)/smcapi.i.verified: $(dir)/smcapi.s.verified