Medrina 1.0.0 User Manual

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 1.0.0 User Manual

1. Overview

1

The medrina package provides a completely application-neutral implementation of a role-based mandatory access control system.

2. Usage

2.1. Overview
2.2. Loading
2.3. Prepare Data
2.4. Evaluate

2.1. Overview

1

The medrina package provides a simple Java API for loading and evaluating security policies. This section of the documentation explains how to use the API. Security policy authors should read the specification in order to understand how to write and interpret security policies.

2.2. Loading

1

Construct a policy parser factory and use it to parse a given policy file. The parser will throw a checked exception with a list of parse errors if the policy file is malformed. A provided function (in this example, the logStatus function) is called once per error and can be used to log errors or warnings as they occur.

2.2.2. Parse

Path file = ...;
MPolicy policy;

final MPolicyParsers parsers = new MPolicyParsers();
try (MPolicyParserType parser = parsers.createParser(file, logStatus)) {
  policy = parser.execute();
}

3

The provided parser factory expects policy files to conform to the suggested syntax for policy files. Applications are free to store security policies in any format they desire, and to skip this step entirely if necessary. An application with a completely static policy might simply choose to declare the rules directly in source code.

2.3. Prepare Data

1

A security policy is evaluated by checking to see if a given subject is permitted to perform a given action on a given object. These are represented by plain Java record types, and the medrina package does not know or care from where the application takes these objects. This example code constructs the objects directly, but real applications would almost certainly store the information comprising the objects in some kind of database.

2.3.2. Prepare

final MSubject subject =
  new MSubject(
    Set.of(new MRoleName("role0"), new MRoleName("role1"))
  );

final MObject object =
  new MObject(
    new MTypeName("object0"),
    Map.of()
  );

final MActionName action =
  new MActionName("write");

2.4. Evaluate

1

Create a policy evaluator, and use it to evaluate the policy:

2.4.2. Evaluate

final MPolicyEvaluatorType evaluator =
  MPolicyEvaluator.create();

final MPolicyResult result =
  evaluator.evaluate(policy, subject, object, action);

3

The evaluator returns a value of type MPolicyResult containing a result such as ACCESS_DENIED, and a list of the rules in the policy that were evaluated to yield that result. The evaluator is entirely stateless and is safe to use from multiple threads.

3. Specification

3.1. Overview
3.2. Notational Conventions
3.3. Names
3.4. Attributes
3.5. Roles
3.6. Subjects
3.7. Objects
3.8. Actions
3.9. Matches
3.10. Rules
3.11. Policies
3.12. Syntax
3.13. Sources

3.1. Overview

1

This section of the user manual defines the formal specification for the medrina package. The purpose of the specification is to provide a description of the expected behaviour of the package, along with proofs of correctness of various properties of the specification [1].

Footnotes

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

3.2. Notational Conventions

3.2.1. Gallina/Coq
3.2.2. Unicode
3.2.3. EBNF
3.2.4. S-Expressions

3.2.1. Gallina/Coq

1

The formal specification described here is written in the Gallina specification language of the Coq theorem prover. The language is a total, pure-functional, dependently-typed language allowing for describing systems in rigorous detail including machine-checked proofs of various chosen properties.

2

Readers are not expected to be able to understand the bodies of the proof texts, and doing so is not in any case required. As long as one can understand the meaning of the propositions being expressed, it suffices to trust that the proofs are correct as they are all machine-checked whenever the specification is published.

3

The full sources of the entire specification are published at the end of this book.

3.2.2. Unicode

1

The specification makes reference to the Unicode character set which, at the time of writing, is at version 15.0.0. The specification often references specific Unicode characters, and does so using the standard notation U+NNNN, where N represents a hexadecimal digit. For example, U+03BB corresponds to the lowercase lambda symbol λ.

3.2.3. EBNF

1

The specification gives grammar definitions in ISO/IEC 14977:1996 Extended Backus-Naur form.

2

