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; }.
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 .
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.
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.
Theorem ruleMatchesFEquivalentT : forall s o a r, ruleMatchesF s o a r = true <-> ruleMatchesR s o a r. Proof. (* Proof omitted for brevity; see Rules.v for proofs. *) Qed.
Theorem ruleMatchesFEquivalentF : forall s o a r, ruleMatchesF s o a r = false <-> ~ruleMatchesR s o a r. Proof. (* Proof omitted for brevity; see Rules.v for proofs. *) Qed.