(* 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.