Because EBNF was designed prior to the existence of Unicode, it is necessary to extend the syntax to be able to refer to Unicode characters in grammar definitions. This specification makes use of the standard unicode U+NNNN syntax in grammar definitions, to refer to specific Unicode characters. It also makes use of the syntax \p{t} which should be understood to represent any Unicode character with the property t. For example, \p{Lowercase_Letter} describes the set of characters that are both letters and are lowercase. The syntax \P{t} should be understood as the negation of \p{t}; it describes the set of characters without the property t.

3.2.4. S-Expressions

1

The medrina policy language uses s-expressions as the base for all syntax. An s-expression is described by the following EBNF grammar:

3.2.4.2. S-Expression Syntax

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 } , ")" ;

3

As shown, the medrina language uses an extension of basic s-expressions that allow for the optional use of either square brackets or parentheses to increase the readability of large nested expressions. These should be treated as interchangeable, but must be correctly balanced as shown by the grammar. For example, the expression [] is semantically equivalent to (), but the expression [) is invalid.

3.3. Names

1

Many objects mentioned in this specification have names.

2

A name is a dotted name taken from the Lanark specification.

3

Details can be found in the specification, but informally, names adhere to the following regular expression:

3.3.4. Regex

([a-z][a-z0-9_-]{0,63})(\.[a-z][a-z0-9_-]{0,62}){0,15}

3.4. Attributes

1

An attribute is a named value held by an object.

2

Attribute names are valid names:

3.4.3. Attribute Names

Record attributeName := ANMake {
  (** The name of the attribute. *)
  anName  : name;
  (** Attribute names are valid. *)
  anValid : nameValid anName
}.

4

Attribute values are valid names:

3.4.5. Attribute Values

Record attributeValue := AVMake {
  (** The value of the attribute. *)
  avValue : name;
  (** Attribute values are valid. *)
  avValid : nameValid avValue
}.

6

Equality of both attribute names and attribute values is decidable:

3.4.7. Attribute Names (Decidable)

Theorem attributeNameDec : forall (a b : attributeName),
  {a = b}+{a <> b}.
Proof.
  (* Proof omitted for brevity; see Attributes.v for proofs. *)
Qed.

3.4.8. Attribute Values (Decidable)

Theorem attributeValueDec : forall (a b : attributeValue),
  {a = b}+{a <> b}.
Proof.
  (* Proof omitted for brevity; see Attributes.v for proofs. *)
Qed.

3.5. Roles

1

A role is a value held by a subject.

2

Role names are valid names:

3.5.3. Role Names

Record roleName := RNMake {
  (** The name of the role. *)
  rnName  : string;
  (** Role names are valid. *)
  rnValid : validName rnName
}.

4

Equality of role names is decidable:

3.5.5. Roles (Decidable)

Theorem roleNameDec : forall (a b : roleName),
  {a = b}+{a <> b}.
Proof.
  (* Proof omitted for brevity; see Roles.v for proofs. *)
Qed.

3.6. Subjects

1

A subject represents an entity attempting to perform an action. A subject is in possession of a set of zero or more roles:

3.6.2. Subjects

Record subject := SMake {
  (** The roles held by the subject. *)
  sRoles : RoleSets.t
}.

3.7. Objects

1

An object is an entity upon which subjects may attempt to perform actions.

2

An object has an associated type. Type names are valid names and have decidable equality:

3.7.3. Type Names

Record typeName := TNMake {
  (** The name of the type. *)
  tnName  : string;
  (** Type names are valid. *)
  tnValid : validName tnName
}.

3.7.4. Type Names (Decidable)

Theorem typeNameDec : forall (a b : typeName),
  {a = b}+{a <> b}.
Proof.
  (* Proof omitted for brevity; see Objects.v for proofs. *)
Qed.

5

An object has a set of associated attributes:

3.7.6. Objects

Record object := OMake {
  (** The object type name. *)
  oType : typeName;
  (** The attributes held by the object. *)
  oAttributes : AttributeNameMaps.t attributeValue
}.

3.8. Actions

1

An action is an operation that can be performed on an object by a subject.

2

An action has a valid name with decidable equality:

