From e23007e511058e0a1a91eafcecc14194ea4ccd4c Mon Sep 17 00:00:00 2001 From: Ken McMillan Date: Mon, 29 Jan 2018 10:29:13 -0800 Subject: [PATCH] removing unneeded lemmas from vsync_paxos_ms --- test/vsync_paxos.ivy | 10 +++++++--- 1 file changed, 7 insertions(+), 3 deletions(-) diff --git a/test/vsync_paxos.ivy b/test/vsync_paxos.ivy index 98bfd86..7491038 100644 --- a/test/vsync_paxos.ivy +++ b/test/vsync_paxos.ivy @@ -163,12 +163,16 @@ action start(e:epoch, e_prev: epoch, n:node, s:stake, nset:nodeset.set, c:config # (s < K2) -> (epoch_ended(e_prev) -> c = config_decided(e_prev)); assume epoch_ended(e_prev) -> c = config_decided(e_prev); +# true but not needed... + # assume epoch_ended(e_prev) -> s = epoch_stake(e_prev) & c = config_decided(e_prev); - assert E1 = e_prev & K = s & C = c & N = nodeset.common(nset,nset) -> accept_msg(e_prev,s,c); - assume accept_msg(e_prev,s,c); +# assert E1 = e_prev & K = s & C = c & N = nodeset.common(nset,nset) -> accept_msg(e_prev,s,c); +# assume accept_msg(e_prev,s,c); +# true but not needed... + # assert forall C,K,E1,N,E2. C = c & K = s & E1 = e_prev & N = nodeset.common(nset,nset) & E2 < e_prev -> epoch_ended(E2); - assume forall E2. (E2 < e_prev -> epoch_ended(E2)); +# assume forall E2. (E2 < e_prev -> epoch_ended(E2)); # assert forall C,K,E1,N,E2,N1,I,V1,S2,K2,C2. C = c & K = s & E1 = e_prev & S1 = accept_maj(E1,s) & N = nodeset.common(S1,S1) & S2 = epoch_maj(E2) & K2 = epoch_stake(E2) & C2 = config_decided(E2) # & E2 < e_prev & nodeset.member(N1,epoch_maj(E2)) & vote(E2,N1,I,V1) -> val_at(c,I,V1);