(* Definition and operations on IP addresses *) (* Venanzio Capretta and Bernard Stepien *) (* May 2006 *) (* Feb 2015: updated to Coq version 8.4 *) Require Import ZArith. Require Import Bool. Require Import Sumbool. (* Bits are identified with booleans, 0=false, 1=true *) Definition bit: Set := bool. Definition byte: Set := (bit*bit*bit*bit*bit*bit*bit*bit)%type. (* Test if an integer is not zero *) Definition bit0: Z -> bit := fun z => negb (Zeq_bool z 0). (* Binary representation of integers (smaller than 256). *) Definition Z_to_byte: Z -> byte := fun z => let (q1,r1):=(Zdiv_eucl z 2) in let (q2,r2):=(Zdiv_eucl q1 2) in let (q3,r3):=(Zdiv_eucl q2 2) in let (q4,r4):=(Zdiv_eucl q3 2) in let (q5,r5):=(Zdiv_eucl q4 2) in let (q6,r6):=(Zdiv_eucl q5 2) in let (q7,r7):=(Zdiv_eucl q6 2) in let (q8,r8):=(Zdiv_eucl q7 2) in (bit0 r8, bit0 r7, bit0 r6, bit0 r5, bit0 r4, bit0 r3, bit0 r2, bit0 r1). (* Definition of IP address, a four-tuple of bytes *) Definition ip_address:Set := (byte*byte*byte*byte)%type. (* Construction of an IP address from four integers *) Definition ip: Z -> Z -> Z -> Z -> ip_address := fun z1 z2 z3 z4 => (Z_to_byte z1, Z_to_byte z2, Z_to_byte z3, Z_to_byte z4). (* A range of IP addresses is specified by a base address and a mask *) Record ip_range: Set := mk_range { ip_base: ip_address; ip_mask: ip_address }. Definition bit_match: bit -> bit -> bit -> Prop := fun b bb bm => bm=true \/ b=bb. Definition byte_match: byte -> byte -> byte -> Prop := fun b bb bm => match b with (((((((b1,b2),b3),b4),b5),b6),b7),b8) => match bb with (((((((bb1,bb2),bb3),bb4),bb5),bb6),bb7),bb8) => match bm with (((((((bm1,bm2),bm3),bm4),bm5),bm6),bm7),bm8) => bit_match b1 bb1 bm1 /\ bit_match b2 bb2 bm2 /\ bit_match b3 bb3 bm3 /\ bit_match b4 bb4 bm4/\ bit_match b5 bb5 bm5 /\ bit_match b6 bb6 bm6 /\ bit_match b7 bb7 bm7 /\ bit_match b8 bb8 bm8 end end end. (* This specifies when an ip_address is in an ip_range. *) Definition ip_match: ip_address -> ip_range -> Prop := fun ip ipr => match ip with (((ip1,ip2),ip3),ip4) => match (ip_base ipr) with (((ipb1,ipb2),ipb3),ipb4) => match (ip_mask ipr) with (((ipm1,ipm2),ipm3),ipm4) => byte_match ip1 ipb1 ipm1 /\ byte_match ip2 ipb2 ipm2 /\ byte_match ip3 ipb3 ipm3 /\ byte_match ip4 ipb4 ipm4 end end end. (* Suppose a1 is a bit from the base ip addres and m1 a bit from the mask, similarly for a2 and m2; then we check if there is an interesection. *) Definition bit_mask_bool: bit -> bit -> bit -> bit -> bool := fun a1 m1 a2 m2 => orb m1 (orb m2 (eqb a1 a2)). (* Similarly for bytes *) Definition byte_mask_bool: byte -> byte -> byte -> byte -> bool := fun a1 m1 a2 m2 => match a1 with (((((((a11,a12),a13),a14),a15),a16),a17),a18) => match m1 with (((((((m11,m12),m13),m14),m15),m16),m17),m18) => match a2 with (((((((a21,a22),a23),a24),a25),a26),a27),a28) => match m2 with (((((((m21,m22),m23),m24),m25),m26),m27),m28) => andb (bit_mask_bool a11 m11 a21 m21) ( andb (bit_mask_bool a12 m12 a22 m22) ( andb (bit_mask_bool a13 m13 a23 m23) ( andb (bit_mask_bool a14 m14 a24 m24) ( andb (bit_mask_bool a15 m15 a25 m25) ( andb (bit_mask_bool a16 m16 a26 m26) ( andb (bit_mask_bool a17 m17 a27 m27) (bit_mask_bool a18 m18 a28 m28) )))))) end end end end. (* Check if two ip ranges intersect. *) Definition ip_address_bool: ip_range -> ip_range -> bool := fun ip1 ip2 => match ip1 with (mk_range ipb1 ipm1) => match ipb1 with (((a11,a12),a13),a14) => match ipm1 with (((m11,m12),m13),m14) => match ip2 with (mk_range ipb2 ipm2) => match ipb2 with (((a21,a22),a23),a24) => match ipm2 with (((m21,m22),m23),m24) => andb (byte_mask_bool a11 m11 a21 m21) ( andb (byte_mask_bool a12 m12 a22 m22) ( andb (byte_mask_bool a13 m13 a23 m23) ( (byte_mask_bool a14 m14 a24 m24) ))) end end end end end end. Lemma bit_match_intersection: forall b1 m1 b2 m2: bit, (bit_mask_bool b1 m1 b2 m2)=true -> exists b:bit, bit_match b b1 m1 /\ bit_match b b2 m2. Proof. intros b1 m1 b2 m2; case m1. intros _; exists b2; split. left; trivial. right; trivial. case m2. intros _; exists b1; split. right; trivial. left; trivial. case b1; case b2; simpl; intro H; try (discriminate H). exists true; split; right; trivial. exists false; split; right; trivial. Qed. Lemma byte_mask_intersection: forall b1 m1 b2 m2:byte, (byte_mask_bool b1 m1 b2 m2)=true -> exists b:byte, byte_match b b1 m1 /\ byte_match b b2 m2. Proof. intros [[[[[[[b11 b12] b13] b14] b15] b16] b17] b18] [[[[[[[m11 m12] m13] m14] m15] m16] m17] m18] [[[[[[[b21 b22] b23] b24] b25] b26] b27] b28] [[[[[[[m21 m22] m23] m24] m25] m26] m27] m28]; simpl. intro H; generalize (andb_prop _ _ H); clear H; intros [H1 H]. generalize (andb_prop _ _ H); clear H; intros [H2 H]. generalize (andb_prop _ _ H); clear H; intros [H3 H]. generalize (andb_prop _ _ H); clear H; intros [H4 H]. generalize (andb_prop _ _ H); clear H; intros [H5 H]. generalize (andb_prop _ _ H); clear H; intros [H6 H]. generalize (andb_prop _ _ H); clear H; intros [H7 H8]. generalize (bit_match_intersection _ _ _ _ H1); intros [b1 [Hb11 Hb21]]. generalize (bit_match_intersection _ _ _ _ H2); intros [b2 [Hb12 Hb22]]. generalize (bit_match_intersection _ _ _ _ H3); intros [b3 [Hb13 Hb23]]. generalize (bit_match_intersection _ _ _ _ H4); intros [b4 [Hb14 Hb24]]. generalize (bit_match_intersection _ _ _ _ H5); intros [b5 [Hb15 Hb25]]. generalize (bit_match_intersection _ _ _ _ H6); intros [b6 [Hb16 Hb26]]. generalize (bit_match_intersection _ _ _ _ H7); intros [b7 [Hb17 Hb27]]. generalize (bit_match_intersection _ _ _ _ H8); intros [b8 [Hb18 Hb28]]. exists (((((((b1,b2),b3),b4),b5),b6),b7),b8); split; red; auto 8. Qed. (* For soundness. *) Lemma ip_range_intersection: forall ip1 ip2:ip_range, (ip_address_bool ip1 ip2)=true -> exists ip:ip_address, ip_match ip ip1 /\ ip_match ip ip2. Proof. intros [[[[b11 b12] b13] b14] [[[m11 m12] m13] m14]] [[[[b21 b22] b23] b24] [[[m21 m22] m23] m24]]; simpl. intro H; generalize (andb_prop _ _ H); clear H; intros [H1 H]. generalize (andb_prop _ _ H); clear H; intros [H2 H]. generalize (andb_prop _ _ H); clear H; intros [H3 H4]. generalize (byte_mask_intersection _ _ _ _ H1); intros [b1 [Hb11 Hb21]]. generalize (byte_mask_intersection _ _ _ _ H2); intros [b2 [Hb12 Hb22]]. generalize (byte_mask_intersection _ _ _ _ H3); intros [b3 [Hb13 Hb23]]. generalize (byte_mask_intersection _ _ _ _ H4); intros [b4 [Hb14 Hb24]]. exists (((b1,b2),b3),b4); split; red; simpl; auto 4. Qed. Definition ip_range_apart: ip_range -> ip_range -> Prop := fun ip1 ip2 => ip_address_bool ip1 ip2 = false. Lemma ip_range_dec: forall ip1 ip2, {ip_range_apart ip1 ip2}+{~ip_range_apart ip1 ip2}. Proof. intros ip1 ip2; unfold ip_range_apart; case (ip_address_bool ip1 ip2). right; discriminate. left; reflexivity. Defined. (* For completeness. *) Lemma intersection_bit_match: forall (b r1 m1 r2 m2:bit), bit_match b r1 m1 -> bit_match b r2 m2 -> bit_mask_bool r1 m1 r2 m2 = true. Proof. intros b r1 m1 r2 m2 H1 H2; case H1. intro Hm1; rewrite Hm1; trivial. intro Hr1; case H2. intro Hm2; rewrite Hm2; simpl. unfold bit_mask_bool; rewrite orb_b_true; trivial. intro Hr2; rewrite <- Hr1; rewrite <- Hr2; simpl. unfold bit_mask_bool; simpl. rewrite eqb_reflx. rewrite orb_b_true; rewrite orb_b_true; trivial. Qed. Lemma intersection_byte_match: forall (b r1 m1 r2 m2:byte), byte_match b r1 m1 -> byte_match b r2 m2 -> byte_mask_bool r1 m1 r2 m2 = true. Proof. intros [[[[[[[b1 b2] b3] b4] b5] b6] b7] b8] [[[[[[[r11 r12] r13] r14] r15] r16] r17] r18] [[[[[[[m11 m12] m13] m14] m15] m16] m17] m18] [[[[[[[r21 r22] r23] r24] r25] r26] r27] r28] [[[[[[[m21 m22] m23] m24] m25] m26] m27] m28]; simpl. intros [H11 [H12 [H13 [H14 [H15 [H16 [H17 H18]]]]]]] [H21 [H22 [H23 [H24 [H25 [H26 [H27 H28]]]]]]]. rewrite intersection_bit_match with (b:=b1); try assumption. rewrite intersection_bit_match with (b:=b2); try assumption. rewrite intersection_bit_match with (b:=b3); try assumption. rewrite intersection_bit_match with (b:=b4); try assumption. rewrite intersection_bit_match with (b:=b5); try assumption. rewrite intersection_bit_match with (b:=b6); try assumption. rewrite intersection_bit_match with (b:=b7); try assumption. rewrite intersection_bit_match with (b:=b8); try assumption. trivial. Qed. Lemma intersection_ip_range: forall (ip1 ip2:ip_range)(ip:ip_address), ip_match ip ip1 -> ip_match ip ip2 -> (ip_address_bool ip1 ip2)=true. Proof. intros [[[[r11 r12] r13] r14] [[[m11 m12] m13] m14]] [[[[r21 r22] r23] r24] [[[m21 m22] m23] m24]] [[[a1 a2] a3] a4]. simpl. intros [H11 [H12 [H13 H14]]] [H21 [H22 [H23 H24]]]. rewrite intersection_byte_match with (b:=a1); try assumption. rewrite intersection_byte_match with (b:=a2); try assumption. rewrite intersection_byte_match with (b:=a3); try assumption. rewrite intersection_byte_match with (b:=a4); try assumption. trivial. Qed.