3.8.3. Action Names

Record actionName := ANMake {
  (** The name of the action. *)
  anName  : string;
  (** Action names are valid. *)
  anValid : validName anName
}.

3.8.4. Action Names (Decidable)

Theorem actionNameDec : forall (a b : actionName),
  {a = b}+{a <> b}.
Proof.
  (* Proof omitted for brevity; see Actions.v for proofs. *)
Qed.

3.8.5. Actions

Record action : Set := AMake {
  aName : actionName
}.

3.9. Matches

3.9.1. Overview
3.9.2. Matching Subjects
3.9.3. Matching Actions
3.9.4. Matching Objects

3.9.1. Overview

1

A medrina security policy is evaluated by matching a subject, object, and action against a sequence of rules.

3.9.2. Matching Subjects

1

The expression used to match a subject is described by the following inductive type:

3.9.2.2. exprMatchSubject

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
  .

3

The expression, when evaluated, matches a subject when any of the following conditions hold:

3.9.2.4. exprMatchSubjectEvalR

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)
  .

3.9.2.5. exprMatchSubjectEvalR Description

The expression EMS_False never matches any subject. Note that there is no corresponding relationship expressed in the exprMatchSubjectEvalR type.
The expression EMS_True trivially matches any subject.
The expression EMS_WithRolesAll r matches any subject s where r is a subset of the roles held by s.
The expression EMS_WithRolesAny r matches any subject s where s has at least one of the roles in r.
The expression EMS_And es matches when all the subexpressions in es match.
The expression EMS_Or es matches when any of the subexpressions in es match.

6

Given a subject s and expression e, the following evaluation function returns true if e matches s:

3.9.2.7. exprMatchSubjectEvalF

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.

8

The evaluation function and the evaluation relation are equivalent.

3.9.2.9. exprMatchSubjectEvalEquivalentT

Theorem exprMatchSubjectEvalEquivalentT : forall s e,
  true = exprMatchSubjectEvalF s e <-> exprMatchSubjectEvalR s e.
Proof.
  (* Proof omitted for brevity; see Matches.v for proofs. *)
Qed.

3.9.2.10. exprMatchSubjectEvalEquivalentF

Theorem exprMatchSubjectEvalEquivalentF : forall s e,
  false = exprMatchSubjectEvalF s e <-> ~exprMatchSubjectEvalR s e.
Proof.
  (* Proof omitted for brevity; see Matches.v for proofs. *)
Qed.

11

It follows that, for an expression EMS_WithRolesAll a, if a is empty the expression will trivially match any subject:

3.9.2.12. exprMatchSubjectEvalRolesAllEmpty

Theorem exprMatchSubjectEvalRolesAllEmpty : forall s,
  true = exprMatchSubjectEvalF s (EMS_WithRolesAll RoleSets.empty).
Proof.
  (* Proof omitted for brevity; see Matches.v for proofs. *)
Qed.

13

For an expression EMS_WithRolesAny a, if a is empty the expression will never match any subject:

3.9.2.14. exprMatchSubjectEvalRolesAnyEmpty

Theorem exprMatchSubjectEvalRolesAnyEmpty : forall s,
  false = exprMatchSubjectEvalF s (EMS_WithRolesAny RoleSets.empty).
Proof.
  (* Proof omitted for brevity; see Matches.v for proofs. *)
Qed.

3.9.3. Matching Actions

1

The expression used to match an action is described by the following inductive type:

3.9.3.2. exprMatchAction

Inductive exprMatchAction : Type :=
  | EMA_False    : exprMatchAction
  | EMA_True     : exprMatchAction
  | EMA_WithName : actionName -> exprMatchAction
  | EMA_And      : list exprMatchAction -> exprMatchAction
  | EMA_Or       : list exprMatchAction -> exprMatchAction
  .

3

The expression, when evaluated, matches an action when any of the following conditions hold:

3.9.3.4. exprMatchActionEvalR

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)
  .

3.9.3.5. exprMatchActionEvalR Description

