| CREATOR | Mark Raynsford |
| DATE | 2023-04-08T12:57:18+00:00 |
| DESCRIPTION | Medrina User Manual |
| IDENTIFIER | 180ec02c-abe9-443d-8b33-722401b34f58 |
| LANGUAGE | en |
| RIGHTS | Public Domain |
| TITLE | Medrina 0.0.3 User Manual |
| 1 |
Note that the proofs of correctness do not constitute proof that the implementation
of the medrina package is correct; the implementation code is manually translated
from the specification code, and this allows for human error in the transcription
and the possibility of
differing semantics of the execution environment. The specification itself is intended
to provide an unambiguous
description of the behaviour that an implementation should have, and the proofs of
correctness are intended to demonstrate the absence of design flaws in the system
as specified.
References to this footnote:
1
|
symbol_character =
? not (")" | "(" | "[" | "]" | U+0022 | \p{Separator}) ? ;
symbol =
symbol_character , { symbol_character } ;
quoted_character =
? not U+0022 ? ;
quoted_string =
(quoted_character | escape) , { (quoted_character | escape) } ;
escape =
escape_carriage
| escape_newline
| escape_tab
| escape_quote
| escape_unicode4
| escape_unicode8 ;
escape_carriage =
"\r" ;
escape_newline =
"\n" ;
escape_quote =
"\" , U+0022 ;
escape_tab =
"\t" ;
escape_unicode4 =
"\u" ,
hex_digit , hex_digit , hex_digit , hex_digit ;
escape_unicode8 =
"\u" ,
hex_digit , hex_digit , hex_digit , hex_digit ,
hex_digit , hex_digit , hex_digit , hex_digit ;
hex_digit =
"0" | "1" | "2" | "3" | "4" | "5" | "6" | "7" | "8" | "9" | "0" |
"a" | "A" | "b" | "B" | "c" | "C" | "d" | "D" | "e" | "E" | "f" | "F" ;
expression =
symbol
| quoted_string
| "[" , { expression } , "]"
| "(" , { expression } , ")" ;
Definition acceptableCharacters : list Ascii.ascii := list_ascii_of_string "abcdefghijklmnopqrstuvwxyz0123456789_.".
Definition validName (s : string) : Prop := Forall (fun c => In c acceptableCharacters) (list_ascii_of_string s) /\ length s >= 1 /\ length s <= 256.
Theorem validNameDecidable : forall s,
{validName s}+{~validName s}.
Proof.
(* Proof omitted for brevity; see Names.v for proofs. *)
Qed.
Record attributeName := ANMake {
(** The name of the attribute. *)
anName : string;
(** Attribute names are valid. *)
anValid : validName anName
}.
Record attributeValue := AVMake {
(** The value of the attribute. *)
avValue : string;
(** Attribute values are valid. *)
avValid : validName avValue
}.
Theorem attributeNameDec : forall (a b : attributeName),
{a = b}+{a <> b}.
Proof.
(* Proof omitted for brevity; see Attributes.v for proofs. *)
Qed.
Theorem attributeValueDec : forall (a b : attributeValue),
{a = b}+{a <> b}.
Proof.
(* Proof omitted for brevity; see Attributes.v for proofs. *)
Qed.
Record roleName := RNMake {
(** The name of the role. *)
rnName : string;
(** Role names are valid. *)
rnValid : validName rnName
}.
Theorem roleNameDec : forall (a b : roleName),
{a = b}+{a <> b}.
Proof.
(* Proof omitted for brevity; see Roles.v for proofs. *)
Qed.
Record subject := SMake {
(** The roles held by the subject. *)
sRoles : RoleSets.t
}.
Record typeName := TNMake {
(** The name of the type. *)
tnName : string;
(** Type names are valid. *)
tnValid : validName tnName
}.
Theorem typeNameDec : forall (a b : typeName),
{a = b}+{a <> b}.
Proof.
(* Proof omitted for brevity; see Objects.v for proofs. *)
Qed.
Record object := OMake {
(** The object type name. *)
oType : typeName;
(** The attributes held by the object. *)
oAttributes : AttributeNameMaps.t attributeValue
}.
Record actionName := ANMake {
(** The name of the action. *)
anName : string;
(** Action names are valid. *)
anValid : validName anName
}.
Theorem actionNameDec : forall (a b : actionName),
{a = b}+{a <> b}.
Proof.
(* Proof omitted for brevity; see Actions.v for proofs. *)
Qed.
Record action : Set := AMake {
aName : actionName
}.
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 .
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)
.
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.
Theorem exprMatchSubjectEvalEquivalentT : forall s e, true = exprMatchSubjectEvalF s e <-> exprMatchSubjectEvalR s e. Proof. (* Proof omitted for brevity; see Matches.v for proofs. *) Qed.
Theorem exprMatchSubjectEvalEquivalentF : forall s e, false = exprMatchSubjectEvalF s e <-> ~exprMatchSubjectEvalR s e. Proof. (* Proof omitted for brevity; see Matches.v for proofs. *) Qed.
Inductive exprMatchAction : Type := | EMA_False : exprMatchAction | EMA_True : exprMatchAction | EMA_WithName : actionName -> exprMatchAction | EMA_And : list exprMatchAction -> exprMatchAction | EMA_Or : list exprMatchAction -> exprMatchAction .
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)
.
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.
Theorem exprMatchActionEvalEquivalentT : forall s e, true = exprMatchActionEvalF s e <-> exprMatchActionEvalR s e. Proof. (* Proof omitted for brevity; see Matches.v for proofs. *) Qed.
Theorem exprMatchActionEvalEquivalentF : forall a e, false = exprMatchActionEvalF a e <-> ~exprMatchActionEvalR a e. Proof. (* Proof omitted for brevity; see Matches.v for proofs. *) Qed.
Inductive exprMatchObject : Type := | EMO_False : exprMatchObject | EMO_True : exprMatchObject | EMO_WithType : typeName -> exprMatchObject | EMO_And : list exprMatchObject -> exprMatchObject | EMO_Or : list exprMatchObject -> exprMatchObject .
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_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)
.
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_And xs => forallb (exprMatchObjectEvalF o) xs | EMO_Or xs => existsb (exprMatchObjectEvalF o) xs end.
Theorem exprMatchObjectEvalEquivalentT : forall s e, true = exprMatchObjectEvalF s e <-> exprMatchObjectEvalR s e. Proof. (* Proof omitted for brevity; see Matches.v for proofs. *) Qed.
Theorem exprMatchObjectEvalEquivalentF : forall a e, false = exprMatchObjectEvalF a e <-> ~exprMatchObjectEvalR a e. Proof. (* Proof omitted for brevity; see Matches.v for proofs. *) Qed.
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
}.
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.
Definition policy := list rule.
Inductive access : Set := | AccessAllowed | AccessDenied .
Inductive halt : Set := | Halt | HContinue .
Inductive evaluationOfRule : Set := | ERuleMatched : halt -> access -> evaluationOfRule | ERuleDidNotMatch : evaluationOfRule .
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.
Definition evaluateRules (rs : list rule) (s : subject) (o : object) (a : action) : access := evaluateRulesInF AccessDenied rs s o a.
Definition evaluatePolicy (p : policy) (s : subject) (o : object) (a : action) : access := evaluateRules p s o a.
Definition ruleAllows (r : rule) : Prop := ((rConclusion r) = RC_AllowImmediately \/ (rConclusion r) = RC_Allow).
Definition ruleDenies (r : rule) : Prop := ((rConclusion r) = RC_DenyImmediately \/ (rConclusion r) = RC_Deny).
Definition ruleHaltsOnMatch (r : rule) : Prop := ((rConclusion r) = RC_AllowImmediately \/ (rConclusion r) = RC_DenyImmediately).
Definition ruleDoesNotHaltOnMatch (r : rule) : Prop := ((rConclusion r) = RC_Allow \/ (rConclusion r) = RC_Deny).
Definition ruleDoesNotMatch (s : subject) (o : object) (a : action) (r : rule) : Prop := ruleMatchesF s o a r = false.
Definition ruleMatchesWithConclusion (s : subject) (o : object) (a : action) (r : rule) (c : ruleConclusion) : Prop := ruleMatchesF s o a r = true /\ (rConclusion r) = c.
Theorem evaluateRulesDefaultDenyNoMatches : forall rs s o a,
Forall (fun r => ruleMatchesF s o a r = false) rs ->
evaluateRules rs s o a = AccessDenied.
Proof.
(* Proof omitted for brevity; see Policies.v for proofs. *)
Qed.
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.
(* Proof omitted for brevity; see Policies.v for proofs. *)
Qed.
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.
(* Proof omitted for brevity; see Policies.v for proofs. *)
Qed.
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.
(* Proof omitted for brevity; see Policies.v for proofs. *)
Qed.
digit =
"1" | "2" | "3" | "4" | "5" | "6" | "7" | "8" | "9" ;
digit-and-zero =
digit | "0" ;
number =
digit , digit-and-zero* ;
medrina =
"(" , "medrina" , number , number , ")" ;
(medrina 1 0)
ruleConclusion =
"allow"
| "allow-immediately"
| "deny"
| "deny-immediately"
;
matchSubjectE =
"true"
| "false"
| "(" , "with-all-roles" , name* , ")"
| "(" , "with-any-roles" , name* , ")"
| "(" , "or" , matchSubjectE , matchSubjectE , ")"
| "(" , "and" , matchSubjectE , matchSubjectE , ")"
;
matchSubject =
"(" , "subject" , matchSubjectE , ")" ;
(subject
[and (or [with-any-roles x y z]
[with-all-roles a b])
(or true false)])
matchObjectE =
"true"
| "false"
| "(" , "with-type" , name , ")"
| "(" , "or" , matchObjectE , matchObjectE , ")"
| "(" , "and" , matchObjectE , matchObjectE , ")"
;
matchObject =
"(" , "object" , matchObjectE , ")" ;
(object
[and (or [with-type a] [with-type b])
(or true false)])
ruleConclusion =
"allow"
| "allow-immediately"
| "deny"
| "deny-immediately"
;
matchSubjectE =
"true"
| "false"
| "(" , "with-all-roles" , name* , ")"
| "(" , "with-any-roles" , name* , ")"
| "(" , "or" , matchSubjectE , matchSubjectE , ")"
| "(" , "and" , matchSubjectE , matchSubjectE , ")"
;
matchSubject =
"(" , "subject" , matchSubjectE , ")" ;
matchObjectE =
"true"
| "false"
| "(" , "with-type" , name , ")"
| "(" , "or" , matchObjectE , matchObjectE , ")"
| "(" , "and" , matchObjectE , matchObjectE , ")"
;
matchObject =
"(" , "object" , matchObjectE , ")" ;
matchActionE =
"true"
| "false"
| "(" , "with-name" , name , ")"
| "(" , "or" , matchActionE , matchActionE , ")"
| "(" , "and" , matchActionE , matchActionE , ")"
;
matchAction =
"(" , "action" , matchActionE , ")" ;
rule =
"(" , ruleConclusion , matchSubject , matchObject , matchAction , ")" ;
digit =
"1" | "2" | "3" | "4" | "5" | "6" | "7" | "8" | "9" ;
digit-and-zero =
digit | "0" ;
number =
digit , digit-and-zero* ;
medrina =
"(" , "medrina" , number , number , ")" ;
policy =
medrina , rule* ;
matchActionE =
"true"
| "false"
| "(" , "with-name" , name , ")"
| "(" , "or" , matchActionE , matchActionE , ")"
| "(" , "and" , matchActionE , matchActionE , ")"
;
matchAction =
"(" , "action" , matchActionE , ")" ;
(action
[and (or [with-name a] [with-name b])
(or true false)])
rule =
"(" , ruleConclusion , matchSubject , matchObject , matchAction , ")" ;
(deny
(subject
[and (or [with-any-roles x y z]
[with-all-roles a b])
(or true false)])
(object
[and (or [with-type a] [with-type b])
(or true false)])
(action
[and (or [with-name a] [with-name b])
(or true false)]))
ruleConclusion =
"allow"
| "allow-immediately"
| "deny"
| "deny-immediately"
;
matchSubjectE =
"true"
| "false"
| "(" , "with-all-roles" , name* , ")"
| "(" , "with-any-roles" , name* , ")"
| "(" , "or" , matchSubjectE , matchSubjectE , ")"
| "(" , "and" , matchSubjectE , matchSubjectE , ")"
;
matchSubject =
"(" , "subject" , matchSubjectE , ")" ;
matchObjectE =
"true"
| "false"
| "(" , "with-type" , name , ")"
| "(" , "or" , matchObjectE , matchObjectE , ")"
| "(" , "and" , matchObjectE , matchObjectE , ")"
;
matchObject =
"(" , "object" , matchObjectE , ")" ;
matchActionE =
"true"
| "false"
| "(" , "with-name" , name , ")"
| "(" , "or" , matchActionE , matchActionE , ")"
| "(" , "and" , matchActionE , matchActionE , ")"
;
matchAction =
"(" , "action" , matchActionE , ")" ;
rule =
"(" , ruleConclusion , matchSubject , matchObject , matchAction , ")" ;
digit =
"1" | "2" | "3" | "4" | "5" | "6" | "7" | "8" | "9" ;
digit-and-zero =
digit | "0" ;
number =
digit , digit-and-zero* ;
medrina =
"(" , "medrina" , number , number , ")" ;
policy =
medrina , rule* ;
(*
* 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 Medrina.Names.
(** The type of attribute names. *)
Record attributeName := ANMake {
(** The name of the attribute. *)
anName : string;
(** Attribute names are valid. *)
anValid : validName 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 [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.
(** The type of attribute values. *)
Record attributeValue := AVMake {
(** The value of the attribute. *)
avValue : string;
(** Attribute values are valid. *)
avValid : validName 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 [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.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.
(*
* 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.
Import ListNotations.
Require Import Medrina.Actions.
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.
(** 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_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_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_And es => P_And es (e_list es)
| EMO_Or es => P_Or es (e_list es)
end.
End ExprMatchObject_ind.
(** 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_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_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 : forall s e,
true = exprMatchObjectEvalF s e -> exprMatchObjectEvalR s e.
Proof.
intros s e.
induction e as [
|
|
|es Hes
|es Hes
] using exprMatchObject_extendedInd. {
(* EMO_False *)
intros Ht.
inversion Ht.
} {
(* EMO_True *)
intros Ht.
constructor.
} {
(* EMO_WithType *)
intros Ht.
unfold exprMatchObjectEvalF in Ht.
symmetry in Ht.
rewrite eqb_eq in Ht.
pose proof (ivIrrelevantEqual _ _ Ht) as H.
subst n.
constructor.
reflexivity.
} {
(* 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 : forall s e,
exprMatchObjectEvalR s e -> true = exprMatchObjectEvalF s e.
Proof.
intros s e.
induction e as [
|
|
|es Hes
|es Hes
] using exprMatchObject_extendedInd. {
(* EMO_False *)
intros Ht.
inversion Ht.
} {
(* EMO_True *)
intros Ht.
reflexivity.
} {
(* EMO_WithType *)
intros Ht.
simpl.
inversion Ht as [ |y Hyz| | ].
subst y.
pose proof (ivIrrelevantEqual _ _ Hyz) as H0.
rewrite H0.
symmetry.
apply eqb_refl.
} {
(* 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.
} {
(* 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.
}
} {
(* 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.
(*
* 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.
(** 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
}.
(** 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
}.