(****************************************************************
   Michel St-Martin and Amy Felty
   December 2015, Coq version V8.4
                                                                 
   A Verified Algorithm for Detecting Conflicts in XACML Access
   Control Rules, Michel St-Martin and Amy P. Felty, In Proceedings of
   the Fifth ACM SIGPLAN Conference on Certified Programs and Proofs
   (CPP), January 2016.

  ***************************************************************)

Require Export RuleSet.

Open Scope Z_scope.

Lemma ThreePm_rc : 0 <= 54000 < MIDNIGHT.
Proof.
unfold MIDNIGHT; omega.
Qed.

Definition ThreePm:Z'NM := (exist _ 54000 ThreePm_rc).

Definition Request1 := (intReq 123)::(intReq 2)::
(intReq 0)::(timeReq ThreePm)::(intReq 1)::
(intReq 2)::(intReq 1)::nil.

Lemma ThreeAm_rc : 0 <= 10800 <= MIDNIGHT.
Proof.
unfold MIDNIGHT; omega.
Qed.

Lemma FourAm_rc : 0 <= 14400 <= MIDNIGHT.
Proof.
unfold MIDNIGHT; omega.
Qed.

Lemma SixAm_rc : 0 <= 21600 <= MIDNIGHT.
Proof.
unfold MIDNIGHT; omega.
Qed.

Lemma FivePm_rc : 0 <= 61200 <= MIDNIGHT.
Proof.
unfold MIDNIGHT; omega.
Qed.

Lemma ElevenPm_rc : 0 <= 82800 <= MIDNIGHT.
Proof.
unfold MIDNIGHT; omega.
Qed.

Definition intEq (z:Z)(n:nat):srac := single (intInRange z z) n.

Definition G123: srac := intEq 123 1.

Definition AILab := intEq 0 2.
Definition FMLab := intEq 1 2.
Definition GradLab := intEq 2 2.
Definition AnyLocation := single (any (intReq 0)) 2.

Definition Enter: srac := intEq 0 3.

Definition ThreeAm:Z' := (exist _ 10800 ThreeAm_rc).
Definition FourAm:Z' := (exist _ 14400 FourAm_rc).
Definition SixAm:Z' := (exist _ 21600 SixAm_rc).
Definition FivePm:Z' := (exist _ 61200 FivePm_rc).
Definition ElevenPm:Z' := (exist _ 82800 ElevenPm_rc).
Definition GlabHours:srac := not (single (timeInRange ThreeAm FourAm) 4).
Definition FMlabHours:srac := single (timeInRange SixAm ElevenPm) 4.
Definition After5:srac := single (timeInRange FivePm Z'MIDNIGHT) 4.
Definition AnyTime: srac := single (any (timeReq Z'NM0)) 4.

Definition NotRegistered := intEq 0 5.
(* Definition Violations := single (intGt 0) 6. *)
Definition Violations := intEq 123 1.

Definition Professors: srac := intEq 2 6.
Definition Grads: srac := intEq 1 6.

Definition Rule1 :=
  ruleCons permit (and (and (and (single (any (intReq 0)) 1) (intEq 4 2))
    Enter) FMlabHours).
Definition Rule2 := ruleCons permit (and (and (and (or Grads Professors) GradLab) Enter) GlabHours).
Definition Rule3 := ruleCons permit (and (and (and G123 FMLab) Enter) FMlabHours).
Definition Rule4 := ruleCons permit (and (and (and (intEq 456 1) AILab) Enter) GlabHours).
Definition Rule5 := ruleCons deny (and (and (and NotRegistered (or FMLab AILab)) Enter) AnyTime).
Definition Rule6 := ruleCons deny (and (and (and Violations AnyLocation) Enter) After5).

Definition setOfRules := Rule1::Rule2::Rule3::Rule4::Rule5::Rule6::nil.

Open Scope nat_scope.

Lemma test: (find_conflicts setOfRules) = (0, 5) :: (1, 5) :: (2, 4) :: (2, 5) :: (3, 4) :: nil.
Proof.
unfold setOfRules.
unfold find_conflicts.
unfold conflicts_aux.
simpl.
unfold toLists.
unfold convertDNF.
unfold Grads, Professors, GradLab, Enter, GlabHours, Violations, AnyLocation, After5.
unfold G123, AnyTime, NotRegistered, FMLab, FMlabHours, AILab.
unfold intEq.

repeat unfoldRemoveNotsG.
simpl.
trivial.
Qed.