The expression EMA_False never matches any action. Note that there is no corresponding relationship expressed in the exprMatchActionEvalR type.
The expression EMA_True trivially matches any action.
The expression EMA_WithName n matches any action a where a has the name n.
The expression EMA_And es matches when all the subexpressions in es match.
The expression EMA_Or es matches when any of the subexpressions in es match.

6

Given an action a and expression e, the following evaluation function returns true if e matches a:

3.9.3.7. exprMatchActionEvalF

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.

8

The evaluation function and the evaluation relation are equivalent.

3.9.3.9. exprMatchActionEvalEquivalentT

Theorem exprMatchActionEvalEquivalentT : forall s e,
  true = exprMatchActionEvalF s e <-> exprMatchActionEvalR s e.
Proof.
  (* Proof omitted for brevity; see Matches.v for proofs. *)
Qed.

3.9.3.10. exprMatchActionEvalEquivalentF

Theorem exprMatchActionEvalEquivalentF : forall a e,
  false = exprMatchActionEvalF a e <-> ~exprMatchActionEvalR a e.
Proof.
  (* Proof omitted for brevity; see Matches.v for proofs. *)
Qed.

3.9.4. Matching Objects

1

The expression used to match an object is described by the following inductive type:

3.9.4.2. exprMatchObject

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
  .

3

The expression, when evaluated, matches an object when any of the following conditions hold:

3.9.4.4. exprMatchObjectEvalR

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)
  .

3.9.4.5. exprMatchObjectEvalR Description

The expression EMO_False never matches any object. Note that there is no corresponding relationship expressed in the exprMatchObjectEvalR type.
The expression EMO_True trivially matches any object.
The expression EMO_WithType t matches any object o where o has the type t.
The expression EMO_WithAttributesAll a matches any object o where o has (at least) all the attributes in a. More formally, for each attribute k in a, an attribute m must be held by o where k = m.
The expression EMO_WithAttributesAny a matches any object o where o has at least one of the attributes in a.
The expression EMO_And es matches when all the subexpressions in es match.
The expression EMO_Or es matches when any of the subexpressions in es match.

6

Given an object o and expression e, the following evaluation function returns true if e matches o:

3.9.4.7. exprMatchObjectEvalF

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.

8

The evaluation function and the evaluation relation are equivalent.

3.9.4.9. exprMatchObjectEvalEquivalentT

Theorem exprMatchObjectEvalEquivalentT : forall s e,
  true = exprMatchObjectEvalF s e <-> exprMatchObjectEvalR s e.
Proof.
  (* Proof omitted for brevity; see Matches.v for proofs. *)
Qed.

3.9.4.10. exprMatchObjectEvalEquivalentF

Theorem exprMatchObjectEvalEquivalentF : forall a e,
  false = exprMatchObjectEvalF a e <-> ~exprMatchObjectEvalR a e.
Proof.
  (* Proof omitted for brevity; see Matches.v for proofs. *)
Qed.

11

It follows that, for an expression EMO_WithAttributesAll a, if a is empty the expression will trivially match any object:

3.9.4.12. exprMatchObjectWithAllEmpty

Theorem exprMatchObjectWithAllEmpty : forall o,
  exprMatchObjectEvalF o (EMO_WithAttributesAll (AttributeNameMaps.empty attributeValue)) = true.
Proof.
  (* Proof omitted for brevity; see Matches.v for proofs. *)
Qed.

13

For an expression EMO_WithAttributesAny a, if a is empty the expression will never match any object:

3.9.4.14. exprMatchObjectWithAnyEmpty

Theorem exprMatchObjectWithAnyEmpty : forall o,
  exprMatchObjectEvalF o (EMO_WithAttributesAny (AttributeNameMaps.empty attributeValue)) = false.
Proof.
  (* Proof omitted for brevity; see Matches.v for proofs. *)
Qed.

3.10. Rules

1

A rule consists of a conclusion, an expression that may match a subject, an expression that may match an action, and an expression that may match an object.

3.10.2. Rule

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;
}.

3

