PVS dump file byzantine.dmp

To extract the specifications and proofs, download this file to byzantine.dmp and from a running PVS type the command
   M-x undump-pvs-files
You will be prompted for the dump file name (byzantine.dmp) and the directory in which to dump the extracted files.
%Patch files loaded: patch2 version 2.399 $$$byzantine.pvs byzantine[m, n: nat, T: NONEMPTY_TYPE]: THEORY BEGIN ASSUMING mn_prop: ASSUMPTION 3 * m < n ENDASSUMING npos: LEMMA n > 0 proc: TYPE = below[n] rounds: TYPE = upto[m] vector: TYPE = [proc -> T] procset: TYPE = setof[proc] ok: procset IMPORTING cardinality@finite_cardinality[proc, n, id], cardinality@card_set[proc, n, id] G, p, q, z: VAR proc r: VAR rounds caucus: VAR procset v: VAR vector t: VAR T nok(caucus): procset = {z: proc | member(z, caucus) AND NOT ok(z)} allprocs: procset = fullset[proc] allset_card: LEMMA fincard(allprocs) = n max_faults: AXIOM fincard(nok(allprocs)) <= m remove_lemma: LEMMA member(p, caucus) IMPLIES fincard(remove(p, caucus)) = fincard(caucus) - 1 nok_lemma1: LEMMA ok(p) IMPLIES fincard(nok(remove(p, caucus))) = fincard(nok(caucus)) nok_lemma3: LEMMA NOT ok(p) AND member(p, caucus) IMPLIES fincard(nok(remove(p, caucus))) = fincard(nok(caucus)) - 1 maj(caucus, v): T maj_ax: AXIOM fincard(caucus) > 2 * fincard(nok(caucus)) AND (FORALL p: ok(p) AND member(p, caucus) => v(p) = t) IMPLIES maj(caucus, v) = t maj_ext: AXIOM FORALL (v1, v2: vector): (FORALL p: member(p, caucus) => v1(p) = v2(p)) IMPLIES maj(caucus, v1) = maj(caucus, v2) send: [T, proc, proc -> T] send_ax: AXIOM ok(p) AND ok(q) => send(t, p, q) = t distr(t, p): vector = (LAMBDA (z: proc): send(t, p, z)) % distr(t,p)(q):t=send(t,p,q) arb: T OMBG(G, r, t, caucus) (p) : RECURSIVE T = IF r = 0 THEN IF member(G, caucus) AND member(p, caucus) THEN send(t, G, p) ELSE arb ENDIF ELSE IF member(G, caucus) AND member(p, caucus) THEN IF p = G THEN send(t, G, G) ELSE maj(remove(G, caucus), (LAMBDA q: OMBG(q, r - 1, send(t, G, q), remove(G, caucus))(p))) ENDIF ELSE arb ENDIF ENDIF MEASURE r C2_prop(r): bool = (FORALL p, G, t, caucus: ok(p) AND ok(G) AND member(p, caucus) AND member(G, caucus) AND fincard(caucus) > 2 * fincard(nok(caucus)) + r IMPLIES OMBG(G, r, t, caucus)(p) = t) C2: LEMMA C2_prop(r) C2_final: THEOREM ok(p) AND ok(G) IMPLIES OMBG(G, m, t, allprocs)(p) = t C1_prop(r): bool = (FORALL p, q, G, caucus, t: ok(p) AND ok(q) AND member(p, caucus) AND member(q, caucus) AND member(G, caucus) AND fincard(caucus) > 3 * r AND r >= fincard(nok(caucus)) IMPLIES OMBG(G, r, t, caucus)(p) = OMBG(G, r, t, caucus)(q)) C1: LEMMA C1_prop(r) C1_final: THEOREM ok(p) AND ok(q) IMPLIES FORALL (G: proc): OMBG(G, m, t, allprocs)(p) = OMBG(G, m, t, allprocs)(q) END byzantine $$$byzantine.prf (|byzantine| (|npos| "" (USE "mn_prop") (("" (ASSERT) NIL))) (|id_TCC1| "" (SUBTYPE-TCC) NIL) (IMPORTING1_TCC1 "" (USE "npos") NIL) (|allset_card| "" (USE "fullset_fincard") (("" (EXPAND "allprocs") (("" (PROPAX) NIL))))) (|remove_lemma| "" (AUTO-REWRITE "npos" "member") (("" (SKOSIMP) (("" (USE "fincard_remove") (("" (GROUND) NIL))))))) (|nok_lemma1| "" (SKOSIMP) (("" (USE "fincard_remove") (("" (GROUND) (("" (CASE-REPLACE "nok(remove(p!1, caucus!1)) = nok(caucus!1)") (("" (HIDE -2 2) (("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (EXPAND "nok") (("" (GRIND) NIL))))))))))))))) (|nok_lemma3| "" (SKOSIMP) (("" (CASE "nok(remove(p!1, caucus!1)) = remove(p!1, nok(caucus!1))") (("1" (REPLACE -1 :HIDE? T) (("1" (LEMMA "fincard_remove") (("1" (INST -1 "p!1" "nok(caucus!1)") (("1" (GROUND) (("1" (EXPAND "nok") (("1" (PROPAX) NIL))))))))))) ("2" (HIDE 3) (("2" (APPLY-EXTENSIONALITY :HIDE? T) (("2" (GRIND) NIL))))))))) (OMBG_TCC1 "" (SUBTYPE-TCC) NIL) (OMBG_TCC2 "" (TERMINATION-TCC) NIL) (C2 "" (AUTO-REWRITE "send_ax" "distr" "remove_lemma" "nok_lemma1") (("" (INDUCT "r") (("1" (ASSERT) (("1" (EXPAND "C2_prop") (("1" (SKOSIMP) (("1" (EXPAND "OMBG") (("1" (GROUND) NIL))))))))) ("2" (SKOSIMP) (("2" (EXPAND "C2_prop" +) (("2" (SKOSIMP) (("2" (EXPAND "OMBG") (("2" (SMASH) (("2" (REWRITE "maj_ax") (("2" (HIDE -7 3) (("2" (SKOSIMP) (("2" (EXPAND "C2_prop") (("2" (INST?) (("2" (GROUND) (("1" (ASSERT) NIL) ("2" (GRIND) NIL))))))))))))))))))))))))))) (|C2_final_TCC1| "" (TCC) NIL) (|C2_final| "" (SKOSIMP) (("" (LEMMA "C2") (("" (EXPAND "C2_prop") (("" (INST?) (("" (GROUND) (("1" (GRIND) NIL) ("2" (GRIND) NIL) ("3" (REWRITE "allset_card") (("3" (LEMMA "max_faults") (("3" (LEMMA "mn_prop") (("3" (ASSERT) NIL))))))))))))))))) (C1 "" (AUTO-REWRITE "send_ax" "distr") (("" (INDUCT "r") (("1" (EXPAND "C1_prop") (("1" (SKOSIMP) (("1" (ASSERT) (("1" (CASE "ok(G!1)") (("1" (EXPAND "OMBG") (("1" (ASSERT) NIL))) ("2" (HIDE 2) (("2" (TYPEPRED "fincard(nok(caucus!1))") (("2" (USE "fincard_non_empty" :IF-MATCH T) (("2" (GROUND) (("2" (INST 1 "G!1") (("2" (EXPAND "nok") (("2" (PROPAX) NIL))))))))))))))))))))) ("2" (SKOSIMP) (("2" (EXPAND "C1_prop" +) (("2" (SKOSIMP) (("2" (ASSERT) (("2" (CASE "ok(G!1)") (("1" (LEMMA "C2") (("1" (EXPAND "C2_prop") (("1" (AUTO-REWRITE -1) (("1" (ASSERT) NIL))))))) ("2" (EXPAND "OMBG") (("2" (GROUND) (("2" (REWRITE "maj_ext") (("2" (HIDE 3) (("2" (SKOSIMP) (("2" (EXPAND "C1_prop") (("2" (INST?) (("2" (GRIND :EXCLUDE "fincard" :REWRITES ("remove_lemma" "nok_lemma3")) NIL))))))))))))))))))))))))))))) (|C1_final_TCC1| "" (TCC) NIL) (|C1_final| "" (SKOSIMP*) (("" (LEMMA "C1") (("" (EXPAND "C1_prop") (("" (INST?) (("" (GROUND) (("1" (GRIND) NIL) ("2" (GRIND) NIL) ("3" (GRIND) NIL) ("4" (LEMMA "allset_card") (("4" (LEMMA "mn_prop") (("4" (ASSERT) NIL))))) ("5" (LEMMA "max_faults") (("5" (ASSERT) NIL))))))))))))))