38 hdr_sum_def |
38 hdr_sum_def |
39 "hdr_sum(M,b) == countm(M,%pkt.hdr(pkt) = b)" |
39 "hdr_sum(M,b) == countm(M,%pkt.hdr(pkt) = b)" |
40 |
40 |
41 (* Lemma 5.1 *) |
41 (* Lemma 5.1 *) |
42 inv1_def |
42 inv1_def |
43 "inv1(s) == \ |
43 "inv1(s) == |
44 \ (!b. count(rsent(rec(s)),b) = count(srcvd(sen(s)),b) + count(rsch(s),b)) \ |
44 (!b. count(rsent(rec(s)),b) = count(srcvd(sen(s)),b) + count(rsch(s),b)) |
45 \ & (!b. count(ssent(sen(s)),b) \ |
45 & (!b. count(ssent(sen(s)),b) |
46 \ = hdr_sum(rrcvd(rec(s)),b) + hdr_sum(srch(s),b))" |
46 = hdr_sum(rrcvd(rec(s)),b) + hdr_sum(srch(s),b))" |
47 |
47 |
48 (* Lemma 5.2 *) |
48 (* Lemma 5.2 *) |
49 inv2_def "inv2(s) == \ |
49 inv2_def "inv2(s) == |
50 \ (rbit(rec(s)) = sbit(sen(s)) & \ |
50 (rbit(rec(s)) = sbit(sen(s)) & |
51 \ ssending(sen(s)) & \ |
51 ssending(sen(s)) & |
52 \ count(rsent(rec(s)),~sbit(sen(s))) <= count(ssent(sen(s)),~sbit(sen(s))) &\ |
52 count(rsent(rec(s)),~sbit(sen(s))) <= count(ssent(sen(s)),~sbit(sen(s))) & |
53 \ count(ssent(sen(s)),~sbit(sen(s))) <= count(rsent(rec(s)),sbit(sen(s)))) \ |
53 count(ssent(sen(s)),~sbit(sen(s))) <= count(rsent(rec(s)),sbit(sen(s)))) |
54 \ | \ |
54 | |
55 \ (rbit(rec(s)) = (~sbit(sen(s))) & \ |
55 (rbit(rec(s)) = (~sbit(sen(s))) & |
56 \ rsending(rec(s)) & \ |
56 rsending(rec(s)) & |
57 \ count(ssent(sen(s)),~sbit(sen(s))) <= count(rsent(rec(s)),sbit(sen(s))) & \ |
57 count(ssent(sen(s)),~sbit(sen(s))) <= count(rsent(rec(s)),sbit(sen(s))) & |
58 \ count(rsent(rec(s)),sbit(sen(s))) <= count(ssent(sen(s)),sbit(sen(s))))" |
58 count(rsent(rec(s)),sbit(sen(s))) <= count(ssent(sen(s)),sbit(sen(s))))" |
59 |
59 |
60 (* Lemma 5.3 *) |
60 (* Lemma 5.3 *) |
61 inv3_def "inv3(s) == \ |
61 inv3_def "inv3(s) == |
62 \ rbit(rec(s)) = sbit(sen(s)) \ |
62 rbit(rec(s)) = sbit(sen(s)) |
63 \ --> (!m. sq(sen(s))=[] | m ~= hd(sq(sen(s))) \ |
63 --> (!m. sq(sen(s))=[] | m ~= hd(sq(sen(s))) |
64 \ --> count(rrcvd(rec(s)),<sbit(sen(s)),m>) \ |
64 --> count(rrcvd(rec(s)),<sbit(sen(s)),m>) |
65 \ + count(srch(s),<sbit(sen(s)),m>) \ |
65 + count(srch(s),<sbit(sen(s)),m>) |
66 \ <= count(rsent(rec(s)),~sbit(sen(s))))" |
66 <= count(rsent(rec(s)),~sbit(sen(s))))" |
67 |
67 |
68 (* Lemma 5.4 *) |
68 (* Lemma 5.4 *) |
69 inv4_def "inv4(s) == rbit(rec(s)) = (~sbit(sen(s))) --> sq(sen(s)) ~= []" |
69 inv4_def "inv4(s) == rbit(rec(s)) = (~sbit(sen(s))) --> sq(sen(s)) ~= []" |
70 |
70 |
71 end |
71 end |