A rule also has a name that must be unique within a policy, and a description providing humanly-readable documentation of the rule. Neither of these elements are used anywhere else in the specification, but are included for completeness.

4

A conclusion is one of the following values:

3.10.5. Conclusion

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
  .

3.10.6. Conclusion Description

A value of RC_Allow indicates that the action in question should be allowed, assuming that no further rules cause the action to be denied.
A value of RC_AllowImmediately indicates that the action in question should be allowed, and no further rules should be evaluated.
A value of RC_Deny indicates that the action in question should be denied, assuming that no further rules cause the action to be allowed.
A value of RC_DenyImmediately indicates that the action in question should be denied, and no further rules should be evaluated.

7

A rule matches against a subject, object, and action iff all the expressions contained within it match:

3.10.8. ruleMatchesR

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.

9

The following evaluation function returns true iff the expressions evaluate to true:

3.10.10. ruleMatchesF

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.

11

The evaluation function and the evaluation relation are equivalent.

3.10.12. ruleMatchesFEquivalentT

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.

3.10.13. ruleMatchesFEquivalentF

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.

3.11. Policies

3.11.1. Overview
3.11.2. Evaluation
3.11.3. Properties
- 3.11.3.1. Abbreviation
- 3.11.3.2. Theorems

3.11.1. Overview

1

A policy is a sequence of rules. A given subject, object, and action are matched against each of the rules of the policy in order to determine whether the given action should be permitted or denied.

3.11.1.2. Policy

Definition policy :=
  list rule.

3.11.2. Evaluation

1

Evaluation of a policy is expressed as a total function from a policy to an access value.

3.11.2.2. Access

Inductive access : Set :=
  | AccessAllowed
  | AccessDenied
  .

3.11.2.3. Access Description

A value of AccessAllowed indicates that the action should be permitted.
A value of AccessDenied indicates that the action should be denied.

4

Evaluating a rule may cause evaluation of subsequent rules to be cancelled.

3.11.2.5. Halt

Inductive halt : Set :=
  | Halt
  | HContinue
  .

3.11.2.6. Halt Description

A value of Halt indicates that no further rules should be evaluated.
A value of HContinue indicates that evaluation of rules should continue.

7

Evaluating a rule has two possible outcomes; the rule matches and returns a halt and access value, or the rule fails to match. This is described by the following inductive type:

3.11.2.8. evaluationOfRule

Inductive evaluationOfRule : Set :=
  | ERuleMatched     : halt -> access -> evaluationOfRule
  | ERuleDidNotMatch : evaluationOfRule
  .

9

The evaluateRule function describes how a single rule is evaluated:

3.11.2.10. evaluateRule

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.

11

The evaluateRulesInF function describes how a list of rules is recursively evaluated:

3.11.2.12. evaluateRulesInF

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.

13

Informally, the body of the evaluateRulesInF maintains a notion of the current access value. If no rule has been evaluated yet, the current access value is a value set by the caller. In this specification, the only caller is the evaluateRules function, which assumes a starting value of AccessDenied. The function checks if the current rule matches. If the current rule does match, the function effectively sets the current access value to that returned by the rule. If the current rule specifies that evaluation should halt, the current access value is returned immediately. If the current rule specifies that evaluation should continue, the rest of the rules are evaluated with the newly set access value. Otherwise, if the rule does not match, the rest of the rules are evaluated with the current access value left unchanged.

14

Subsequently, the evaluateRules and evaluatePolicy functions describe how an entire policy is evaluated.

3.11.2.15. evaluateRules

Definition evaluateRules
  (rs  : list rule)
  (s   : subject)
  (o   : object)
  (a   : action)
: access :=
  evaluateRulesInF AccessDenied rs s o a.

3.11.2.16. evaluatePolicy

Definition evaluatePolicy
  (p : policy)
  (s : subject)
  (o : object)
  (a : action)
: access :=
  evaluateRules p s o a.

3.11.3. Properties

3.11.3.1. Abbreviation

1

In order to succinctly describe various properties of policy evaluation, numerous shorthand propositions are used. These propositions do not actually define any new information; they are simply used to make the various theorems and proofs shorter to read.

