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 |