Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Remove NullMsg #7

Merged
merged 3 commits into from
Feb 6, 2018
Merged

Remove NullMsg #7

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
2947298
remove need for null address
palmskog Feb 4, 2018
058c0ea
remove NullMsg
palmskog Feb 4, 2018
9ef6f84
Merge branch 'no-null-msg' into remove-nullmsg
palmskog Feb 6, 2018
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
23 changes: 9 additions & 14 deletions Properties/InvCliqueTopology.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -81,7 +81,6 @@ Lemma procMsg_nGetData_no_blocks st p q stPm ms n' :
Proof.
rewrite [procMsg _ _ _ _]surjective_pairing; case=>_{stPm}<-{ms}.
case (msg p); rewrite /procMsg/=; case: st=>id ps bt tp GD/=.
- by case: ifP=>//_; apply/allP=>m; rewrite inE=>/eqP->/=; rewrite eqxx.
- move=>pt; apply/allP=>m; rewrite !inE.
move/mapP=>[z]; rewrite mem_filter/emitMany/emitBroadcast=>/andP[_].
by rewrite mem_cat=>/orP[]/=; move/mapP=>[y]_->->/=; rewrite eqxx.
Expand Down Expand Up @@ -245,7 +244,7 @@ case: GSyncW=>can_bc [can_bt] [can_n] []
+ move=>st'; rewrite findU c1 /=;
case: ifP; last by move=>_ F'; apply (HHold _ F').
move/eqP=>Eq [Eq']; subst can_n stPm.
case Msg: (msg p)=>[|||b|||]; rewrite Msg in P;
case Msg: (msg p)=>[||b|||]; rewrite Msg in P;
do? by [NBlockMsg_dest_btChain q st p b Msg P H; move: (HHold _ F)].
BlockMsg_dest q st (src p) b iF P Msg;
move: (c3 (dst p) _ F) (c4 (dst p) _ F) (c5 (dst p) _ F)=>V Vh Ib;
Expand All @@ -256,7 +255,7 @@ case: GSyncW=>can_bc [can_bt] [can_n] []
(* can_bc is still the largest chain *)
+ move=>n' bc'; rewrite/holds findU c1 /=; case: ifP.
move/eqP=>Eq st' [Eq']; subst n' stPm.
case Msg: (msg p)=>[|||b|||]; rewrite Msg in P;
case Msg: (msg p)=>[||b|||]; rewrite Msg in P;
do? by
[NBlockMsg_dest_btChain q st p b Msg P H=>Hc; move: (HGt (dst p) bc' _ F Hc)].
by BlockMsg_dest q st (src p) b iF P Msg;
Expand All @@ -283,7 +282,7 @@ case: GSyncW=>can_bc [can_bt] [can_n] []
* move/eqP=>Eq [Eq']; subst n' stPm;
move=>z; specialize (H1 z); specialize (H2 z).
rewrite H2 in H1; move=>H3. specialize (H1 H3).
case Msg: (msg p)=>[|prs|||||]; rewrite Msg in P;
case Msg: (msg p)=>[prs|||||]; rewrite Msg in P;
rewrite [procMsg _ _ _ _] surjective_pairing in P; case: P=><- _;
destruct st; rewrite/procMsg/=; do? by [];
do? rewrite /Protocol.peers in H1.
Expand All @@ -307,7 +306,7 @@ case: GSyncW=>can_bc [can_bt] [can_n] []
case:ifP=>[/eqP Z|_/=]; first by subst x; rewrite eq_sym NDst.
by case: ifP=>///eqP Z; subst n'; rewrite/= Hi.

case Msg: (msg p)=>[||||||hash];
case Msg: (msg p)=>[|||||hash];
set old_msgs := [seq msg_block (msg p) | p <- inFlightMsgs w & dst p == n'];
set bt := (foldl btExtend (blockTree st') old_msgs);
move: (c3 _ _ F')=>h3; move: (c4 _ _ F')=>h4; move: (c5 _ _ F')=>h5;
Expand All @@ -320,10 +319,8 @@ case: GSyncW=>can_bc [can_bt] [can_n] []
move: (btExtend_foldG hIB allG)=>->].
(* procMsg GetDataMsg => BlockMsg in ms *)
rewrite [procMsg _ _ _ _] surjective_pairing in P; case: P=>_ <-.
case: st F P'=>id0 peers0 blockTree0 txPool0 F P';
rewrite/procMsg Msg /=; case: ifP=>/=;
first by case: ifP=>//=;
by move: (find_some hIB)=>hG; move: (btExtend_withDup_noEffect hG)=><-.
case: st F P'=>id0 peers0 blockTree0 txPool0 F P'.
rewrite/procMsg Msg /=; case: ifP=>/=; first by move: (find_some hIB)=>hG.
move/eqP => H_neq.
case: ifP=>//=; move=>/eqP En'.
- rewrite/get_block. (* blockTree wrt. the state of (dst p) in w *)
Expand Down Expand Up @@ -355,7 +352,7 @@ case: GSyncW=>can_bc [can_bt] [can_n] []
(ts q) (c3 _ _ F) (c4 _ _ F) (c5 _ _ F))=>G'.
rewrite ?Z1 ?Z2 in V' G';
rewrite filter_cat map_cat foldl_cat btExtend_fold_comm//.
case Msg: (msg p)=>[|||b|||h];
case Msg: (msg p)=>[||b|||h];
do? [
(have: (msg_type (msg p) != MGetData) by rewrite Msg)=>notGD;
move: (procMsg_nGetData_no_blocks (dst p) P notGD)=>//allG;
Expand All @@ -382,8 +379,7 @@ case: GSyncW=>can_bc [can_bt] [can_n] []

(* GetDataMsg *)
destruct st; rewrite -Z2 /procMsg Msg /=; case: ifP=>/=X.
* by case: ifP=>/=?;
do? [rewrite/has_init_block /= in G';
* by do? [rewrite/has_init_block /= in G';
move: (btExtend_withDup_noEffect (find_some G'))=><-];
move: (HExt _ _ F); rewrite/blocksFor=>-> /=;
do [rewrite Z1 in H'; rewrite (rem_non_block w V')//;
Expand All @@ -400,8 +396,7 @@ case: GSyncW=>can_bc [can_bt] [can_n] []
case: ifP => H_eq' //=; last by move/eqP: H_eq' => H_eq'; move/eqP: H_neq => H_neq.
exact: (HExt _ _ F).
- move/eqP: H_neq => H_neq //=.
by case ohead => [tx|] //=;
case:ifP=> //=; move/eqP => H_eq;
by case ohead => [tx|] //=; first (case:ifP=> //=; move/eqP => H_eq);
do? [rewrite/has_init_block /= in G';
move: (btExtend_withDup_noEffect (find_some G'))=><-];
move: (HExt _ _ F); rewrite/blocksFor=>-> /=;
Expand Down
1 change: 0 additions & 1 deletion Structures/Forests.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -23,7 +23,6 @@ Definition Hash := [ordType of nat].
Parameter VProof : eqType.
Parameter Transaction : eqType.
Parameter Address : finType.
Parameter NullAddress : Address.

Definition block := @Block Transaction VProof.
Parameter GenesisBlock : block.
Expand Down
62 changes: 25 additions & 37 deletions Systems/Protocol.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -15,7 +15,6 @@ Unset Printing Implicit Defensive.
Definition peers_t := seq Address.

Inductive Message :=
| NullMsg
| AddrMsg of peers_t
| ConnectMsg
| BlockMsg of block
Expand All @@ -24,7 +23,6 @@ Inductive Message :=
| GetDataMsg of Hash.

Inductive MessageType :=
| MNull
| MAddr
| MConnect
| MBlock
Expand All @@ -35,7 +33,6 @@ Inductive MessageType :=
Module MsgTypeEq.
Definition eq_msg_type a b :=
match a, b with
| MNull, MNull => true
| MAddr, MAddr => true
| MConnect, MConnect => true
| MBlock, MBlock => true
Expand All @@ -58,7 +55,6 @@ Export MsgTypeEq.

Definition msg_type (msg : Message) : MessageType :=
match msg with
| NullMsg => MNull
| AddrMsg _ => MAddr
| ConnectMsg => MConnect
| BlockMsg _ => MBlock
Expand Down Expand Up @@ -87,8 +83,6 @@ Inductive InternalTransition :=
Module MsgEq.
Definition eq_msg a b :=
match a, b with
| NullMsg, NullMsg => true
| NullMsg, _ => false
| AddrMsg prsA, AddrMsg prsB => (prsA == prsB)
| AddrMsg _, _ => false
| ConnectMsg, ConnectMsg => true
Expand All @@ -112,23 +106,22 @@ Ltac simple_tactic mb n n' B :=
Lemma eq_msgP : Equality.axiom eq_msg.
Proof.
move=> ma mb. rewrite/eq_msg.
case: ma=>[|p||b|t|h|h].
- case: mb=>//[|p'||b'|t'|h'|h']; do? [by constructor 2]; by constructor 1.
- case: mb=>//[|p'||b'|t'|h'|h']; do? [by constructor 2].
case: ma=>[p||b|t|h|h].
- case: mb=>//[p'||b'|t'|h'|h']; do? [by constructor 2].
case B: ((p == p')).
- by move/eqP:B=><-; constructor 1.
by constructor 2; case=>Z; subst p'; rewrite eqxx in B.
- case:mb=>////[|p'||b'|t'|h'|h']; do? [by constructor 2|by constructor 1].
- case:mb=>////[|p'||b'|t'|h'|h']; do? [by constructor 2].
- case:mb=>////[p'||b'|t'|h'|h']; do? [by constructor 2|by constructor 1].
- case:mb=>////[p'||b'|t'|h'|h']; do? [by constructor 2].
case B: (b == b'); [by case/eqP:B=><-; constructor 1|constructor 2].
by case=>Z; subst b'; rewrite eqxx in B.
- case:mb=>////[|p'||b'|t'|h'|h']; do? [by constructor 2].
- case:mb=>////[p'||b'|t'|h'|h']; do? [by constructor 2].
case B: (t == t'); [by case/eqP:B=><-; constructor 1|constructor 2].
by case=>Z; subst t'; rewrite eqxx in B.
- case:mb=>////[|p'||b'|t'|h'|h']; do? [by constructor 2].
- case:mb=>////[p'||b'|t'|h'|h']; do? [by constructor 2].
case B: (h == h'); [by case/eqP:B=><-; constructor 1|constructor 2].
by case=>Z; subst h'; rewrite eqxx in B.
- case:mb=>////[|p'||b'|t'|h'|h']; do? [by constructor 2].
- case:mb=>////[p'||b'|t'|h'|h']; do? [by constructor 2].
case B: (h == h'); [by case/eqP:B=><-; constructor 1|constructor 2].
by case=>Z; subst h'; rewrite eqxx in B.
Qed.
Expand All @@ -139,7 +132,6 @@ End MsgEq.
Export MsgEq.

Record Packet := mkP {src: Address; dst: Address; msg: Message}.
Definition NullPacket := mkP NullAddress NullAddress NullMsg.

Module PacketEq.
Definition eq_pkt a b :=
Expand All @@ -161,7 +153,7 @@ Export PacketEq.


Definition ToSend := seq Packet.
Definition emitZero : ToSend := [:: NullPacket].
Definition emitZero : ToSend := [::].
Definition emitOne (packet : Packet) : ToSend := [:: packet].
Definition emitMany (packets : ToSend) := packets.

Expand All @@ -178,25 +170,25 @@ Record State :=

Definition Init (n : Address) : State :=
Node n [:: n] (#GenesisBlock \\-> GenesisBlock) [::].
Lemma peers_uniq_init (n : Address) : uniq [::n]. Proof. done. Qed.
Lemma peers_uniq_init (n : Address) : uniq [::n]. Proof. by []. Qed.

Definition procMsg (st: State) (from : Address) (msg: Message) (ts: Timestamp) :=
let: (Node n prs bt pool) := st in
let: Node n prs bt pool := st in
match msg with
| ConnectMsg =>
let: ownHashes := (keys_of bt) ++ [seq hashT t | t <- pool] in
pair (Node n (undup (from :: prs)) bt pool)
(emitOne(mkP n from (InvMsg ownHashes)))
(emitOne (mkP n from (InvMsg ownHashes)))

| AddrMsg knownPeers =>
let: newP := [seq x <- knownPeers | x \notin prs] in
let: connects := [seq mkP n p ConnectMsg | p <- newP] in
let: updP := undup (prs ++ newP) in
pair (Node n updP bt pool)
(emitMany(connects) ++ emitBroadcast n prs (AddrMsg updP))
(emitMany connects ++ emitBroadcast n prs (AddrMsg updP))

| BlockMsg b =>
let: newBt := (btExtend bt b) in
let: newBt := btExtend bt b in
let: newPool := [seq t <- pool | txValid t (btChain newBt)] in
let: ownHashes := (keys_of newBt) ++ [seq hashT t | t <- newPool] in
pair (Node n prs newBt newPool) (emitBroadcast n prs (InvMsg ownHashes))
Expand All @@ -210,53 +202,49 @@ Definition procMsg (st: State) (from : Address) (msg: Message) (ts: Timestamp) :
let: ownHashes := (keys_of bt) ++ [seq hashT t | t <- pool] in
let: newH := [seq h <- peerHashes | h \notin ownHashes] in
let: gets := [seq mkP n from (GetDataMsg h) | h <- newH] in
pair st (emitMany(gets))
pair st (emitMany gets)

| GetDataMsg h =>
(* Do not respond to yourself *)
if from == n then pair st emitZero else
let: matchingBlocks := [seq b <- [:: get_block bt h] | b != GenesisBlock] in
match ohead matchingBlocks with
| Some b => pair (Node n prs bt pool) (emitOne(mkP n from (BlockMsg b)))
| Some b => pair (Node n prs bt pool) (emitOne (mkP n from (BlockMsg b)))
| None =>
let: matchingTxs := [seq t <- pool | (hashT t) == h] in
match ohead matchingTxs with
| Some tx =>
pair (Node n prs bt pool) (emitOne(mkP n from (TxMsg tx)))
pair (Node n prs bt pool) (emitOne (mkP n from (TxMsg tx)))
| None => pair st emitZero
end
end
| NullMsg => pair st emitZero
end.

Definition procInt (st : State) (tr : InternalTransition) (ts : Timestamp) :=
let: (Node n prs bt pool) := st in
let: Node n prs bt pool := st in
match tr with
| TxT tx => pair st (emitBroadcast n prs (TxMsg tx))

(* Assumption: nodes broadcast to themselves as well! => simplifies logic *)
| MintT =>
let: bc := (btChain bt) in
let: bc := btChain bt in
let: attempt := genProof n bc in
match attempt with
| Some(pf) =>
| Some pf =>
if VAF pf ts bc then
let: allowedTxs := [seq t <- pool | txValid t bc] in
let: prevBlock := (last GenesisBlock bc) in
let: block := mkB (hashB prevBlock) allowedTxs pf in

if tx_valid_block (btChain bt) block then
let: newBt := (btExtend bt block) in
let: newBt := btExtend bt block in
let: newPool := [seq t <- pool | txValid t (btChain newBt)] in
let: ownHashes := (keys_of newBt) ++ [seq hashT t | t <- newPool] in
pair (Node n prs newBt newPool) (emitBroadcast n prs (BlockMsg block))
else
pair st emitZero

else
pair st emitZero

| _ => pair st emitZero
| None => pair st emitZero
end
end.

Expand All @@ -281,7 +269,7 @@ Lemma procMsg_valid :
valid (blockTree s1) -> valid (blockTree (procMsg s1 from m ts).1).
Proof.
move=> s1 from m ts.
case Msg: m=>[|||b|||];
case Msg: m=>[||b|||];
destruct s1; rewrite/procMsg/=; do?by [|move: (btExtendV blockTree0 b)=><-].
case:ifP => //=.
move/eqP => H_neq; case: ifP; move/eqP => //= H_eq H_v.
Expand All @@ -306,7 +294,7 @@ Lemma procMsg_validH :
validH (blockTree (procMsg s1 from m ts).1).
Proof.
move=> s1 from m ts.
case Msg: m=>[|||b|||];
case Msg: m=>[||b|||];
destruct s1; rewrite/procMsg/=; do? by []; do? by case: ifP => //=.
- by move=>v vh; apply btExtendH.
- move=>v vh; case: ifP => //=; move/eqP => H_neq; case: ifP; move/eqP => //= H_eq.
Expand All @@ -333,7 +321,7 @@ Lemma procMsg_has_init_block:
has_init_block (blockTree (procMsg s1 from m ts).1).
Proof.
move=> s1 from m ts.
case Msg: m=>[|||b|||];
case Msg: m=>[||b|||];
destruct s1; rewrite/procMsg/=; do? by []; do? by case:ifP.
- by apply btExtendIB.
- move=>v vh; case: ifP => //=; move/eqP => H_neq; case: ifP; move/eqP => //= H_eq.
Expand Down Expand Up @@ -380,7 +368,7 @@ Lemma procMsg_non_block_nc_blockTree :
blockTree s1 = blockTree s2.
Proof.
move=>s1 from m ts neq.
case: m neq=>[|prs||b|t|sh|h] neq;
case: m neq=>[prs||b|t|sh|h] neq;
do? by[rewrite/procMsg; destruct s1=>/=].
- by specialize (neq b); contradict neq; rewrite eqxx.
- rewrite/procMsg/=; case: s1=>????/=; case:ifP => //=.
Expand Down