(* * Copyright © 2023 Mark Raynsford <code@io7m.com> https://www.io7m.com * * Permission to use, copy, modify, and/or distribute this software for any * purpose with or without fee is hereby granted, provided that the above * copyright notice and this permission notice appear in all copies. * * THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES * WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF * MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR ANY * SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES * WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN * ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF OR * IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE. *) Require Import Coq.Strings.String. Require Import Medrina.Names. (** The type of action names. *) Record actionName := ANMake { (** The name of the action. *) anName : string; (** Action names are valid. *) anValid : validName anName }. Require Import Coq.Logic.ProofIrrelevance. (** Equality of action names is decidable. *) Theorem actionNameDec : forall (a b : actionName), {a = b}+{a <> b}. Proof. intros a b. destruct a as [a0 [a1 [a2 a3]]]. destruct b as [b0 [b1 [b2 b3]]]. destruct (string_dec a0 b0) as [H0|H1]. { subst b0. left. assert (a1 = b1) by apply proof_irrelevance. subst b1. assert (a2 = b2) by apply proof_irrelevance. subst b2. assert (a3 = b3) by apply proof_irrelevance. subst b3. intuition. } { right. congruence. } Qed. (** Proof irrelevance allows for equality between instances with equal names. *) Theorem actionNameIrrelevance : forall (a b : actionName), anName a = anName b -> a = b. Proof. intros a b Heq. destruct a as [a0 a1]. destruct b as [b0 b1]. simpl in Heq. subst b0. assert (a1 = b1) by apply proof_irrelevance. subst b1. reflexivity. Qed. #[export] Instance actionNameName : IsValidName actionName := { ivName := anName; ivValid := anValid; ivIrrelevantEqual := actionNameIrrelevance }. (** The type of actions. *) Record action : Set := AMake { aName : actionName }.
(* * Copyright © 2023 Mark Raynsford <code@io7m.com> https://www.io7m.com * * Permission to use, copy, modify, and/or distribute this software for any * purpose with or without fee is hereby granted, provided that the above * copyright notice and this permission notice appear in all copies. * * THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES * WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF * MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR ANY * SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES * WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN * ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF OR * IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE. *) Require Import Coq.Strings.String. Require Import Coq.Logic.FunctionalExtensionality. Require Import com.io7m.lanark.core.Lanark. (** The type of attribute names. *) Record attributeName := ANMake { (** The name of the attribute. *) anName : name; (** Attribute names are valid. *) anValid : nameValid anName }. Require Import Coq.Logic.ProofIrrelevance. (** Equality of attribute names is decidable. *) Theorem attributeNameDec : forall (a b : attributeName), {a = b}+{a <> b}. Proof. intros a b. destruct a as [a0 a1]. destruct b as [b0 b1]. destruct (nameDec a0 b0) as [H0|H1]. { subst b0. left. assert (a1 = b1) by apply proof_irrelevance. subst b1. reflexivity. } { right. congruence. } Qed. (** The type of attribute values. *) Record attributeValue := AVMake { (** The value of the attribute. *) avValue : name; (** Attribute values are valid. *) avValid : nameValid avValue }. (** Equality of attribute values is decidable. *) Theorem attributeValueDec : forall (a b : attributeValue), {a = b}+{a <> b}. Proof. intros a b. destruct a as [a0 a1]. destruct b as [b0 b1]. destruct (nameDec a0 b0) as [H0|H1]. { subst b0. left. assert (a1 = b1) by apply proof_irrelevance. subst b1. reflexivity. } { right. congruence. } Qed. (** Boolean equality of attribute values. *) Definition attributeValueBool (a b : attributeValue) : bool := match attributeValueDec a b with | left _ => true | right _ => false end. Theorem attributeValueBoolDecT : forall (a b : attributeValue), a = b <-> attributeValueBool a b = true. Proof. intros a b. split. { intros Heq. subst b. unfold attributeValueBool. destruct (attributeValueDec a a) eqn:Hdec. - reflexivity. - contradiction. } { unfold attributeValueBool. destruct (attributeValueDec a b). - intros. auto. - intros H0. contradict H0. discriminate. } Qed. Theorem attributeValueBoolDecF : forall (a b : attributeValue), a <> b <-> attributeValueBool a b = false. Proof. intros a b. split. { intros Heq. unfold attributeValueBool. destruct (attributeValueDec a b) eqn:Hdec. - contradiction. - reflexivity. } { unfold attributeValueBool. destruct (attributeValueDec a b). - intros H0. contradict H0. discriminate. - intros. auto. } Qed. Require Import Coq.FSets.FMapInterface. Require Import Coq.FSets.FMapWeakList. Require Import Coq.FSets.FMapFacts. Require Import Coq.Structures.Equalities. (** A mini decidable type module to instantiate maps. *) Module AttributeNameMiniDec : MiniDecidableType with Definition t := attributeName. Definition t := attributeName. Definition eq := @Logic.eq t. Definition eq_refl := @Logic.eq_refl t. Definition eq_sym := @Logic.eq_sym t. Definition eq_trans := @Logic.eq_trans t. Theorem eq_dec : forall x y : t, {eq x y} + {~ eq x y}. Proof. apply attributeNameDec. Qed. End AttributeNameMiniDec. (** A usual decidable type module to instantiate maps. *) Module AttributeNameDec <: UsualDecidableType with Definition t := attributeName with Definition eq := @Logic.eq attributeName := Make_UDT AttributeNameMiniDec. (** A Maps module with attribute name keys. *) Module AttributeNameMaps : FMapInterface.WS with Definition E.t := attributeName with Definition E.eq := @Logic.eq attributeName := FMapWeakList.Make AttributeNameDec. Module AttributeNameMapsFacts := Facts AttributeNameMaps. Lemma AttributeNameMapsEqEquiv : Equivalence (AttributeNameMaps.eq_key_elt (elt:=attributeValue)). Proof. unfold AttributeNameMaps.eq_key_elt. constructor. { constructor; reflexivity. } { intros x y [Heq0 Heq1]. symmetry in Heq0. symmetry in Heq1. intuition. } { intros x y z [Heq0 Heq1] [Heq2 Heq3]. rewrite Heq1. rewrite Heq3. rewrite <- Heq2. rewrite Heq0. constructor; reflexivity. } Qed. Lemma AttributeNameMapsEqLeibniz : forall p0 p1, AttributeNameMaps.eq_key_elt (elt:=attributeValue) p0 p1 <-> p0 = p1. Proof. unfold AttributeNameMaps.eq_key_elt. intros p0. intros p1. destruct p0 as [p0k p0v]. destruct p1 as [p1k p1v]. simpl. unfold AttributeNameMaps.E.eq. split. { intros [Heq0 Heq1]. subst p0k. subst p0v. reflexivity. } { intros Heq0. assert (p0k = p1k) by congruence. assert (p0v = p1v) by congruence. intuition. } Qed. Lemma attributesEmptyElements : AttributeNameMaps.elements (AttributeNameMaps.empty attributeValue) = nil. Proof. destruct (AttributeNameMaps.elements (AttributeNameMaps.empty _)) eqn:H. { reflexivity. } { assert (In p (AttributeNameMaps.elements (AttributeNameMaps.empty _))) as Hin. { rewrite H. intuition. } assert (InA (AttributeNameMaps.eq_key_elt (elt:=attributeValue)) p (AttributeNameMaps.elements (AttributeNameMaps.empty attributeValue)) ) as H0. { apply In_InA. exact AttributeNameMapsEqEquiv. exact Hin. } destruct p as [k v]. rewrite <- AttributeNameMapsFacts.elements_mapsto_iff in H0. rewrite AttributeNameMapsFacts.empty_mapsto_iff in H0. contradiction. } Qed.
(* * Copyright © 2023 Mark Raynsford <code@io7m.com> https://www.io7m.com * * Permission to use, copy, modify, and/or distribute this software for any * purpose with or without fee is hereby granted, provided that the above * copyright notice and this permission notice appear in all copies. * * THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES * WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF * MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR ANY * SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES * WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN * ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF OR * IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE. *) Require Import Coq.Strings.String. Require Import Coq.Lists.List. Require Import Coq.Lists.SetoidList. Import ListNotations. Require Import Medrina.Actions. Require Import Medrina.Attributes. Require Import Medrina.Names. Require Import Medrina.Subjects. Require Import Medrina.Roles. Require Import Medrina.Objects. (** An expression that matches a subject. *) Inductive exprMatchSubject : Type := | EMS_False : exprMatchSubject | EMS_True : exprMatchSubject | EMS_WithRolesAll : RoleSets.t -> exprMatchSubject | EMS_WithRolesAny : RoleSets.t -> exprMatchSubject | EMS_And : list exprMatchSubject -> exprMatchSubject | EMS_Or : list exprMatchSubject -> exprMatchSubject . Section ExprMatchSubjects_ind. Variable P : exprMatchSubject -> Prop. Hypothesis P_False : P EMS_False. Hypothesis P_True : P EMS_True. Hypothesis P_WithRolesAll : forall r, P (EMS_WithRolesAll r). Hypothesis P_WithRolesAny : forall r, P (EMS_WithRolesAny r). Hypothesis P_And : forall es, Forall P es -> P (EMS_And es). Hypothesis P_Or : forall es, Forall P es -> P (EMS_Or es). Fixpoint exprMatchSubject_extendedInd (e : exprMatchSubject) : P e := let fix e_list (xs : list exprMatchSubject) : Forall P xs := match xs as rxs return (Forall P rxs) with | [] => Forall_nil _ | (y :: ys) => @Forall_cons _ _ y ys (exprMatchSubject_extendedInd y) (e_list ys) end in match e with | EMS_False => P_False | EMS_True => P_True | EMS_WithRolesAll r => P_WithRolesAll r | EMS_WithRolesAny r => P_WithRolesAny r | EMS_And es => P_And es (e_list es) | EMS_Or es => P_Or es (e_list es) end. End ExprMatchSubjects_ind. (** An evaluation function for subject match expressions. *) Fixpoint exprMatchSubjectEvalF (s : subject) (e : exprMatchSubject) : bool := match e with | EMS_False => false | EMS_True => true | EMS_WithRolesAll r => RoleSets.subset r (sRoles s) | EMS_WithRolesAny r => RoleSets.exists_ (fun x => RoleSets.mem x (sRoles s)) r | EMS_And es => forallb (exprMatchSubjectEvalF s) es | EMS_Or es => existsb (exprMatchSubjectEvalF s) es end. (** The evaluation function for subject match expressions as a relation. *) Inductive exprMatchSubjectEvalR (s : subject) : exprMatchSubject -> Prop := | EMSR_True : exprMatchSubjectEvalR s EMS_True | EMSR_WithRolesAll : forall (r : RoleSets.t), RoleSets.Subset r (sRoles s) -> exprMatchSubjectEvalR s (EMS_WithRolesAll r) | EMSR_WithRolesAny : forall (r : RoleSets.t), (exists x, RoleSets.In x r /\ RoleSets.In x (sRoles s)) -> exprMatchSubjectEvalR s (EMS_WithRolesAny r) | EMSR_And : forall (es : list exprMatchSubject), Forall (exprMatchSubjectEvalR s) es -> exprMatchSubjectEvalR s (EMS_And es) | EMSR_Or : forall (es : list exprMatchSubject), Exists (exprMatchSubjectEvalR s) es -> exprMatchSubjectEvalR s (EMS_Or es) . (** Implication lifted into the Forall structure. *) Lemma Forall_impl_lifted : forall (A : Type) (P : A -> Prop) (Q : A -> Prop) (xs : list A), Forall (fun x => P x) xs -> Forall (fun x => P x -> Q x) xs -> Forall (fun x => Q x) xs. Proof. induction xs as [|y ys IH]. { intros F0 H1. constructor. } { intros F0 F1. constructor. { apply (Forall_inv F1). apply (Forall_inv F0). } { apply IH. apply (Forall_inv_tail F0). apply (Forall_inv_tail F1). } } Qed. Lemma exprMatchSubjectEvalEquivalent_FR_T : forall s e, true = exprMatchSubjectEvalF s e -> exprMatchSubjectEvalR s e. Proof. intros s e. induction e as [ | | | |es Hes |es Hes ] using exprMatchSubject_extendedInd. { (* EMS_False *) intros Ht. inversion Ht. } { (* EMS_True *) intros Ht. constructor. } { (* EMS_WithRolesAll *) intros Ht. unfold exprMatchSubjectEvalF in Ht. constructor. apply RoleSets.subset_2. intuition. } { (* EMS_WithRolesAny *) intros Ht. unfold exprMatchSubjectEvalF in Ht. constructor. symmetry in Ht. assert ( SetoidList.compat_bool RoleSets.E.eq (fun x : RoleSets.elt => RoleSets.mem x (sRoles s)) ) as Hsetcomp. { unfold SetoidList.compat_bool. unfold Morphisms.Proper. unfold Morphisms.respectful. intros x y Heq. rewrite Heq. reflexivity. } pose proof (RoleSets.exists_2 Hsetcomp Ht) as [x [H0 H1]]. exists x. intuition. } { (* EMS_And *) destruct es as [|y ys]. { intros Ht. constructor. constructor. } { simpl. intros Ht. (* We need to show that the relation holds for all (y :: ys). *) assert (Forall (exprMatchSubjectEvalR s) (y :: ys)) as H0. { (* We do this by showing it holds for y... *) assert (exprMatchSubjectEvalR s y) as H1. { symmetry in Ht. rewrite Bool.andb_true_iff in Ht. rewrite forallb_forall in Ht. destruct Ht as [HT0 HT1]. rewrite <- (@Forall_forall exprMatchSubject _ ys) in HT1. apply (Forall_inv Hes). symmetry. exact HT0. } (* ... And for all ys. *) assert (Forall (exprMatchSubjectEvalR s) ys) as H2. { symmetry in Ht. rewrite Bool.andb_true_iff in Ht. rewrite forallb_forall in Ht. destruct Ht as [HT0 HT1]. rewrite <- (@Forall_forall exprMatchSubject _ ys) in HT1. assert (Forall (fun x : exprMatchSubject => true = exprMatchSubjectEvalF s x) ys) as H2. { rewrite Forall_forall. symmetry. generalize dependent x. rewrite <- Forall_forall. exact HT1. } pose proof (Forall_inv_tail Hes) as HesT. apply (Forall_impl_lifted _ _ _ ys H2 HesT). } (* ... And then composing the two. *) constructor. exact H1. exact H2. } constructor. exact H0. } } { (* EMS_Or *) destruct es as [|y ys]. { intros Ht. contradict Ht. simpl. discriminate. } { intros Ht. (* We need to show that the relation holds for y or something in ys. *) constructor. simpl in Ht. symmetry in Ht. destruct (Bool.orb_true_elim _ _ Ht) as [HtL|HtR]. { constructor. apply (Forall_inv Hes). auto. } { assert (Exists (exprMatchSubjectEvalR s) (y :: ys)) as H0. { rewrite existsb_exists in HtR. destruct HtR as [k [Htk0 Htk1]]. rewrite Forall_forall in Hes. pose proof (in_cons y k ys Htk0) as H0. pose proof (Hes k H0 (eq_sym Htk1)) as H1. apply Exists_cons_tl. rewrite Exists_exists. exists k. auto. } exact H0. } } } Qed. Lemma exprMatchSubjectEvalEquivalent_RF_T : forall s e, exprMatchSubjectEvalR s e -> true = exprMatchSubjectEvalF s e. Proof. intros s e. induction e as [ | | | |es Hes |es Hes ] using exprMatchSubject_extendedInd. { (* EMS_False *) intros Ht. inversion Ht. } { (* EMS_True *) intros Ht. reflexivity. } { (* EMS_WithRolesAll *) intros Ht. symmetry. apply RoleSets.subset_1. inversion Ht. intuition. } { (* EMS_WithRolesAny *) intros Ht. symmetry. inversion Ht as [ | |s0 Hexist Heq| | ]. subst s0. simpl. assert ( RoleSets.Exists (fun x : RoleSets.elt => RoleSets.mem x (sRoles s) = true) r ) as Hex. { unfold RoleSets.Exists. destruct Hexist as [y [Hy0 Hy1]]. exists y. intuition. } assert ( SetoidList.compat_bool RoleSets.E.eq (fun x : RoleSets.elt => RoleSets.mem x (sRoles s)) ) as Hsetcomp. { unfold SetoidList.compat_bool. unfold Morphisms.Proper. unfold Morphisms.respectful. intros x y Heq. rewrite Heq. reflexivity. } apply (RoleSets.exists_1 Hsetcomp Hex). } { (* EMS_And *) intros Ht. inversion Ht as [ | | |es0 Hfa Heq|]. subst es0. simpl. symmetry. rewrite forallb_forall. intros x Hin. symmetry. generalize dependent x. rewrite <- Forall_forall. apply (Forall_impl_lifted exprMatchSubject _ _ es Hfa Hes). } { (* EMS_Or *) intros Ht. symmetry. simpl. rewrite existsb_exists. inversion Ht as [ | | | |es0 Hex Heq]. subst es. destruct Hex as [k ks Hk|k ks Hk]. { exists k. constructor. constructor; reflexivity. apply (eq_sym (Forall_inv Hes Hk)). } { rewrite Exists_exists in Hk. destruct Hk as [q [Hq0 Hq1]]. exists q. constructor. apply (in_cons k q ks Hq0). pose proof (Forall_inv_tail Hes) as HesT. rewrite Forall_forall in HesT. apply (eq_sym (HesT q Hq0 Hq1)). } } Qed. (** The evaluation function and the evaluation relation are equivalent. *) Theorem exprMatchSubjectEvalEquivalentT : forall s e, true = exprMatchSubjectEvalF s e <-> exprMatchSubjectEvalR s e. Proof. split. apply exprMatchSubjectEvalEquivalent_FR_T. apply exprMatchSubjectEvalEquivalent_RF_T. Qed. Lemma exprMatchSubjectEvalEquivalent_FR_F : forall s e, false = exprMatchSubjectEvalF s e -> ~exprMatchSubjectEvalR s e. Proof. intros s e. induction e as [ | | | |es Hes |es Hes ] using exprMatchSubject_extendedInd. { (* EMS_False *) intros Ht. intro Hcontra. inversion Hcontra. } { (* EMS_True *) intros Ht. contradict Ht. discriminate. } { (* EMS_WithRolesAll *) intros Ht. intros Hcontra. rewrite <- (exprMatchSubjectEvalEquivalent_RF_T _ _ Hcontra) in Ht. contradict Ht; discriminate. } { (* EMS_WithRolesAny *) intros Ht. intros Hcontra. rewrite <- (exprMatchSubjectEvalEquivalent_RF_T _ _ Hcontra) in Ht. contradict Ht; discriminate. } { (* EMS_And *) intros Ht. intros Hcontra. rewrite <- (exprMatchSubjectEvalEquivalent_RF_T _ _ Hcontra) in Ht. contradict Ht; discriminate. } { (* EMS_Or *) intros Ht. intros Hcontra. rewrite <- (exprMatchSubjectEvalEquivalent_RF_T _ _ Hcontra) in Ht. contradict Ht; discriminate. } Qed. Lemma exprMatchSubjectEvalEquivalent_RF_F : forall s e, ~exprMatchSubjectEvalR s e -> false = exprMatchSubjectEvalF s e. Proof. intros s e. induction e as [ | | | |es Hes |es Hes ] using exprMatchSubject_extendedInd. { (* EMS_False *) intros Ht. reflexivity. } { (* EMS_True *) intros Ht. contradict Ht. constructor. } { (* EMS_WithRolesAll *) intros Ht. simpl. assert (~RoleSets.Subset r (sRoles s)) as Hns. { intros Hcontra. apply Ht. constructor. exact Hcontra. } symmetry. rewrite <- roleSubsetFalse. intuition. } { (* EMS_WithRolesAny *) intros Ht. symmetry. intuition. simpl. assert ( SetoidList.compat_bool RoleSets.E.eq (fun x : RoleSets.elt => RoleSets.mem x (sRoles s)) ) as Hsetcomp. { unfold SetoidList.compat_bool. unfold Morphisms.Proper. unfold Morphisms.respectful. intros x y Heq. rewrite Heq. reflexivity. } rewrite <- (roleExistsFalse r _ Hsetcomp). intro Hcontra. apply Ht. constructor. inversion Hcontra as [z [Hz0 Hz1]]. exists z. intuition. } { (* EMS_And *) intros Ht. destruct (exprMatchSubjectEvalF s (EMS_And es)) eqn:H. { symmetry in H. rewrite exprMatchSubjectEvalEquivalentT in H. contradiction. } { reflexivity. } } { (* EMS_Or *) intros Ht. destruct (exprMatchSubjectEvalF s (EMS_Or es)) eqn:H. { symmetry in H. rewrite exprMatchSubjectEvalEquivalentT in H. contradiction. } { reflexivity. } } Qed. (** The evaluation function and the evaluation relation are equivalent. *) Theorem exprMatchSubjectEvalEquivalentF : forall s e, false = exprMatchSubjectEvalF s e <-> ~exprMatchSubjectEvalR s e. Proof. split. apply exprMatchSubjectEvalEquivalent_FR_F. apply exprMatchSubjectEvalEquivalent_RF_F. Qed. (** The evaluation relation is decidable. *) Theorem exprMatchSubjectEvalRDec : forall s e, {exprMatchSubjectEvalR s e}+{~exprMatchSubjectEvalR s e}. Proof. intros s e. destruct (exprMatchSubjectEvalF s e) eqn:Hev. { symmetry in Hev. rewrite exprMatchSubjectEvalEquivalentT in Hev. left; intuition. } { symmetry in Hev. rewrite exprMatchSubjectEvalEquivalentF in Hev. right; intuition. } Qed. Theorem exprMatchSubjectEvalRolesAllEmpty : forall s, true = exprMatchSubjectEvalF s (EMS_WithRolesAll RoleSets.empty). Proof. intros s. simpl. symmetry. rewrite <- RoleSetsFacts.subset_iff. unfold RoleSets.Subset. intros x Hin. rewrite RoleSetsFacts.empty_iff in Hin. contradiction. Qed. Theorem exprMatchSubjectEvalRolesAnyEmpty : forall s, false = exprMatchSubjectEvalF s (EMS_WithRolesAny RoleSets.empty). Proof. intros s. simpl. symmetry. rewrite <- roleExistsFalse. unfold RoleSets.Exists. unfold not. intros [x [Hcontra0 Hcontra1]]. rewrite RoleSetsFacts.empty_iff in Hcontra0. exact Hcontra0. unfold compat_bool. intuition. Qed. (** An expression that matches an action. *) Inductive exprMatchAction : Type := | EMA_False : exprMatchAction | EMA_True : exprMatchAction | EMA_WithName : actionName -> exprMatchAction | EMA_And : list exprMatchAction -> exprMatchAction | EMA_Or : list exprMatchAction -> exprMatchAction . (** An evaluation function for action match expressions. *) Fixpoint exprMatchActionEvalF (a : action) (e : exprMatchAction) : bool := match e with | EMA_False => false | EMA_True => true | EMA_WithName n => eqb (ivName (aName a)) (ivName n) | EMA_And xs => forallb (exprMatchActionEvalF a) xs | EMA_Or xs => existsb (exprMatchActionEvalF a) xs end. (** The evaluation function for action match expressions as a relation. *) Inductive exprMatchActionEvalR (a : action) : exprMatchAction -> Prop := | EMAR_True : exprMatchActionEvalR a EMA_True | EMAR_WithName : forall (x : actionName), ivName (aName a) = ivName x -> exprMatchActionEvalR a (EMA_WithName x) | EMAR_And : forall (es : list exprMatchAction), Forall (exprMatchActionEvalR a) es -> exprMatchActionEvalR a (EMA_And es) | EMAR_Or : forall (es : list exprMatchAction), Exists (exprMatchActionEvalR a) es -> exprMatchActionEvalR a (EMA_Or es) . Section ExprMatchAction_ind. Variable P : exprMatchAction -> Prop. Hypothesis P_False : P EMA_False. Hypothesis P_True : P EMA_True. Hypothesis P_WithName : forall n, P (EMA_WithName n). Hypothesis P_And : forall es, Forall P es -> P (EMA_And es). Hypothesis P_Or : forall es, Forall P es -> P (EMA_Or es). Fixpoint exprMatchAction_extendedInd (e : exprMatchAction) : P e := let fix e_list (xs : list exprMatchAction) : Forall P xs := match xs as rxs return (Forall P rxs) with | [] => Forall_nil _ | (y :: ys) => @Forall_cons _ _ y ys (exprMatchAction_extendedInd y) (e_list ys) end in match e with | EMA_False => P_False | EMA_True => P_True | EMA_WithName a => P_WithName a | EMA_And es => P_And es (e_list es) | EMA_Or es => P_Or es (e_list es) end. End ExprMatchAction_ind. Lemma exprMatchActionEvalEquivalent_FR_T : forall s e, true = exprMatchActionEvalF s e -> exprMatchActionEvalR s e. Proof. intros s e. induction e as [ | | |es Hes |es Hes ] using exprMatchAction_extendedInd. { (* EMA_False *) intros Ht. inversion Ht. } { (* EMA_True *) intros Ht. constructor. } { (* EMA_WithName *) intros Ht. unfold exprMatchActionEvalF in Ht. symmetry in Ht. rewrite eqb_eq in Ht. pose proof (ivIrrelevantEqual _ _ Ht) as H. subst n. constructor. reflexivity. } { (* EMA_And *) destruct es as [|y ys]. { intros Ht. constructor. constructor. } { simpl. intros Ht. (* We need to show that the relation holds for all (y :: ys). *) assert (Forall (exprMatchActionEvalR s) (y :: ys)) as H0. { (* We do this by showing it holds for y... *) assert (exprMatchActionEvalR s y) as H1. { symmetry in Ht. rewrite Bool.andb_true_iff in Ht. rewrite forallb_forall in Ht. destruct Ht as [HT0 HT1]. rewrite <- (@Forall_forall exprMatchAction _ ys) in HT1. apply (Forall_inv Hes). symmetry. exact HT0. } (* ... And for all ys. *) assert (Forall (exprMatchActionEvalR s) ys) as H2. { symmetry in Ht. rewrite Bool.andb_true_iff in Ht. rewrite forallb_forall in Ht. destruct Ht as [HT0 HT1]. rewrite <- (@Forall_forall exprMatchAction _ ys) in HT1. assert (Forall (fun x => true = exprMatchActionEvalF s x) ys) as H2. { rewrite Forall_forall. symmetry. generalize dependent x. rewrite <- Forall_forall. exact HT1. } pose proof (Forall_inv_tail Hes) as HesT. apply (Forall_impl_lifted _ _ _ ys H2 HesT). } (* ... And then composing the two. *) constructor. exact H1. exact H2. } constructor. exact H0. } } { (* EMA_Or *) destruct es as [|y ys]. { intros Ht. contradict Ht. simpl. discriminate. } { intros Ht. (* We need to show that the relation holds for y or something in ys. *) constructor. simpl in Ht. symmetry in Ht. destruct (Bool.orb_true_elim _ _ Ht) as [HtL|HtR]. { constructor. apply (Forall_inv Hes). auto. } { assert (Exists (exprMatchActionEvalR s) (y :: ys)) as H0. { rewrite existsb_exists in HtR. destruct HtR as [k [Htk0 Htk1]]. rewrite Forall_forall in Hes. pose proof (in_cons y k ys Htk0) as H0. pose proof (Hes k H0 (eq_sym Htk1)) as H1. apply Exists_cons_tl. rewrite Exists_exists. exists k. auto. } exact H0. } } } Qed. Lemma exprMatchActionEvalEquivalent_RF_T : forall s e, exprMatchActionEvalR s e -> true = exprMatchActionEvalF s e. Proof. intros s e. induction e as [ | | |es Hes |es Hes ] using exprMatchAction_extendedInd. { (* EMA_False *) intros Ht. inversion Ht. } { (* EMA_True *) intros Ht. reflexivity. } { (* EMA_WithName *) intros Ht. simpl. inversion Ht as [ |y Hyz| | ]. subst y. pose proof (ivIrrelevantEqual _ _ Hyz) as H0. rewrite H0. symmetry. apply eqb_refl. } { (* EMA_And *) intros Ht. inversion Ht as [ | |es0 Hfa Heq|]. subst es0. simpl. symmetry. rewrite forallb_forall. intros x Hin. symmetry. generalize dependent x. rewrite <- Forall_forall. apply (Forall_impl_lifted exprMatchAction _ _ es Hfa Hes). } { (* EMA_Or *) intros Ht. symmetry. simpl. rewrite existsb_exists. inversion Ht as [ | | |es0 Hex Heq]. subst es. destruct Hex as [k ks Hk|k ks Hk]. { exists k. constructor. constructor; reflexivity. apply (eq_sym (Forall_inv Hes Hk)). } { rewrite Exists_exists in Hk. destruct Hk as [q [Hq0 Hq1]]. exists q. constructor. apply (in_cons k q ks Hq0). pose proof (Forall_inv_tail Hes) as HesT. rewrite Forall_forall in HesT. apply (eq_sym (HesT q Hq0 Hq1)). } } Qed. (** The evaluation function and the evaluation relation are equivalent. *) Theorem exprMatchActionEvalEquivalentT : forall s e, true = exprMatchActionEvalF s e <-> exprMatchActionEvalR s e. Proof. split. apply exprMatchActionEvalEquivalent_FR_T. apply exprMatchActionEvalEquivalent_RF_T. Qed. Lemma exprMatchActionEvalEquivalent_FR_F : forall a e, false = exprMatchActionEvalF a e -> ~exprMatchActionEvalR a e. Proof. intros s e. induction e as [ | | |es Hes |es Hes ] using exprMatchAction_extendedInd. { (* EMA_False *) intros Ht. intro Hcontra. inversion Hcontra. } { (* EMA_True *) intros Ht. contradict Ht. discriminate. } { (* EMA_WithName *) intros Ht. intros Hcontra. rewrite <- (exprMatchActionEvalEquivalent_RF_T _ _ Hcontra) in Ht. contradict Ht; discriminate. } { (* EMS_And *) intros Ht. intros Hcontra. rewrite <- (exprMatchActionEvalEquivalent_RF_T _ _ Hcontra) in Ht. contradict Ht; discriminate. } { (* EMS_Or *) intros Ht. intros Hcontra. rewrite <- (exprMatchActionEvalEquivalent_RF_T _ _ Hcontra) in Ht. contradict Ht; discriminate. } Qed. Lemma exprMatchActionEvalEquivalent_RF_F : forall a e, ~exprMatchActionEvalR a e -> false = exprMatchActionEvalF a e. Proof. intros s e. induction e as [ | | |es Hes |es Hes ] using exprMatchAction_extendedInd. { (* EMA_False *) intros Ht. reflexivity. } { (* EMA_True *) intros Ht. contradict Ht. constructor. } { (* EMS_WithName *) intros Ht. destruct (exprMatchActionEvalF s (EMA_WithName n)) eqn:H. { symmetry in H. rewrite exprMatchActionEvalEquivalentT in H. contradiction. } { reflexivity. } } { (* EMS_And *) intros Ht. destruct (exprMatchActionEvalF s (EMA_And es)) eqn:H. { symmetry in H. rewrite exprMatchActionEvalEquivalentT in H. contradiction. } { reflexivity. } } { (* EMS_Or *) intros Ht. destruct (exprMatchActionEvalF s (EMA_Or es)) eqn:H. { symmetry in H. rewrite exprMatchActionEvalEquivalentT in H. contradiction. } { reflexivity. } } Qed. (** The evaluation function and the evaluation relation are equivalent. *) Theorem exprMatchActionEvalEquivalentF : forall a e, false = exprMatchActionEvalF a e <-> ~exprMatchActionEvalR a e. Proof. split. apply exprMatchActionEvalEquivalent_FR_F. apply exprMatchActionEvalEquivalent_RF_F. Qed. (** The evaluation relation is decidable. *) Theorem exprMatchActionEvalRDec : forall a e, {exprMatchActionEvalR a e}+{~exprMatchActionEvalR a e}. Proof. intros a e. destruct (exprMatchActionEvalF a e) eqn:Hev. { symmetry in Hev. rewrite exprMatchActionEvalEquivalentT in Hev. left; intuition. } { symmetry in Hev. rewrite exprMatchActionEvalEquivalentF in Hev. right; intuition. } Qed. (** An expression that matches an object. *) Inductive exprMatchObject : Type := | EMO_False : exprMatchObject | EMO_True : exprMatchObject | EMO_WithType : typeName -> exprMatchObject | EMO_WithAttributesAll : AttributeNameMaps.t attributeValue -> exprMatchObject | EMO_WithAttributesAny : AttributeNameMaps.t attributeValue -> exprMatchObject | EMO_And : list exprMatchObject -> exprMatchObject | EMO_Or : list exprMatchObject -> exprMatchObject . Section ExprMatchObject_ind. Variable P : exprMatchObject -> Prop. Hypothesis P_False : P EMO_False. Hypothesis P_True : P EMO_True. Hypothesis P_WithType : forall n, P (EMO_WithType n). Hypothesis P_WithAttributesAll : forall n, P (EMO_WithAttributesAll n). Hypothesis P_WithAttributesAny : forall n, P (EMO_WithAttributesAny n). Hypothesis P_And : forall es, Forall P es -> P (EMO_And es). Hypothesis P_Or : forall es, Forall P es -> P (EMO_Or es). Fixpoint exprMatchObject_extendedInd (e : exprMatchObject) : P e := let fix e_list (xs : list exprMatchObject) : Forall P xs := match xs as rxs return (Forall P rxs) with | [] => Forall_nil _ | (y :: ys) => @Forall_cons _ _ y ys (exprMatchObject_extendedInd y) (e_list ys) end in match e with | EMO_False => P_False | EMO_True => P_True | EMO_WithType a => P_WithType a | EMO_WithAttributesAll a => P_WithAttributesAll a | EMO_WithAttributesAny a => P_WithAttributesAny a | EMO_And es => P_And es (e_list es) | EMO_Or es => P_Or es (e_list es) end. End ExprMatchObject_ind. Definition mapsB (m : AttributeNameMaps.t attributeValue) (k : attributeName) (v : attributeValue) : bool := match AttributeNameMaps.find k m with | Some w => attributeValueBool v w | None => false end. Lemma mapsB_MapsToL : forall m k v, mapsB m k v = true -> AttributeNameMaps.MapsTo k v m. Proof. unfold mapsB. intros m k v Hf. destruct (AttributeNameMaps.find k m) eqn:Hfind. { rewrite <- attributeValueBoolDecT in Hf. subst v. apply (AttributeNameMaps.find_2 Hfind). } { contradict Hf. discriminate. } Qed. Lemma mapsB_MapsToR : forall m k v, AttributeNameMaps.MapsTo k v m -> mapsB m k v = true. Proof. intros m k v Hmaps. unfold mapsB. destruct (AttributeNameMaps.find k m) eqn:Hfind. { rewrite <- attributeValueBoolDecT. rewrite <- AttributeNameMapsFacts.find_mapsto_iff in Hfind. apply (AttributeNameMapsFacts.MapsTo_fun Hmaps Hfind). } { rewrite AttributeNameMapsFacts.find_mapsto_iff in Hmaps. rewrite Hmaps in Hfind. contradict Hfind. discriminate. } Qed. Lemma mapsB_MapsTo_iff : forall m k v, AttributeNameMaps.MapsTo k v m <-> mapsB m k v = true. Proof. split. apply mapsB_MapsToR. apply mapsB_MapsToL. Qed. (** An evaluation function for object match expressions. *) Fixpoint exprMatchObjectEvalF (o : object) (e : exprMatchObject) : bool := match e with | EMO_False => false | EMO_True => true | EMO_WithType n => eqb (ivName (oType o)) (ivName n) | EMO_WithAttributesAll attributesRequired => let attributesHeld := oAttributes o in forallb (fun p => mapsB attributesHeld (fst p) (snd p)) (AttributeNameMaps.elements attributesRequired) | EMO_WithAttributesAny attributesRequired => let attributesHeld := oAttributes o in existsb (fun p => mapsB attributesHeld (fst p) (snd p)) (AttributeNameMaps.elements attributesRequired) | EMO_And xs => forallb (exprMatchObjectEvalF o) xs | EMO_Or xs => existsb (exprMatchObjectEvalF o) xs end. (** The evaluation function for object match expressions as a relation. *) Inductive exprMatchObjectEvalR (o : object) : exprMatchObject -> Prop := | EMOR_True : exprMatchObjectEvalR o EMO_True | EMOR_WithName : forall (t : typeName), ivName (oType o) = ivName t -> exprMatchObjectEvalR o (EMO_WithType t) | EMOR_WithAttributesAll : forall (required : AttributeNameMaps.t attributeValue), (forall (k : attributeName) (v : attributeValue), AttributeNameMaps.MapsTo k v required -> AttributeNameMaps.MapsTo k v (oAttributes o)) -> exprMatchObjectEvalR o (EMO_WithAttributesAll required) | EMOR_WithAttributesAny : forall (required : AttributeNameMaps.t attributeValue), (exists k : attributeName, (exists v : attributeValue, AttributeNameMaps.MapsTo k v required /\ AttributeNameMaps.MapsTo k v (oAttributes o))) -> exprMatchObjectEvalR o (EMO_WithAttributesAny required) | EMOR_And : forall (es : list exprMatchObject), Forall (exprMatchObjectEvalR o) es -> exprMatchObjectEvalR o (EMO_And es) | EMOR_Or : forall (es : list exprMatchObject), Exists (exprMatchObjectEvalR o) es -> exprMatchObjectEvalR o (EMO_Or es) . Lemma exprMatchObjectEvalEquivalent_FR_T_EMO_False : forall s, true = exprMatchObjectEvalF s EMO_False -> exprMatchObjectEvalR s EMO_False. Proof. intros s Ht. inversion Ht. Qed. Lemma exprMatchObjectEvalEquivalent_FR_T_EMO_True : forall s, true = exprMatchObjectEvalF s EMO_True -> exprMatchObjectEvalR s EMO_True. Proof. intros s Ht. constructor. Qed. Lemma exprMatchObjectEvalEquivalent_FR_T_EMO_WithType : forall s n, true = exprMatchObjectEvalF s (EMO_WithType n) -> exprMatchObjectEvalR s (EMO_WithType n). Proof. intros s n Ht. unfold exprMatchObjectEvalF in Ht. symmetry in Ht. rewrite eqb_eq in Ht. pose proof (ivIrrelevantEqual _ _ Ht) as H. subst n. constructor. reflexivity. Qed. Lemma exprMatchObjectEvalEquivalent_FR_T_EMO_WithAttributesAll : forall s required, true = exprMatchObjectEvalF s (EMO_WithAttributesAll required) -> exprMatchObjectEvalR s (EMO_WithAttributesAll required). Proof. intros s required Ht. constructor. simpl in Ht. symmetry in Ht. rewrite forallb_forall in Ht. intros k v Hmaps. pose proof (Ht (k, v)) as Hp0. clear Ht. simpl in Hp0. rewrite <- mapsB_MapsTo_iff in Hp0. apply Hp0. clear Hp0. rewrite AttributeNameMapsFacts.elements_mapsto_iff in Hmaps. induction Hmaps as [x xs [H01 H02]|y ys H1]. { simpl. left. destruct x as [fx sx]. assert (fx = k) as Hp0. { simpl in H01. symmetry. exact H01. } assert (sx = v) as Hp1. { simpl in H02. symmetry. exact H02. } subst fx. subst sx. reflexivity. } { simpl. right; auto. } Qed. Lemma exprMatchObjectEvalEquivalent_FR_T_EMO_WithAttributesAny : forall s required, true = exprMatchObjectEvalF s (EMO_WithAttributesAny required) -> exprMatchObjectEvalR s (EMO_WithAttributesAny required). Proof. intros s required Ht. constructor. simpl in Ht. symmetry in Ht. rewrite existsb_exists in Ht. destruct Ht as [[k0 v0] [Ht0 Ht1]]. exists k0. exists v0. rewrite <- mapsB_MapsTo_iff in Ht1. simpl in Ht1. intros. split. { rewrite AttributeNameMapsFacts.elements_mapsto_iff. apply In_InA. exact AttributeNameMapsEqEquiv. exact Ht0. } { exact Ht1. } Qed. Lemma exprMatchObjectEvalEquivalent_FR_T : forall s e, true = exprMatchObjectEvalF s e -> exprMatchObjectEvalR s e. Proof. intros s e. induction e as [ | | |required |required |es Hes |es Hes ] using exprMatchObject_extendedInd. { apply exprMatchObjectEvalEquivalent_FR_T_EMO_False. } { apply exprMatchObjectEvalEquivalent_FR_T_EMO_True. } { apply exprMatchObjectEvalEquivalent_FR_T_EMO_WithType. } { apply exprMatchObjectEvalEquivalent_FR_T_EMO_WithAttributesAll. } { apply exprMatchObjectEvalEquivalent_FR_T_EMO_WithAttributesAny. } { (* EMO_And *) destruct es as [|y ys]. { intros Ht. constructor. constructor. } { simpl. intros Ht. (* We need to show that the relation holds for all (y :: ys). *) assert (Forall (exprMatchObjectEvalR s) (y :: ys)) as H0. { (* We do this by showing it holds for y... *) assert (exprMatchObjectEvalR s y) as H1. { symmetry in Ht. rewrite Bool.andb_true_iff in Ht. rewrite forallb_forall in Ht. destruct Ht as [HT0 HT1]. rewrite <- (@Forall_forall exprMatchObject _ ys) in HT1. apply (Forall_inv Hes). symmetry. exact HT0. } (* ... And for all ys. *) assert (Forall (exprMatchObjectEvalR s) ys) as H2. { symmetry in Ht. rewrite Bool.andb_true_iff in Ht. rewrite forallb_forall in Ht. destruct Ht as [HT0 HT1]. rewrite <- (@Forall_forall exprMatchObject _ ys) in HT1. assert (Forall (fun x => true = exprMatchObjectEvalF s x) ys) as H2. { rewrite Forall_forall. symmetry. generalize dependent x. rewrite <- Forall_forall. exact HT1. } pose proof (Forall_inv_tail Hes) as HesT. apply (Forall_impl_lifted _ _ _ ys H2 HesT). } (* ... And then composing the two. *) constructor. exact H1. exact H2. } constructor. exact H0. } } { (* EMO_Or *) destruct es as [|y ys]. { intros Ht. contradict Ht. simpl. discriminate. } { intros Ht. (* We need to show that the relation holds for y or something in ys. *) constructor. simpl in Ht. symmetry in Ht. destruct (Bool.orb_true_elim _ _ Ht) as [HtL|HtR]. { constructor. apply (Forall_inv Hes). auto. } { assert (Exists (exprMatchObjectEvalR s) (y :: ys)) as H0. { rewrite existsb_exists in HtR. destruct HtR as [k [Htk0 Htk1]]. rewrite Forall_forall in Hes. pose proof (in_cons y k ys Htk0) as H0. pose proof (Hes k H0 (eq_sym Htk1)) as H1. apply Exists_cons_tl. rewrite Exists_exists. exists k. auto. } exact H0. } } } Qed. Lemma exprMatchObjectEvalEquivalent_RF_T_False : forall s, exprMatchObjectEvalR s EMO_False -> true = exprMatchObjectEvalF s EMO_False. Proof. intros s Ht. inversion Ht. Qed. Lemma exprMatchObjectEvalEquivalent_RF_T_True : forall s, exprMatchObjectEvalR s EMO_True -> true = exprMatchObjectEvalF s EMO_True. Proof. intros s Ht. reflexivity. Qed. Lemma exprMatchObjectEvalEquivalent_RF_T_WithType : forall s n, exprMatchObjectEvalR s (EMO_WithType n) -> true = exprMatchObjectEvalF s (EMO_WithType n). Proof. intros s n Ht. simpl. inversion Ht as [ |y Hyz| | | |]. subst y. pose proof (ivIrrelevantEqual _ _ Hyz) as H0. rewrite H0. symmetry. apply eqb_refl. Qed. Lemma exprMatchObjectEvalEquivalent_RF_T_WithAttributesAll : forall s n, exprMatchObjectEvalR s (EMO_WithAttributesAll n) -> true = exprMatchObjectEvalF s (EMO_WithAttributesAll n). Proof. intros s n Hem. inversion Hem as [ | |required H0 H1| | |]. subst n. simpl. symmetry. rewrite forallb_forall. intros [k v] Hin. simpl. rewrite <- mapsB_MapsTo_iff. apply H0. rewrite AttributeNameMapsFacts.elements_mapsto_iff. apply In_InA. unfold AttributeNameMaps.eq_key_elt. constructor. { constructor; reflexivity. } { constructor. intuition. symmetry. intuition. } { intros x y z [Heq0 Heq1] [Heq2 Heq3]. rewrite Heq1. rewrite Heq3. rewrite <- Heq2. rewrite Heq0. constructor; reflexivity. } trivial. Qed. Lemma exprMatchObjectEvalEquivalent_RF_T_WithAttributesAny : forall s n, exprMatchObjectEvalR s (EMO_WithAttributesAny n) -> true = exprMatchObjectEvalF s (EMO_WithAttributesAny n). Proof. intros s n Hem. inversion Hem as [ | | |required H0 H1| |]. subst n. destruct H0 as [k [v [Hpm0 Hpm1]]]. simpl. symmetry. rewrite existsb_exists. exists (k, v). rewrite <- mapsB_MapsTo_iff. simpl. split. { rewrite AttributeNameMapsFacts.elements_mapsto_iff in Hpm0. rewrite InA_alt in Hpm0. destruct Hpm0 as [y [Hy0 Hy1]]. rewrite AttributeNameMapsEqLeibniz in Hy0. subst y. exact Hy1. } { exact Hpm1. } Qed. Lemma exprMatchObjectEvalEquivalent_RF_T : forall s e, exprMatchObjectEvalR s e -> true = exprMatchObjectEvalF s e. Proof. intros s e. induction e as [ | | | | |es Hes |es Hes ] using exprMatchObject_extendedInd. { apply exprMatchObjectEvalEquivalent_RF_T_False. } { apply exprMatchObjectEvalEquivalent_RF_T_True. } { apply exprMatchObjectEvalEquivalent_RF_T_WithType. } { apply exprMatchObjectEvalEquivalent_RF_T_WithAttributesAll. } { apply exprMatchObjectEvalEquivalent_RF_T_WithAttributesAny. } { (* EMO_And *) intros Ht. inversion Ht as [ | | | |es0 Hfa Heq|]. subst es0. simpl. symmetry. rewrite forallb_forall. intros x Hin. symmetry. generalize dependent x. rewrite <- Forall_forall. apply (Forall_impl_lifted exprMatchObject _ _ es Hfa Hes). } { (* EMO_Or *) intros Ht. symmetry. simpl. rewrite existsb_exists. inversion Ht as [ | | | | |es0 Hex Heq]. subst es. destruct Hex as [k ks Hk|k ks Hk]. { exists k. constructor. constructor; reflexivity. apply (eq_sym (Forall_inv Hes Hk)). } { rewrite Exists_exists in Hk. destruct Hk as [q [Hq0 Hq1]]. exists q. constructor. apply (in_cons k q ks Hq0). pose proof (Forall_inv_tail Hes) as HesT. rewrite Forall_forall in HesT. apply (eq_sym (HesT q Hq0 Hq1)). } } Qed. (** The evaluation function and the evaluation relation are equivalent. *) Theorem exprMatchObjectEvalEquivalentT : forall s e, true = exprMatchObjectEvalF s e <-> exprMatchObjectEvalR s e. Proof. split. apply exprMatchObjectEvalEquivalent_FR_T. apply exprMatchObjectEvalEquivalent_RF_T. Qed. Lemma exprMatchObjectEvalEquivalent_FR_F : forall a e, false = exprMatchObjectEvalF a e -> ~exprMatchObjectEvalR a e. Proof. intros s e. induction e as [ | | | | |es Hes |es Hes ] using exprMatchObject_extendedInd. { (* EMO_False *) intros Ht. intro Hcontra. inversion Hcontra. } { (* EMO_True *) intros Ht. contradict Ht. discriminate. } { (* EMO_WithType *) intros Ht. intros Hcontra. rewrite <- (exprMatchObjectEvalEquivalent_RF_T _ _ Hcontra) in Ht. contradict Ht; discriminate. } { (* EMO_WithAttributesAll *) intros Ht. intros Hcontra. rewrite <- (exprMatchObjectEvalEquivalent_RF_T _ _ Hcontra) in Ht. contradict Ht; discriminate. } { (* EMO_WithAttributesAny *) intros Ht. intros Hcontra. rewrite <- (exprMatchObjectEvalEquivalent_RF_T _ _ Hcontra) in Ht. contradict Ht; discriminate. } { (* EMS_And *) intros Ht. intros Hcontra. rewrite <- (exprMatchObjectEvalEquivalent_RF_T _ _ Hcontra) in Ht. contradict Ht; discriminate. } { (* EMS_Or *) intros Ht. intros Hcontra. rewrite <- (exprMatchObjectEvalEquivalent_RF_T _ _ Hcontra) in Ht. contradict Ht; discriminate. } Qed. Lemma exprMatchObjectEvalEquivalent_RF_F : forall a e, ~exprMatchObjectEvalR a e -> false = exprMatchObjectEvalF a e. Proof. intros s e. induction e as [ | | | | |es Hes |es Hes ] using exprMatchObject_extendedInd. { (* EMO_False *) intros Ht. reflexivity. } { (* EMO_True *) intros Ht. contradict Ht. constructor. } { (* EMS_WithType *) intros Ht. destruct (exprMatchObjectEvalF s (EMO_WithType n)) eqn:H. { symmetry in H. rewrite exprMatchObjectEvalEquivalentT in H. contradiction. } { reflexivity. } } { (* EMO_WithAttributesAll *) intros Ht. destruct (exprMatchObjectEvalF s (EMO_WithAttributesAll n)) eqn:H. { symmetry in H. rewrite exprMatchObjectEvalEquivalentT in H. contradiction. } { reflexivity. } } { (* EMO_WithAttributesAny *) intros Ht. destruct (exprMatchObjectEvalF s (EMO_WithAttributesAny n)) eqn:H. { symmetry in H. rewrite exprMatchObjectEvalEquivalentT in H. contradiction. } { reflexivity. } } { (* EMS_And *) intros Ht. destruct (exprMatchObjectEvalF s (EMO_And es)) eqn:H. { symmetry in H. rewrite exprMatchObjectEvalEquivalentT in H. contradiction. } { reflexivity. } } { (* EMS_Or *) intros Ht. destruct (exprMatchObjectEvalF s (EMO_Or es)) eqn:H. { symmetry in H. rewrite exprMatchObjectEvalEquivalentT in H. contradiction. } { reflexivity. } } Qed. (** The evaluation function and the evaluation relation are equivalent. *) Theorem exprMatchObjectEvalEquivalentF : forall a e, false = exprMatchObjectEvalF a e <-> ~exprMatchObjectEvalR a e. Proof. split. apply exprMatchObjectEvalEquivalent_FR_F. apply exprMatchObjectEvalEquivalent_RF_F. Qed. (** The evaluation relation is decidable. *) Theorem exprMatchObjectEvalRDec : forall o e, {exprMatchObjectEvalR o e}+{~exprMatchObjectEvalR o e}. Proof. intros o e. destruct (exprMatchObjectEvalF o e) eqn:Hev. { symmetry in Hev. rewrite exprMatchObjectEvalEquivalentT in Hev. left; intuition. } { symmetry in Hev. rewrite exprMatchObjectEvalEquivalentF in Hev. right; intuition. } Qed. (** Any object trivially matches a _WithAttributesAll_ expression that specifies an empty set of attributes. *) Theorem exprMatchObjectWithAllEmpty : forall o, exprMatchObjectEvalF o (EMO_WithAttributesAll (AttributeNameMaps.empty attributeValue)) = true. Proof. intros o. simpl. rewrite forallb_forall. intros x Hcontra. destruct x as [k v]. pose proof (In_InA AttributeNameMapsEqEquiv Hcontra) as H0. rewrite <- AttributeNameMapsFacts.elements_mapsto_iff in H0. rewrite AttributeNameMapsFacts.empty_mapsto_iff in H0. contradiction. Qed. (** No object matches a _WithAttributesAny_ expression that specifies an empty set of attributes. *) Theorem exprMatchObjectWithAnyEmpty : forall o, exprMatchObjectEvalF o (EMO_WithAttributesAny (AttributeNameMaps.empty attributeValue)) = false. Proof. intros o. simpl. rewrite attributesEmptyElements. reflexivity. Qed.
(* * Copyright © 2023 Mark Raynsford <code@io7m.com> https://www.io7m.com * * Permission to use, copy, modify, and/or distribute this software for any * purpose with or without fee is hereby granted, provided that the above * copyright notice and this permission notice appear in all copies. * * THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES * WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF * MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR ANY * SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES * WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN * ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF OR * IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE. *) Require Import Coq.Lists.List. Require Import Coq.Strings.String. Require Import Coq.Strings.Ascii. Local Open Scope string_scope. Set Mangle Names. (** The set of acceptable characters in a name. *) Definition acceptableCharacters : list Ascii.ascii := list_ascii_of_string "abcdefghijklmnopqrstuvwxyz0123456789_.". (** A description of a valid name. *) Definition validName (s : string) : Prop := Forall (fun c => In c acceptableCharacters) (list_ascii_of_string s) /\ length s >= 1 /\ length s <= 256. (** Whether all characters in a string are valid is decidable. *) Lemma validNameForall_dec : forall s, {Forall (fun c => In c acceptableCharacters) (list_ascii_of_string s)}+ {~Forall (fun c => In c acceptableCharacters) (list_ascii_of_string s)}. Proof. intros s. apply Forall_dec. intros c. apply in_dec. apply Ascii.ascii_dec. Qed. (** Whether a string is non-empty is decidable. *) Lemma validNameLength1_dec : forall s, {length s >= 1}+{~length s >= 1}. Proof. intros s. apply Compare_dec.ge_dec. Qed. (** Whether a string is short enough is decidable. *) Lemma validNameLength256_dec : forall s, {length s <= 256}+{~length s <= 256}. Proof. intros s. apply Compare_dec.ge_dec. Qed. (** Whether a string is valid is decidable. *) Theorem validNameDecidable : forall s, {validName s}+{~validName s}. Proof. intros s. unfold validName. destruct (validNameForall_dec s); intuition. destruct (validNameLength1_dec s); intuition. destruct (validNameLength256_dec s); intuition. Qed. (** The class of valid names. *) Class IsValidName (A : Type) := { (** A valid name exposes its contents as a string. *) ivName : A -> string; (** A valid name's contents are valid according to _validName_. *) ivValid : forall (x : A), validName (ivName x); (** Two names with the same contents are equal. *) ivIrrelevantEqual : forall (x y : A), ivName x = ivName y -> x = y }.
(* * Copyright © 2023 Mark Raynsford <code@io7m.com> https://www.io7m.com * * Permission to use, copy, modify, and/or distribute this software for any * purpose with or without fee is hereby granted, provided that the above * copyright notice and this permission notice appear in all copies. * * THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES * WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF * MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR ANY * SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES * WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN * ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF OR * IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE. *) Require Import Coq.Strings.String. Require Import Medrina.Attributes. Require Import Medrina.Names. (** The type of type names. *) Record typeName := TNMake { (** The name of the type. *) tnName : string; (** Type names are valid. *) tnValid : validName tnName }. Require Import Coq.Logic.ProofIrrelevance. (** Equality of type names is decidable. *) Theorem typeNameDec : forall (a b : typeName), {a = b}+{a <> b}. Proof. intros a b. destruct a as [a0 [a1 [a2 a3]]]. destruct b as [b0 [b1 [b2 b3]]]. destruct (string_dec a0 b0) as [H0|H1]. { subst b0. left. assert (a1 = b1) by apply proof_irrelevance. subst b1. assert (a2 = b2) by apply proof_irrelevance. subst b2. assert (a3 = b3) by apply proof_irrelevance. subst b3. intuition. } { right. congruence. } Qed. (** Proof irrelevance allows for equality between instances with equal names. *) Theorem typeNameIrrelevance : forall (a b : typeName), tnName a = tnName b -> a = b. Proof. intros a b Heq. destruct a as [a0 a1]. destruct b as [b0 b1]. simpl in Heq. subst b0. assert (a1 = b1) by apply proof_irrelevance. subst b1. reflexivity. Qed. #[export] Instance typeNameName : IsValidName typeName := { ivName := tnName; ivValid := tnValid; ivIrrelevantEqual := typeNameIrrelevance }. (** The type of objects. *) Record object := OMake { (** The object type name. *) oType : typeName; (** The attributes held by the object. *) oAttributes : AttributeNameMaps.t attributeValue }.
(* * Copyright © 2023 Mark Raynsford <code@io7m.com> https://www.io7m.com * * Permission to use, copy, modify, and/or distribute this software for any * purpose with or without fee is hereby granted, provided that the above * copyright notice and this permission notice appear in all copies. * * THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES * WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF * MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR ANY * SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES * WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN * ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF OR * IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE. *) Require Import Medrina.Subjects. Require Import Medrina.Objects. Require Import Medrina.Actions. Require Import Medrina.Rules. Require Import Coq.Lists.List. Require Import Psatz. Import ListNotations. (** A policy is a list of rules. *) Definition policy := list rule. (** The result of evaluating a policy either allows or denies access. *) Inductive access : Set := | AccessAllowed | AccessDenied . (** The conclusion of a rule implies a particular access value. *) Definition ruleConclusionAccess (c : ruleConclusion) : access := match c with | RC_Allow => AccessAllowed | RC_AllowImmediately => AccessAllowed | RC_Deny => AccessDenied | RC_DenyImmediately => AccessDenied end. (** The evaluation of a rule may either halt or continue evaluation. *) Inductive halt : Set := | Halt | HContinue . (** When a rule is evaluated, the rule either matches the input and therefore returns a _halt_ and _access_ value, or the rule does not match (and therefore evaluation implicitly continues). *) Inductive evaluationOfRule : Set := | ERuleMatched : halt -> access -> evaluationOfRule | ERuleDidNotMatch : evaluationOfRule . (** Shorthand for the conditions where a matching rule allows access; the conclusion of the rule is one of the "allow" values. *) Definition ruleAllows (r : rule) : Prop := ((rConclusion r) = RC_AllowImmediately \/ (rConclusion r) = RC_Allow). (** Shorthand for the conditions where a matching rule denies access; the conclusion of the rule is one of the "deny" values. *) Definition ruleDenies (r : rule) : Prop := ((rConclusion r) = RC_DenyImmediately \/ (rConclusion r) = RC_Deny). (** Shorthand for the conditions where a matching rule will halt evaluation. *) Definition ruleHaltsOnMatch (r : rule) : Prop := ((rConclusion r) = RC_AllowImmediately \/ (rConclusion r) = RC_DenyImmediately). (** Shorthand for the conditions where a matching rule will not halt evaluation. *) Definition ruleDoesNotHaltOnMatch (r : rule) : Prop := ((rConclusion r) = RC_Allow \/ (rConclusion r) = RC_Deny). (** Shorthand for the condition where a rule does not match. *) Definition ruleDoesNotMatch (s : subject) (o : object) (a : action) (r : rule) : Prop := ruleMatchesF s o a r = false. (** Shorthand for a rule that matches and results in a given conclusion. *) Definition ruleMatchesWithConclusion (s : subject) (o : object) (a : action) (r : rule) (c : ruleConclusion) : Prop := ruleMatchesF s o a r = true /\ (rConclusion r) = c. (** The evaluation function for a single rule. *) Definition evaluateRule (r : rule) (s : subject) (o : object) (a : action) : evaluationOfRule := match ruleMatchesF s o a r with | true => match (rConclusion r) with | RC_Allow => ERuleMatched HContinue AccessAllowed | RC_AllowImmediately => ERuleMatched Halt AccessAllowed | RC_Deny => ERuleMatched HContinue AccessDenied | RC_DenyImmediately => ERuleMatched Halt AccessDenied end | false => ERuleDidNotMatch end. Fixpoint evaluateRulesInF (acc : access) (rs : list rule) (s : subject) (o : object) (a : action) : access := match rs with | [] => acc | x :: xs => match evaluateRule x s o a with | ERuleMatched h acc_new => match h with | Halt => acc_new | HContinue => evaluateRulesInF acc_new xs s o a end | ERuleDidNotMatch => evaluateRulesInF acc xs s o a end end. (** The function to evaluate a list of rules, using _AccessDenied_ as the default access if no rules match. *) Definition evaluateRules (rs : list rule) (s : subject) (o : object) (a : action) : access := evaluateRulesInF AccessDenied rs s o a. (** The function to evaluate a policy. *) Definition evaluatePolicy (p : policy) (s : subject) (o : object) (a : action) : access := evaluateRules p s o a. Theorem evaluateRulesInFSplit : forall (s : subject) (o : object) (a : action), forall (r : rule), ruleMatchesF s o a r = true -> forall r_pre : list rule, Forall (fun q => ruleDoesNotHaltOnMatch q) r_pre -> forall acc, evaluateRulesInF acc (r_pre ++ [r]) s o a = evaluateRulesInF acc [r] s o a. Proof. intros s o a r Hm r_pre. induction r_pre as [|z zs]. { reflexivity. } { simpl. unfold evaluateRule. rewrite Hm. destruct (ruleMatchesF s o a z) eqn:Hzmat. { intros Hfa acc. pose proof (Forall_inv Hfa) as H0. simpl in H0. unfold ruleDoesNotHaltOnMatch in H0. destruct (rConclusion z) eqn:Hrcz. { destruct H0 as [H0L|H0R]. - destruct (rConclusion r) eqn:Hrcr; (pose proof (IHzs (Forall_inv_tail Hfa) AccessAllowed) as IH0; rewrite IH0; simpl; unfold evaluateRule; rewrite Hm; rewrite Hrcr; reflexivity). - contradict H0R; discriminate. } { destruct H0 as [H0L|H0R]. - destruct (rConclusion r) eqn:Hrcr; (try reflexivity; try (contradict H0L; discriminate)). - contradict H0R; discriminate. } { destruct H0 as [H0L|H0R]. - contradict H0L; discriminate. - destruct (rConclusion r) eqn:Hrcr; (pose proof (IHzs (Forall_inv_tail Hfa) AccessDenied) as IH0; rewrite IH0; simpl; unfold evaluateRule; rewrite Hm; rewrite Hrcr; reflexivity). } { destruct H0 as [H|H]; (contradict H; discriminate). } } { intros Hfa acc. rewrite (IHzs (Forall_inv_tail Hfa) acc). simpl. unfold evaluateRule. rewrite Hm. reflexivity. } } Qed. Theorem evaluateRulesInFSplitHalt : forall (s : subject) (o : object) (a : action), forall (r : rule), ruleMatchesF s o a r = true /\ ruleHaltsOnMatch r -> forall r_pre : list rule, Forall (fun q => ruleDoesNotHaltOnMatch q) r_pre -> forall r_post : list rule, forall acc0 acc1, evaluateRulesInF acc0 (r_pre ++ [r] ++ r_post) s o a = evaluateRulesInF acc1 [r] s o a. Proof. intros s o a r [Hm0 Hm1] r_pre. induction r_pre as [|z zs]. { simpl. unfold evaluateRule. rewrite Hm0. destruct Hm1 as [H|H]; (rewrite H; reflexivity). } { intros Hfa. intros r_post acc0. simpl (evaluateRulesInF acc0 ((z :: zs) ++ [r] ++ r_post) s o a) at 1. unfold evaluateRule. destruct (ruleMatchesF s o a z) eqn:Hzmat. { pose proof (Forall_inv Hfa) as [H|H]; (rewrite H; apply IHzs; apply (Forall_inv_tail Hfa)). } { apply IHzs. apply (Forall_inv_tail Hfa). } } Qed. Theorem evaluateRulesInFHaltAllow : forall (s : subject) (o : object) (a : action), forall (r : rule), ruleMatchesF s o a r = true /\ ruleHaltsOnMatch r /\ ruleAllows r -> forall r_pre : list rule, Forall (fun q => ruleDoesNotHaltOnMatch q) r_pre -> forall r_post : list rule, forall acc, evaluateRulesInF acc (r_pre ++ [r] ++ r_post) s o a = AccessAllowed. Proof. intros s o a r [Hm0 [Hm1L Hm1R]] r_pre. intros Hfa. intros r_post acc. rewrite (evaluateRulesInFSplitHalt s o a r (conj Hm0 Hm1L) r_pre Hfa r_post acc acc). simpl. unfold evaluateRule. rewrite Hm0. destruct Hm1R as [H|H]; (rewrite H; reflexivity). Qed. Theorem evaluateRulesInFHaltDeny : forall (s : subject) (o : object) (a : action), forall (r : rule), ruleMatchesF s o a r = true /\ ruleHaltsOnMatch r /\ ruleDenies r -> forall r_pre : list rule, Forall (fun q => ruleDoesNotHaltOnMatch q) r_pre -> forall r_post : list rule, forall acc, evaluateRulesInF acc (r_pre ++ [r] ++ r_post) s o a = AccessDenied. Proof. intros s o a r [Hm0 [Hm1L Hm1R]] r_pre. intros Hfa. intros r_post acc. rewrite (evaluateRulesInFSplitHalt s o a r (conj Hm0 Hm1L) r_pre Hfa r_post acc acc). simpl. unfold evaluateRule. rewrite Hm0. destruct Hm1R as [H|H]; (rewrite H; reflexivity). Qed. Theorem evaluateRulesInFPreNotMatching : forall (s : subject) (o : object) (a : action), forall r_pre : list rule, Forall (fun q => ruleDoesNotMatch s o a q) r_pre -> forall r_post : list rule, forall acc, evaluateRulesInF acc (r_pre ++ r_post) s o a = evaluateRulesInF acc r_post s o a. Proof. intros s o a. induction r_pre as [|z zs IH]. { intros. rewrite app_nil_l. reflexivity. } { intros Hfa r_post acc. simpl (evaluateRulesInF acc ((z :: zs) ++ r_post) s o a) at 1. unfold evaluateRule. rewrite (Forall_inv Hfa). apply IH. apply (Forall_inv_tail Hfa). } Qed. Theorem evaluateRulesInFPostNotMatching : forall (s : subject) (o : object) (a : action), forall r_post : list rule, Forall (fun q => ruleDoesNotMatch s o a q) r_post -> forall r_pre : list rule, forall acc, evaluateRulesInF acc (r_pre ++ r_post) s o a = evaluateRulesInF acc r_pre s o a. Proof. intros s o a r_post Hfa. induction r_post as [|z zs IH]. { intros r_pre. rewrite app_nil_r. reflexivity. } { induction r_pre as [|w ws IHp]. { intros acc. rewrite <- (IH (Forall_inv_tail Hfa) [] acc). rewrite app_nil_l. rewrite app_nil_l. simpl. unfold evaluateRule. rewrite (Forall_inv Hfa). reflexivity. } { intros acc. simpl (evaluateRulesInF acc ((w :: ws) ++ z :: zs) s o a) at 1. unfold evaluateRule. destruct (ruleMatchesF s o a w) eqn:Hrwm. { destruct (rConclusion w) eqn:Hwc. { simpl (evaluateRulesInF acc (w :: ws) s o a) at 1. unfold evaluateRule. rewrite Hrwm. rewrite Hwc. apply IHp. } { simpl (evaluateRulesInF acc (w :: ws) s o a) at 1. unfold evaluateRule. rewrite Hrwm. rewrite Hwc. reflexivity. } { simpl (evaluateRulesInF acc (w :: ws) s o a) at 1. unfold evaluateRule. rewrite Hrwm. rewrite Hwc. apply IHp. } { simpl (evaluateRulesInF acc (w :: ws) s o a) at 1. unfold evaluateRule. rewrite Hrwm. rewrite Hwc. reflexivity. } } { simpl (evaluateRulesInF acc (w :: ws) s o a) at 1. unfold evaluateRule. rewrite Hrwm. apply IHp. } } } Qed. Theorem evaluateRulesInFPreNotHalting : forall (s : subject) (o : object) (a : action), forall (r : rule), ruleMatchesF s o a r = true -> forall r_pre : list rule, Forall (fun q => ruleDoesNotHaltOnMatch q) r_pre -> forall acc, evaluateRulesInF acc (r_pre ++ [r]) s o a = ruleConclusionAccess (rConclusion r). Proof. intros s o a r Hrm. induction r_pre as [|z zs]. { simpl. unfold evaluateRule. rewrite Hrm. intros Hfa acc. destruct (rConclusion r); reflexivity. } { intros Hfa. intros acc. simpl (evaluateRulesInF acc ((z :: zs) ++ [r]) s o a) at 1. unfold evaluateRule. destruct (ruleMatchesF s o a z) eqn:Hzm. { destruct (Forall_inv Hfa) as [H|H]; (rewrite H; apply IHzs; apply (Forall_inv_tail Hfa)). } { apply IHzs. apply (Forall_inv_tail Hfa). } } Qed. Theorem evaluateRulesInFLastMatching : forall (s : subject) (o : object) (a : action), forall (r : rule), ruleMatchesF s o a r = true -> forall r_pre : list rule, Forall (fun q => ruleDoesNotHaltOnMatch q) r_pre -> forall r_post : list rule, Forall (fun q => ruleDoesNotMatch s o a q) r_post -> forall acc, evaluateRulesInF acc (r_pre ++ [r] ++ r_post) s o a = ruleConclusionAccess (rConclusion r). Proof. intros s o a r Hrm. induction r_pre as [|z zs]. { intros Hfa r_post. rewrite app_nil_l. simpl. unfold evaluateRule. rewrite Hrm. destruct (rConclusion r) eqn:Hrcr. { induction r_post as [|w ws IH]. { reflexivity. } { intros Hfaw acc. simpl. unfold evaluateRule. rewrite (Forall_inv Hfaw). rewrite IH. reflexivity. apply (Forall_inv_tail Hfaw). exact acc. } } { induction r_post; reflexivity. } { induction r_post as [|w ws IH]. { reflexivity. } { intros Hfaw acc. simpl. unfold evaluateRule. rewrite (Forall_inv Hfaw). rewrite IH. reflexivity. apply (Forall_inv_tail Hfaw). exact acc. } } { induction r_post; reflexivity. } } { intros Hfaz. simpl. destruct (Forall_inv Hfaz) as [H|H]. { unfold evaluateRule. rewrite H. destruct (ruleMatchesF s o a z) eqn:Hmz. { intros r_post Hfap acc. apply (IHzs (Forall_inv_tail Hfaz) r_post Hfap AccessAllowed). } { intros r_post Hfap acc. apply (IHzs (Forall_inv_tail Hfaz) r_post Hfap acc). } } { unfold evaluateRule. rewrite H. destruct (ruleMatchesF s o a z) eqn:Hmz. { intros r_post Hfap acc. apply (IHzs (Forall_inv_tail Hfaz) r_post Hfap AccessDenied). } { intros r_post Hfap acc. apply (IHzs (Forall_inv_tail Hfaz) r_post Hfap acc). } } } Qed. Theorem evaluateRulesInFLastMatchingPreNoHalt : forall (s : subject) (o : object) (a : action), forall (r : rule), ruleMatchesF s o a r = true -> forall r_pre : list rule, Forall (fun q => ruleDoesNotHaltOnMatch q) r_pre -> forall r_post : list rule, Forall (fun q => ruleDoesNotMatch s o a q) r_post -> forall acc, evaluateRulesInF acc (r_pre ++ [r] ++ r_post) s o a = evaluateRulesInF acc [r] s o a. Proof. intros s o a r Hrm. assert (forall acc q, ruleMatchesF s o a q = true -> evaluateRulesInF acc [q] s o a = ruleConclusionAccess (rConclusion q)) as H0. { intros acc q Hq. simpl. unfold evaluateRule. rewrite Hq. destruct (rConclusion q); reflexivity. } intros. rewrite (H0 acc r Hrm). apply evaluateRulesInFLastMatching; trivial. Qed. (* * Externally visible proofs. *) (** If no rules in a policy match, the default is to deny access. *) Theorem evaluateRulesDefaultDenyNoMatches : forall rs s o a, Forall (fun r => ruleMatchesF s o a r = false) rs -> evaluateRules rs s o a = AccessDenied. Proof. unfold evaluateRules. induction rs as [|y ys IH]. { reflexivity. } { intros s o a Hfa. pose proof (IH s o a (Forall_inv_tail Hfa)) as Hfa0. pose proof (Forall_inv Hfa) as Hfa1. simpl in Hfa1. simpl. unfold evaluateRule. rewrite Hfa1. exact Hfa0. } Qed. (** If a policy consists of a sequence of rules _r_pre_ that do not halt on matching, followed by a rule _r_ that does match, followed by a possibly-empty sequence of rules _r_post_ that do not match, then evaluation is equivalent to evaluating _r_ on its own. *) Theorem evaluateRulesLastMatchingPreNoHalt : forall (s : subject) (o : object) (a : action) (r : rule) (r_pre : list rule) (r_post : list rule), ruleMatchesF s o a r = true -> Forall (fun q => ruleDoesNotHaltOnMatch q) r_pre -> Forall (fun q => ruleDoesNotMatch s o a q) r_post -> evaluateRules (r_pre ++ [r] ++ r_post) s o a = evaluateRules [r] s o a. Proof. unfold evaluateRules. intros. apply evaluateRulesInFLastMatchingPreNoHalt; trivial. Qed. (** If a policy consists of a sequence or rules _r_pre_, followed by a sequence of rules _r_post_ that do not match, then the result is equivalent to evaluating _r_pre_. *) Theorem evaluateRulesPostNotMatching : forall (s : subject) (o : object) (a : action) (r_pre : list rule) (r_post : list rule), Forall (fun q => ruleDoesNotMatch s o a q) r_post -> evaluateRules (r_pre ++ r_post) s o a = evaluateRules r_pre s o a. Proof. unfold evaluateRules. intros. apply evaluateRulesInFPostNotMatching; trivial. Qed. (** If a policy consists of a sequence or rules _r_pre_ that do not match, followed by a sequence of rules _r_post_, then the result is equivalent to evaluating _r_post_. *) Theorem evaluateRulesPreNotMatching : forall (s : subject) (o : object) (a : action) (r_pre : list rule) (r_post : list rule), Forall (fun q => ruleDoesNotMatch s o a q) r_pre -> evaluateRules (r_pre ++ r_post) s o a = evaluateRules r_post s o a. Proof. unfold evaluateRules. intros. apply evaluateRulesInFPreNotMatching; trivial. Qed.
(* * Copyright © 2023 Mark Raynsford <code@io7m.com> https://www.io7m.com * * Permission to use, copy, modify, and/or distribute this software for any * purpose with or without fee is hereby granted, provided that the above * copyright notice and this permission notice appear in all copies. * * THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES * WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF * MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR ANY * SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES * WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN * ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF OR * IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE. *) Require Import Coq.Strings.String. Require Import Medrina.Names. (** The type of role names. *) Record roleName := RNMake { (** The name of the role. *) rnName : string; (** Role names are valid. *) rnValid : validName rnName }. Require Import Coq.Logic.ProofIrrelevance. (** Equality of role names is decidable. *) Theorem roleNameDec : forall (a b : roleName), {a = b}+{a <> b}. Proof. intros a b. destruct a as [a0 [a1 [a2 a3]]]. destruct b as [b0 [b1 [b2 b3]]]. destruct (string_dec a0 b0) as [H0|H1]. { subst b0. left. assert (a1 = b1) by apply proof_irrelevance. subst b1. assert (a2 = b2) by apply proof_irrelevance. subst b2. assert (a3 = b3) by apply proof_irrelevance. subst b3. intuition. } { right. congruence. } Qed. Require Import Coq.FSets.FSetInterface. Require Import Coq.FSets.FSetWeakList. Require Import Coq.FSets.FSetFacts. Require Import Coq.Structures.Equalities. (** A mini decidable type module to instantiate sets. *) Module RoleNameMiniDec : MiniDecidableType with Definition t := roleName. Definition t := roleName. Definition eq := @Logic.eq t. Definition eq_refl := @Logic.eq_refl t. Definition eq_sym := @Logic.eq_sym t. Definition eq_trans := @Logic.eq_trans t. Theorem eq_dec : forall x y : t, {eq x y} + {~ eq x y}. Proof. apply roleNameDec. Qed. End RoleNameMiniDec. (** A usual decidable type module to instantiate sets. *) Module RoleNameDec <: UsualDecidableType with Definition t := roleName with Definition eq := @Logic.eq roleName := Make_UDT RoleNameMiniDec. (** A Maps module with attribute name keys. *) Module RoleSets : FSetInterface.WS with Definition E.t := roleName with Definition E.eq := @Logic.eq roleName := FSetWeakList.Make RoleNameDec. Module RoleSetsFacts := Facts RoleSets. (** Proof irrelevance allows for equality between instances with equal names. *) Theorem roleNameIrrelevance : forall (a b : roleName), rnName a = rnName b -> a = b. Proof. intros a b Heq. destruct a as [a0 a1]. destruct b as [b0 b1]. simpl in Heq. subst b0. assert (a1 = b1) by apply proof_irrelevance. subst b1. reflexivity. Qed. #[export] Instance roleNameName : IsValidName roleName := { ivName := rnName; ivValid := rnValid; ivIrrelevantEqual := roleNameIrrelevance }. Theorem roleSubsetFalse : forall (r s : RoleSets.t), ~ RoleSets.Subset r s <-> RoleSets.subset r s = false. Proof. intros r s. split. { intros Hnot. destruct (RoleSets.subset r s) eqn:H. { rewrite <- RoleSetsFacts.subset_iff in H. contradiction. } { reflexivity. } } { intros Hnot. destruct (RoleSets.subset r s) eqn:H. { contradict Hnot; discriminate. } { intro Hfalse. rewrite RoleSetsFacts.subset_iff in Hfalse. rewrite Hfalse in H. contradict H; discriminate. } } Qed. Theorem roleExistsFalse : forall (r : RoleSets.t) (f : RoleSets.elt -> bool), compat_bool eq f -> ~ RoleSets.Exists (fun x => f x = true) r <-> RoleSets.exists_ f r = false. Proof. intros r f Hf. split. { intros Hnot. intuition. destruct (RoleSets.exists_ f r) eqn:H. { rewrite <- (RoleSetsFacts.exists_iff r Hf) in H. contradiction. } { reflexivity. } } { intros Hnot. intros Hfalse. rewrite (RoleSetsFacts.exists_iff _ Hf) in Hfalse. rewrite Hfalse in Hnot. contradict Hnot. discriminate. } Qed.
(* * Copyright © 2023 Mark Raynsford <code@io7m.com> https://www.io7m.com * * Permission to use, copy, modify, and/or distribute this software for any * purpose with or without fee is hereby granted, provided that the above * copyright notice and this permission notice appear in all copies. * * THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES * WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF * MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR ANY * SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES * WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN * ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF OR * IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE. *) Require Import Medrina.Objects. Require Import Medrina.Subjects. Require Import Medrina.Actions. Require Import Medrina.Matches. Require Import Medrina.Names. Require Import Coq.Strings.String. (** The conclusion for a rule, if the rule matches. *) Inductive ruleConclusion : Set := (** Allow access and continue evaluating rules. *) | RC_Allow (** Allow access and halt evaluation. *) | RC_AllowImmediately (** Deny access and continue evaluating rules. *) | RC_Deny (** Deny access and halt evaluation. *) | RC_DenyImmediately . (** Rule conclusion equality is decidable. *) Theorem ruleConclusionDec : forall (x y : ruleConclusion), {x = y}+{~x = y}. Proof. decide equality. Qed. (** A single rule in a policy. *) Record rule := Rule { (** The rule conclusion. *) rConclusion : ruleConclusion; (** The expression that matches a subject. *) rMatchSubject : exprMatchSubject; (** The expression that matches an object. *) rMatchObject : exprMatchObject; (** The expression that matches a subject. *) rMatchAction : exprMatchAction; (** The rule name. *) rName : string; rNameValid : validName rName; (** The rule description. *) rDescription : string; }. (** A function that determines if a rule matches. *) Definition ruleMatchesF (s : subject) (o : object) (a : action) (r : rule) : bool := let sm := exprMatchSubjectEvalF s (rMatchSubject r) in let om := exprMatchObjectEvalF o (rMatchObject r) in let am := exprMatchActionEvalF a (rMatchAction r) in andb (andb sm om) am. (** The rule matching relation. *) Inductive ruleMatchesR : subject -> object -> action -> rule -> Prop := RM_Matches : forall s o a r, exprMatchSubjectEvalR s (rMatchSubject r) -> exprMatchObjectEvalR o (rMatchObject r) -> exprMatchActionEvalR a (rMatchAction r) -> ruleMatchesR s o a r. (** The match function and relation are equivalent. *) Theorem ruleMatchesFEquivalentT : forall s o a r, ruleMatchesF s o a r = true <-> ruleMatchesR s o a r. Proof. intros s o a r. split. { intros Hm. unfold ruleMatchesF in Hm. rewrite Bool.andb_true_iff in Hm. rewrite Bool.andb_true_iff in Hm. destruct Hm as [[Hm0 Hm1] Hm2]. symmetry in Hm0. symmetry in Hm1. symmetry in Hm2. rewrite exprMatchSubjectEvalEquivalentT in Hm0. rewrite exprMatchObjectEvalEquivalentT in Hm1. rewrite exprMatchActionEvalEquivalentT in Hm2. constructor; auto. } { intros Hm. inversion Hm as [x0 x1 x2 x3 H0 H1 H2]. subst x0. subst x1. subst x2. subst x3. rewrite <- exprMatchSubjectEvalEquivalentT in H0. rewrite <- exprMatchObjectEvalEquivalentT in H1. rewrite <- exprMatchActionEvalEquivalentT in H2. unfold ruleMatchesF. intuition. } Qed. (** The match function and relation are equivalent. *) Theorem ruleMatchesFEquivalentF : forall s o a r, ruleMatchesF s o a r = false <-> ~ruleMatchesR s o a r. Proof. intros s o a r. split. { intros Hm. unfold ruleMatchesF in Hm. rewrite Bool.andb_false_iff in Hm. rewrite Bool.andb_false_iff in Hm. destruct Hm as [[Hm0|Hm1]|Hm2]. { intros Hnot. inversion Hnot as [x0 x1 x2 x3 H0 H1 H2]. subst x0. subst x1. subst x2. subst x3. rewrite <- exprMatchSubjectEvalEquivalentT in H0. rewrite <- H0 in Hm0. contradict Hm0; discriminate. } { intros Hnot. inversion Hnot as [x0 x1 x2 x3 H0 H1 H2]. subst x0. subst x1. subst x2. subst x3. rewrite <- exprMatchObjectEvalEquivalentT in H1. rewrite <- H1 in Hm1. contradict Hm1; discriminate. } { intros Hnot. inversion Hnot as [x0 x1 x2 x3 H0 H1 H2]. subst x0. subst x1. subst x2. subst x3. rewrite <- exprMatchActionEvalEquivalentT in H2. rewrite <- H2 in Hm2. contradict Hm2; discriminate. } } { intros Hnot. unfold ruleMatchesF. rewrite Bool.andb_false_iff. rewrite Bool.andb_false_iff. destruct (exprMatchSubjectEvalF s (rMatchSubject r)) eqn:H0. { destruct (exprMatchObjectEvalF o (rMatchObject r)) eqn:H1. { destruct (exprMatchActionEvalF a (rMatchAction r)) eqn:H2. { symmetry in H0. symmetry in H1. symmetry in H2. rewrite exprMatchSubjectEvalEquivalentT in H0. rewrite exprMatchObjectEvalEquivalentT in H1. rewrite exprMatchActionEvalEquivalentT in H2. assert (ruleMatchesR s o a r) as Hcontra. { constructor; intuition. } contradiction. } { intuition. } } { intuition. } } { intuition. } } Qed. (** The match relation is decidable. *) Theorem ruleMatchesDec : forall s o a r, {ruleMatchesR s o a r}+{~ruleMatchesR s o a r}. Proof. intros s o a r. destruct (ruleMatchesF s o a r) eqn:Hm. { rewrite ruleMatchesFEquivalentT in Hm. left; intuition. } { rewrite ruleMatchesFEquivalentF in Hm. right; intuition. } Qed.
(* * Copyright © 2023 Mark Raynsford <code@io7m.com> https://www.io7m.com * * Permission to use, copy, modify, and/or distribute this software for any * purpose with or without fee is hereby granted, provided that the above * copyright notice and this permission notice appear in all copies. * * THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES * WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF * MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR ANY * SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES * WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN * ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF OR * IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE. *) Require Import Medrina.Roles. (** The type of subjects. *) Record subject := SMake { (** The roles held by the subject. *) sRoles : RoleSets.t }.