2

The proposition ruleAllows r states that r has a conclusion that would result in an action being permitted.

3.11.3.1.3. ruleAllows

Definition ruleAllows (r : rule) : Prop :=
  ((rConclusion r) = RC_AllowImmediately \/ (rConclusion r) = RC_Allow).

4

The proposition ruleDenies r states that r has a conclusion that would result in an action being denied.

3.11.3.1.5. ruleDenies

Definition ruleDenies (r : rule) : Prop :=
  ((rConclusion r) = RC_DenyImmediately \/ (rConclusion r) = RC_Deny).

6

The proposition ruleHaltsOnMatch r states that r has a conclusion that would result in evaluation being halted if the rule was to match.

3.11.3.1.7. ruleHaltsOnMatch

Definition ruleHaltsOnMatch (r : rule) : Prop :=
  ((rConclusion r) = RC_AllowImmediately \/ (rConclusion r) = RC_DenyImmediately).

8

The proposition ruleDoesNotHaltOnMatch r states that r has a conclusion that would result in evaluation being continued if the rule was to match.

3.11.3.1.9. ruleDoesNotHaltOnMatch

Definition ruleDoesNotHaltOnMatch (r : rule) : Prop :=
  ((rConclusion r) = RC_Allow \/ (rConclusion r) = RC_Deny).

10

The proposition ruleDoesNotMatch ... r states that r does not match against the given inputs.

3.11.3.1.11. ruleDoesNotMatch

Definition ruleDoesNotMatch
  (s : subject)
  (o : object)
  (a : action)
  (r : rule)
: Prop :=
  ruleMatchesF s o a r = false.

12

The proposition ruleMatchesWithConclusion ... r c states that r matches against the given inputs and has the conclusion c.

3.11.3.1.13. ruleMatchesWithConclusion

Definition ruleMatchesWithConclusion
  (s : subject)
  (o : object)
  (a : action)
  (r : rule)
  (c : ruleConclusion)
: Prop :=
  ruleMatchesF s o a r = true /\ (rConclusion r) = c.

3.11.3.2. Theorems

1

If no rules in a policy match, the default is to deny access.

3.11.3.2.2. evaluateRulesDefaultDenyNoMatches

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.

3

If a policy consists of a possibly-empty 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.

3.11.3.2.4. evaluateRulesLastMatchingPreNoHalt

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.

5

If a policy consists of a possibly-empty sequence of rules r_pre, followed by a possibly-empty sequence of rules r_post that do not match, then evaluation is equivalent to evaluating r_pre.

3.11.3.2.6. evaluateRulesPostNotMatching

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.

7

If a policy consists of a possibly-empty sequence of rules r_pre that do not match, followed by a possibly-empty sequence of rules r_post, then evaluation is equivalent to evaluating r_post.

3.11.3.2.8. evaluateRulesPreNotMatching

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.

3.12. Syntax

3.12.1. Overview
3.12.2. Medrina
3.12.3. Rule Conclusions
3.12.4. Subject Match
3.12.5. Object Match
3.12.6. Complete Syntax
3.12.7. Action Match
3.12.8. Rules
3.12.9. Complete Syntax

digit =
  "1" | "2" | "3" | "4" | "5" | "6" | "7" | "8" | "9" ;

digit-and-zero =
  digit | "0" ;

number =
  digit , digit-and-zero* ;

medrina =
  "(" , "Medrina" , number , number , ")" ;

3.12.2.3. Medrina (Example)

(Medrina 1 0)

3.12.3. Rule Conclusions

1

Rule conclusions are expressed with the following syntax:

3.12.3.2. Rule Conclusions

ruleConclusion =
    "Allow"
  | "AllowImmediately"
  | "Deny"
  | "DenyImmediately"
  ;

3.12.3.3. Rule Conclusions (Example)

Allow

4

Inside rule declarations, conclusions are expressed using the following syntax:

3.12.3.5. Rule Conclusion Expressions

ruleConclusionE =
  "(" , "Conclusion" , ruleConclusion , ")"
  ;

3.12.3.6. Rule Conclusion Expressions (Example)

(Conclusion Allow)

3.12.4. Subject Match

1

Subject match expressions are expressed with the following syntax:

3.12.4.2. Subject Match

matchSubjectE =
    "True"
  | "False"
  | "(" , "WithAllRolesFrom" , name* , ")"
  | "(" , "WithAnyRolesFrom" , name* , ")"
  | "(" , "Or" , matchSubjectE , matchSubjectE , ")"
  | "(" , "And" , matchSubjectE , matchSubjectE , ")"
  ;

matchSubject =
  "(" , "MatchSubject" , matchSubjectE , ")" ;

3.12.4.3. Subject Match (Example)

(MatchSubject
  [And (Or [WithAnyRolesFrom x y z]
           [WithAllRolesFrom a b])
       (Or True False)])

3.12.5. Object Match

1

Object match expressions are expressed with the following syntax:

3.12.5.2. Object Match

attribute =
  "(" , "Attribute" , name , name , ")" ;

matchObjectE =
    "True"
  | "False"
  | "(" , "WithType" , name , ")"
  | "(" , "WithAllAttributesFrom" , attribute* , ")"
  | "(" , "WithAnyAttributesFrom" , attribute* , ")"
  | "(" , "Or" , matchObjectE , matchObjectE , ")"
  | "(" , "And" , matchObjectE , matchObjectE , ")"
  ;

matchObject =
  "(" , "MatchObject" , matchObjectE , ")" ;

3.12.5.3. Object Match (Example)

(MatchObject
  [And (Or [WithType a] [WithType b])
       (WithAllAttributesFrom [attribute x z] [attribute y b])
       (Or True False)])

3.12.6. Complete Syntax

1

The complete syntax is as follows:

3.12.6.2. Complete Syntax

ruleConclusion =
    "Allow"
  | "AllowImmediately"
  | "Deny"
  | "DenyImmediately"
  ;

ruleConclusionE =
  "(" , "Conclusion" , ruleConclusion , ")"
  ;

matchSubjectE =
    "True"
  | "False"
  | "(" , "WithAllRolesFrom" , name* , ")"
  | "(" , "WithAnyRolesFrom" , name* , ")"
  | "(" , "Or" , matchSubjectE , matchSubjectE , ")"
  | "(" , "And" , matchSubjectE , matchSubjectE , ")"
  ;

matchSubject =
  "(" , "MatchSubject" , matchSubjectE , ")" ;

attribute =
  "(" , "Attribute" , name , name , ")" ;

matchObjectE =
    "True"
  | "False"
  | "(" , "WithType" , name , ")"
  | "(" , "WithAllAttributesFrom" , attribute* , ")"
  | "(" , "WithAnyAttributesFrom" , attribute* , ")"
  | "(" , "Or" , matchObjectE , matchObjectE , ")"
  | "(" , "And" , matchObjectE , matchObjectE , ")"
  ;

matchObject =
  "(" , "MatchObject" , matchObjectE , ")" ;

matchActionE =
    "True"
  | "False"
  | "(" , "WithName" , name , ")"
  | "(" , "Or" , matchActionE , matchActionE , ")"
  | "(" , "And" , matchActionE , matchActionE , ")"
  ;

matchAction =
  "(" , "MatchAction" , matchActionE , ")" ;

ruleName =
  "(" , "Name" , name , ")" ;

ruleDescription =
  "(" , "Description" , quoted , ")" ;

ruleElement =
    ruleName?
  | ruleDescription?
  | ruleConclusionE
  | matchSubject
  | matchObject
  | matchAction
  ;

rule =
  "(" , "Rule" , ruleElement* , ")" ;

quoted =
  <Any s-expression quoted string> ;

name =
  <A valid Lanark dotted name> ;

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* ;

3.12.7. Action Match

1

Action match expressions are expressed with the following syntax:

3.12.7.2. Action Match

matchActionE =
    "True"
  | "False"
  | "(" , "WithName" , name , ")"
  | "(" , "Or" , matchActionE , matchActionE , ")"
  | "(" , "And" , matchActionE , matchActionE , ")"
  ;

matchAction =
  "(" , "MatchAction" , matchActionE , ")" ;

3.12.7.3. Action Match (Example)

(MatchAction
  [And (Or [WithName a] [WithName b])
       (Or True False)])

3.12.8. Rules

1

Rules are expressed with the following syntax:

3.12.8.2. Rule

ruleName =
  "(" , "Name" , name , ")" ;

ruleDescription =
  "(" , "Description" , quoted , ")" ;

ruleElement =
    ruleName?
  | ruleDescription?
  | ruleConclusionE
  | matchSubject
  | matchObject
  | matchAction
  ;

rule =
  "(" , "Rule" , ruleElement* , ")" ;

3.12.8.3. Rule (Example)

[Rule
  [Name rule0]
  [Description "A rule."]
  [Conclusion Deny]
  [MatchSubject
    [And (Or [WithAnyRolesFrom x y z]
             [WithAllRolesFrom a b])
         (Or True False)]]
  [MatchObject
    [And (Or [WithType a] [WithType b])
         (Or True False)]]
  [MatchAction
    [And (Or [WithName a] [WithName b])
         (Or True False)]]
]

3.12.9. Complete Syntax

1

The complete syntax is as follows:

3.12.9.2. Complete Syntax

ruleConclusion =
    "Allow"
  | "AllowImmediately"
  | "Deny"
  | "DenyImmediately"
  ;

ruleConclusionE =
  "(" , "Conclusion" , ruleConclusion , ")"
  ;

matchSubjectE =
    "True"
  | "False"
  | "(" , "WithAllRolesFrom" , name* , ")"
  | "(" , "WithAnyRolesFrom" , name* , ")"
  | "(" , "Or" , matchSubjectE , matchSubjectE , ")"
  | "(" , "And" , matchSubjectE , matchSubjectE , ")"
  ;

matchSubject =
  "(" , "MatchSubject" , matchSubjectE , ")" ;

attribute =
  "(" , "Attribute" , name , name , ")" ;

matchObjectE =
    "True"
  | "False"
  | "(" , "WithType" , name , ")"
  | "(" , "WithAllAttributesFrom" , attribute* , ")"
  | "(" , "WithAnyAttributesFrom" , attribute* , ")"
  | "(" , "Or" , matchObjectE , matchObjectE , ")"
  | "(" , "And" , matchObjectE , matchObjectE , ")"
  ;

matchObject =
  "(" , "MatchObject" , matchObjectE , ")" ;

matchActionE =
    "True"
  | "False"
  | "(" , "WithName" , name , ")"
  | "(" , "Or" , matchActionE , matchActionE , ")"
  | "(" , "And" , matchActionE , matchActionE , ")"
  ;

matchAction =
  "(" , "MatchAction" , matchActionE , ")" ;

ruleName =
  "(" , "Name" , name , ")" ;

ruleDescription =
  "(" , "Description" , quoted , ")" ;

ruleElement =
    ruleName?
  | ruleDescription?
  | ruleConclusionE
  | matchSubject
  | matchObject
  | matchAction
  ;

rule =
  "(" , "Rule" , ruleElement* , ")" ;

quoted =
  <Any s-expression quoted string> ;

name =
  <A valid Lanark dotted name> ;

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* ;

3.13. Sources

1

The full sources for the Coq/Gallina model underlying this specification are included here.

3.13.2. Medrina/Actions.v

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

3.13.3. Medrina/Attributes.v

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

3.13.4. Medrina/Matches.v

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

3.13.5. Medrina/Names.v

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

3.13.6. Medrina/Objects.v

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

3.13.7. Medrina/Policies.v

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

3.13.8. Medrina/Roles.v

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

3.13.9. Medrina/Rules.v

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

3.13.10. Medrina/Subjects.v

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

Medrina 1.0.0 User Manual

Table Of Contents

Footnotes