path: root/xacml-proofs/lean/Xacml.lean

------------------------------------------------------------------------
---- Atoms -------------------------------------------------------------
------------------------------------------------------------------------
--
-- # References
--
-- - 7.6 Match evaluation
--
------------------------------------------------------------------------

inductive MatchResult where
  | is_match      : MatchResult
  | no_match      : MatchResult
  | indeterminate : MatchResult
deriving BEq, Repr

inductive Decision where
  | permit           : Decision
  | deny             : Decision
  | indeterminate    : Decision
  | not_applicable   : Decision
deriving BEq, Repr

-- This type is used to implement the semantics described in § 7.10 (Extended
-- Indeterminate). It is only relevant to combining algorithms.
inductive Decision' where
  | permit           : Decision'
  | deny             : Decision'
  | indeterminate    : Decision'
  | indeterminate_d  : Decision'
  | indeterminate_p  : Decision'
  | indeterminate_dp : Decision'
  | not_applicable   : Decision'
deriving BEq, Repr

instance : Coe Decision' Decision where
  coe b :=
    match b with
      | Decision'.permit           => Decision.permit
      | Decision'.deny             => Decision.deny
      | Decision'.indeterminate    => Decision.indeterminate
      | Decision'.indeterminate_d  => Decision.indeterminate
      | Decision'.indeterminate_p  => Decision.indeterminate
      | Decision'.indeterminate_dp => Decision.indeterminate
      | Decision'.not_applicable   => Decision.not_applicable

inductive EffectType where
  | permit : EffectType
  | deny   : EffectType
deriving BEq, Repr

namespace EffectType
  def to_decision (e : EffectType) : Decision :=
    match e with
    | EffectType.permit => Decision.permit
    | EffectType.deny   => Decision.deny

  def to_decision' (e : EffectType) : Decision' :=
    match e with
    | EffectType.permit => Decision'.permit
    | EffectType.deny   => Decision'.deny
end EffectType

------------------------------------------------------------------------
---- Values ------------------------------------------------------------
------------------------------------------------------------------------
--
-- From A.2 Data-types: "Although XML instances represent all data-types
-- as strings, an XACML PDP must operate on types of data that, while
-- they have string representations, are not just strings. Types such as
-- Boolean, integer, and double MUST be converted from their XML string
-- representations to values that can be compared with values in their
-- domain of discourse, such as numbers."
--
-- The standard enumerates the types that must be supported by any
-- conforming implementaiton. This is represented in `XmlType`, and
-- `Value` is the representation of a value payload with its associated
-- type.
--
------------------------------------------------------------------------

inductive XmlType
  | string            : XmlType
  | boolean           : XmlType
  | integer           : XmlType
  | double            : XmlType
  | time              : XmlType
  | date              : XmlType
  | dateTime          : XmlType
  | anyURI            : XmlType
  | hexBinary         : XmlType
  | base64Binary      : XmlType
  | dayTimeDuration   : XmlType
  | yearMonthDuration : XmlType
  | x500Name          : XmlType
  | rfc822Name        : XmlType
  | ipAddress         : XmlType
  | dnsName           : XmlType
deriving BEq, Repr

def Primitive : Type := XmlType × String
deriving BEq, Repr

def Primitive.mk (type : XmlType) (inner : String) : Primitive := (type, inner)

notation:65 "#<" lhs:65 "," rhs:66 ">" => Primitive.mk lhs rhs

instance : Coe Bool Primitive where
  coe b :=
    match b with
      | true  => #<XmlType.boolean, "True">
      | false => #<XmlType.boolean, "False">

-- Per 7.4 Expression evaluation,
--
-- "XACML defines an evaluation result of "Indeterminate", which is said
-- to be the result of an invalid expression, or an operational error
-- occurring during the evaluation of the expression."

instance : Coe (Option Primitive) Primitive where
  coe b :=
    match b with
      | Option.none   => #<XmlType.boolean, "Indeterminate">
      | Option.some a => a

structure Bag where
  contents: List Primitive
deriving Repr

def List.count [BEq α] (xs : List α) (x : α) : Int :=
  (xs.filter (fun y => y == x)).length

def Bag.beq (b₁ b₂ : Bag) : Bool :=
  b₁.contents.all (fun x => b₂.contents.count x == b₁.contents.count x)

instance : BEq Bag where
  beq := Bag.beq

inductive Value where
  | primitive (p : Primitive) : Value
  | bag (b : Bag)             : Value
deriving BEq, Repr

instance : Coe (Option Value) Value where
  coe b :=
    match b with
      | Option.none   => Value.primitive (#<XmlType.boolean, "Indeterminate">)
      | Option.some a => a

instance : Coe (Option Value) MatchResult where
  coe b :=
    match b with
      | Option.some (Value.primitive (XmlType.boolean, "True"))          => MatchResult.is_match
      | Option.some (Value.primitive (XmlType.boolean, "False"))         => MatchResult.no_match
      | _                                                                => MatchResult.indeterminate

------------------------------------------------------------------------
---- Attributes---------------------------------------------------------
------------------------------------------------------------------------
--
-- # References
--
-- - 5.46 Element <Attribute>
-- - 5.42 Element <Request>
--
-- Attributes are categories into <Attributes> elements. In this
-- implementation, categories are rolled up - every attribute carries
-- the category of its enclosing <Attributes> element.
--
------------------------------------------------------------------------

structure Attribute where
  category   : String
  identifier : String
  issuer     : Option String
  value      : Primitive
deriving Repr

-- More than one attribute with a particular (category, identifier, issuer) can
-- exist in a `Request`. Indeed, this is how poly-valued attributes are
-- represented.

def Request : Type := List Attribute
deriving Repr

---

def Identifier : Type := String
deriving BEq, Repr

inductive RuleCombinatorAlgorithm where
  | deny_overrides                  : RuleCombinatorAlgorithm
  | ordered_deny_overrides          : RuleCombinatorAlgorithm
  | permit_overrides                : RuleCombinatorAlgorithm
  | ordered_permit_overrides        : RuleCombinatorAlgorithm
  | deny_unless_permit              : RuleCombinatorAlgorithm
  | permit_unless_deny              : RuleCombinatorAlgorithm
  | first_applicable                : RuleCombinatorAlgorithm
  | legacy_deny_overrides           : RuleCombinatorAlgorithm
  | legacy_ordered_deny_overrides   : RuleCombinatorAlgorithm
  | legacy_permit_overrides         : RuleCombinatorAlgorithm
  | legacy_ordered_permit_overrides : RuleCombinatorAlgorithm

namespace RuleCombinatorAlgorithm
  -- The output of a combining algorithm which does not track the extended set
  -- of “Indeterminate” values MUST be treated as “Indeterminate{DP}” for the
  -- value “Indeterminate” by a combining algorithm which tracks the extended
  -- set of “Indeterminate” values. A combining algorithm which does not track
  -- the extended set of “Indeterminate” values MUST treat the output of a
  -- combining algorithm which tracks the extended set of “Indeterminate” values
  -- as an “Indeterminate” for any of the possible values of the extended set of
  -- “Indeterminate”.

  def eval_deny_overrides (results : List Decision') : Decision' :=
    if results.elem Decision'.deny then Decision'.deny else
    if results.elem Decision'.indeterminate_dp then Decision'.indeterminate_dp else
    if results.elem Decision'.indeterminate_d ∧ results.elem Decision'.indeterminate_p then Decision'.indeterminate_dp else
    if results.elem Decision'.indeterminate_d then Decision'.indeterminate_d else
    if results.elem Decision'.permit then Decision'.permit else
    if results.elem Decision'.indeterminate_p then Decision'.indeterminate_p else
    Decision'.not_applicable
  def eval_ordered_deny_overrides : List Decision' -> Decision' := eval_deny_overrides

  def eval_permit_overrides (results : List Decision') : Decision' :=
    if results.elem Decision'.permit then Decision'.permit else
    if results.elem Decision'.indeterminate_dp then Decision'.indeterminate_dp else
    if results.elem Decision'.indeterminate_d ∧ results.elem Decision'.indeterminate_p then Decision'.indeterminate_dp else
    if results.elem Decision'.indeterminate_p then Decision'.indeterminate_p else
    if results.elem Decision'.deny then Decision'.deny else
    if results.elem Decision'.indeterminate_d then Decision'.indeterminate_d else
    Decision'.not_applicable
  def eval_ordered_permit_overrides : List Decision' -> Decision' := eval_permit_overrides

  def eval_deny_unless_permit (results : List Decision') : Decision' :=
    if results.elem Decision'.permit then Decision'.permit else Decision'.deny

  def eval_permit_unless_deny (results : List Decision') : Decision' :=
    if results.elem Decision'.deny then Decision'.deny else Decision'.permit

  -- The non-normative part of the specification asserts that "If an error
  -- occurs while evaluating the target or condition of a rule, then the
  -- evaluation SHALL halt, and the policy shall evaluate to "Indeterminate",
  -- with the appropriate error status."
  --
  -- This behavior isn't spelled out in the normative part, because errors are
  -- represented as an Indeterminate.
  def eval_first_applicable (results : List Decision') : Decision' :=
    match (results.filter (fun d => d != Decision'.not_applicable)).get? 0 with
      | some a => a
      | none => Decision'.not_applicable

  def eval_legacy_deny_overrides (results : List Decision') : Decision' :=
    -- Note that "any rule having Effect=Deny evaluates to Indeterminate"
    -- corresponds to indeterminate_d, and "any rule having Effect=Permit
    -- evaluates to Indeterminate" corresponds to indeterminate_p.
    if results.elem Decision'.deny then Decision'.deny else
    if results.elem Decision'.indeterminate_d then Decision'.indeterminate else
    if results.elem Decision'.permit then Decision'.permit else
    if results.elem Decision'.indeterminate_p then Decision'.indeterminate else
    Decision'.not_applicable
  def eval_legacy_ordered_deny_overrides : List Decision' -> Decision' := eval_legacy_deny_overrides

  -- See the comment for `eval_legacy_deny_overrides_rule`.
  def eval_legacy_permit_overrides (results : List Decision') : Decision' :=
    if results.elem Decision'.permit then Decision'.permit else
    if results.elem Decision'.indeterminate_p then Decision'.indeterminate else
    if results.elem Decision'.deny then Decision'.deny else
    if results.elem Decision'.indeterminate_d then Decision'.indeterminate else
    Decision'.not_applicable
  def eval_legacy_ordered_permit_overrides : List Decision' -> Decision' := eval_legacy_permit_overrides
end RuleCombinatorAlgorithm

inductive PolicyCombinatorAlgorithm where
  | deny_overrides                  : PolicyCombinatorAlgorithm
  | ordered_deny_overrides          : PolicyCombinatorAlgorithm
  | permit_overrides                : PolicyCombinatorAlgorithm
  | ordered_permit_overrides        : PolicyCombinatorAlgorithm
  | deny_unless_permit              : PolicyCombinatorAlgorithm
  | permit_unless_deny              : PolicyCombinatorAlgorithm
  | first_applicable                : PolicyCombinatorAlgorithm
  | only_one_applicable             : PolicyCombinatorAlgorithm
  | legacy_deny_overrides           : PolicyCombinatorAlgorithm
  | legacy_ordered_deny_overrides   : PolicyCombinatorAlgorithm
  | legacy_permit_overrides         : PolicyCombinatorAlgorithm
  | legacy_ordered_permit_overrides : PolicyCombinatorAlgorithm

namespace PolicyCombinatorAlgorithm
  def eval_deny_overrides := RuleCombinatorAlgorithm.eval_deny_overrides
  def eval_ordered_deny_overrides := RuleCombinatorAlgorithm.eval_ordered_deny_overrides
  def eval_permit_overrides := RuleCombinatorAlgorithm.eval_permit_overrides
  def eval_ordered_permit_overrides := RuleCombinatorAlgorithm.eval_ordered_permit_overrides
  def eval_deny_unless_permit := RuleCombinatorAlgorithm.eval_deny_unless_permit
  def eval_permit_unless_deny := RuleCombinatorAlgorithm.eval_permit_unless_deny
  def eval_first_applicable := RuleCombinatorAlgorithm.eval_first_applicable

  -- The non-normative part of the specification asserts that "If an error
  -- occurs while evaluating the target or condition of a rule, then the
  -- evaluation SHALL halt, and the policy shall evaluate to "Indeterminate",
  -- with the appropriate error status."
  --
  -- This behavior isn't spelled out in the normative part, because errors are
  -- represented as an Indeterminate.
  def eval_only_one_applicable (results : List Decision') : Decision' :=
    match results.filter (fun d => d != Decision'.not_applicable) with
      | []  => Decision'.not_applicable
      | [a] => a
      | _   => Decision'.indeterminate

  def eval_legacy_deny_overrides (results : List Decision') : Decision' :=
    if results.elem Decision'.deny then Decision'.deny else
    if results.elem Decision'.indeterminate then Decision'.deny else
    if results.elem Decision'.permit then Decision'.permit else
    Decision'.not_applicable
  def eval_legacy_ordered_deny_overrides : List Decision' -> Decision' := eval_legacy_deny_overrides

  -- See the comment for `eval_legacy_deny_overrides`.
  def eval_legacy_permit_overrides (results : List Decision') : Decision' :=
    if results.elem Decision'.permit then Decision'.permit else
    if results.elem Decision'.deny then Decision'.deny else
    if results.elem Decision'.indeterminate then Decision'.indeterminate else
    Decision'.not_applicable
  def eval_legacy_ordered_permit_overrides : List Decision' -> Decision' := eval_legacy_permit_overrides
end PolicyCombinatorAlgorithm

inductive StatusCode
  | ok                : StatusCode
  | missing_attribute : StatusCode
  | syntax_error      : StatusCode
  | processing_error  : StatusCode
deriving BEq, Repr

structure AttributeDesignator where
  category        : String
  identifier      : String
  type            : XmlType
  issuer          : Option String
  must_be_present : Bool
deriving BEq, Repr

namespace AttributeDesignator
  def eval (designator : AttributeDesignator) (context : List Attribute) : Sum Value (List StatusCode) :=
    match designator with
      | AttributeDesignator.mk category identifier type issuer must_be_present =>
        let found :=
          -- A named attribute SHALL match an attribute if the values of
          -- their respective Category, AttributeId, DataType and Issuer
          -- attributes match. The attribute designator’s Category MUST
          -- match, by identifier equality, the Category of the
          -- <Attributes> element in which the attribute is present. The
          -- attribute designator’s AttributeId MUST match, by identifier
          -- equality, the AttributeId of the attribute. The attribute
          -- designator’s DataType MUST match, by identifier equality, the
          -- DataType of the same attribute.
          --
          -- If the Issuer attribute is present in the attribute
          -- designator, then it MUST match, using the
          -- “urn:oasis:names:tc:xacml:1.0:function:string-equal”
          -- function, the Issuer of the same attribute. If the Issuer is
          -- not present in the attribute designator, then the matching of
          -- the attribute to the named attribute SHALL be governed by
          -- AttributeId and DataType attributes alone.
          context.filter (fun (attr : Attribute) =>
                            attr.category == category
                          ∧ attr.identifier == identifier
                          ∧ attr.value.fst == type
                          ∧ (attr.issuer == Option.none ∨ attr.issuer == issuer))
        let found := found.map (fun x => x.value)
        if must_be_present then
          match found with
            | [] => Sum.inr $ [StatusCode.missing_attribute]
            | _ => Sum.inl $ Value.bag (Bag.mk found)
        else Sum.inl $ Value.bag (Bag.mk found)
end AttributeDesignator

def matches? (designator : AttributeDesignator) (attr : Attribute) : Prop :=
  designator.category == attr.category ∧
  designator.identifier == attr.identifier ∧
  designator.type == attr.value.fst ∧
  match (designator.issuer, attr.issuer) with
  | (none, _) => True
  | (some issuer₁, some issuer₂)  => issuer₁ == issuer₂
  | _ => False

def FunctionID : Type := String
deriving BEq, Repr

-- "The <Expression> element is not used directly in a policy. The <Expression>
-- element signifies that an element that extends the ExpressionType and is a
-- member of the <Expression> element substitution group SHALL appear in its
-- place."
--
-- We omit the `<xacml:AttributeSelector>` case because this model of XACML does
-- not include it, and we exclude the `<xacml:VariableReference>` case because
-- we erase variable references in the compiler.

inductive Expression where
  -- Note well that `apply` accepts a list of Values, not a list of Expressions,
  -- as its arguments. The compiler is responsible for ensuring that the
  -- arguments in a function call are fully evaluated.
  --
  -- Lean is quite strict about recursion being bounded, which is a little hard
  -- to prove in our case! Fortunately, we can punt the job of proving that to
  -- the compiler.
  | apply                (function : FunctionID) (args: List Value)      : Expression
  | attribute_designator (inner : AttributeDesignator)                   : Expression
  | attribute_value      (inner : Value)                                 : Expression
  | function             (function : FunctionID)                         : Expression
deriving BEq, Repr

namespace Expression
  def apply_eval (name : FunctionID) (args : List Value) : Option Value :=
    if name == "urn:oasis:names:tc:xacml:1.0:function:rfc822Name-match" then
      match args with
        | [Value.primitive (XmlType.string,     lhs),
           Value.primitive (XmlType.rfc822Name, rhs)] =>
           Value.primitive (lhs == rhs)
        | _ => Value.primitive (#<XmlType.boolean, "Indeterminate">)
    else Option.none

  def eval (expression : Expression) (context : Request) : Option Value :=
    -- The return type of `<Apply>` may be made more specific by type unification.
    --
    -- The evaluation result can be specified to be "Indeterminate"; we encode
    -- this as `Option.none` here for ergonomics, but we do give an instance for
    -- `Coe (Option Value) Value`.
    --
    -- § 7.6 enumerates but does not describe the semantics for:
    --
    -- - <xacml:AttributeValue>
    -- - <xacml:AttributeDesignator>
    -- - <xacml:AttributeSelector>
    -- - <xacml:Apply>
    -- - <xacml:Function>
    -- - <xacml:VariableReference>
    match expression with
      | Expression.apply name args            => apply_eval name args
      | Expression.attribute_designator inner =>
        match inner.eval context with
        | Sum.inl res => res
        | Sum.inr status => Option.none
      | Expression.attribute_value inner      => some inner
      | _                                     => Option.none
end Expression

structure Match where
  function   : Identifier
  designator : AttributeDesignator
  value      : Value
deriving BEq, Repr
def AllOf  : Type := List Match
deriving BEq, Repr
def AnyOf  : Type := List AllOf
deriving BEq, Repr
def Target : Type := List AnyOf
deriving BEq, Repr

namespace Match
  -- The evaluation semantics for a matching element is as follows.
  --
  -- 1. If an operational error were to occur while evaluating the
  --    <AttributeDesignator> or <AttributeSelector> element, then the
  --    result of the entire expression SHALL be "Indeterminate".
  --
  -- 2. If the <AttributeDesignator> or <AttributeSelector> element were
  --    to evaluate to an empty bag, then the result of the expression
  --    SHALL be "False".
  --
  -- 3. Otherwise, the MatchId function SHALL be applied between the
  --    <AttributeValue> and each element of the bag returned from the
  --    <AttributeDesignator> or <AttributeSelector> element.
  --    a. If at least one of those function applications were to evaluate
  --       to "True", then the result of the entire expression SHALL be
  --       "True".
  --    b. Otherwise, if at least one of the function applications results
  --       in "Indeterminate", then the result SHALL be "Indeterminate".
  --    c. Finally, if all function applications evaluate to "False", then
  --       the result of the entire expression SHALL be "False".
  def eval (m : Match) (context : Request) : Option Value :=
    match m with
      | Match.mk fn designator value =>
        match designator.eval context with
          | Sum.inl result =>
            let results := match result with
            -- Otherwise, the MatchId function SHALL be applied between the
            -- <AttributeValue> and each element of the bag returned from the
            -- <AttributeDesignator> or <AttributeSelector> element.
            | (Value.bag (Bag.mk attrs)) =>
              attrs.map fun attr =>
                let args := [value, Value.primitive attr]
                (Expression.apply fn args).eval context
            | (Value.primitive attr) =>
              -- TODO: Prove that this case is impossible.
              let args := [value, Value.primitive attr]
              [(Expression.apply fn args).eval context]

            let results := results.map (fun (x : Option Value) => (x : Value))
            -- If at least one of those function applications were to evaluate to
            -- "True", then the result of the entire expression SHALL be "True".
            if results.elem (Value.primitive (#<XmlType.boolean, "True">)) then
              (Value.primitive (#<XmlType.boolean, "True">))
            -- Otherwise, if at least one of the function applications results in
            -- "Indeterminate", then the result SHALL be "Indeterminate".
            else if results.elem (Value.primitive (#<XmlType.boolean, "Indeterminate">)) then
              (Value.primitive (#<XmlType.boolean, "Indeterminate">))
            -- The `else` arm handles the following cases:
            --
            -- If the <AttributeDesignator> or <AttributeSelector> element were to
            -- evaluate to an empty bag, then the result of the expression SHALL
            -- be "False".
            --
            -- Finally, if all function applications evaluate to "False", then the
            -- result of the entire expression SHALL be "False".
            else
              Value.primitive (#<XmlType.boolean, "False">)
          -- If an operational error were to occur while evaluating the
          -- <AttributeDesignator> or <AttributeSelector> element, then the result
          -- of the entire expression SHALL be "Indeterminate".
          | Sum.inr status => Option.none
end Match

namespace AllOf
  def eval (conj : AllOf) (context : Request) : MatchResult :=
    let result := conj.map (fun x => x.eval context)
    let result := result.map (fun (x : Option Value) => (x : Value))
    if result.all (fun x => x == Value.primitive (XmlType.boolean, "True")) then MatchResult.is_match
    else if result.all (fun x => x != Value.primitive (XmlType.boolean, "False")) ∧
            result.elem (Value.primitive (XmlType.boolean, "Indeterminate"))
         then MatchResult.indeterminate
    else MatchResult.no_match
  end AllOf

namespace AnyOf
  def eval (disj : AnyOf) (context : Request) : MatchResult :=
  match disj with
    | [] => MatchResult.is_match
    | List.cons x xs => match x.eval context with
      | MatchResult.is_match => MatchResult.is_match
      | MatchResult.no_match =>
        let rest := AnyOf.eval xs context
        if rest == MatchResult.is_match then MatchResult.no_match else rest
      | MatchResult.indeterminate =>
        let rest := AnyOf.eval xs context
        if rest == MatchResult.no_match then MatchResult.indeterminate else rest
end AnyOf

namespace Target
  def eval (target : Target) (context : Request) : MatchResult :=
    match target with
      -- An empty target matches any request.
      | [] => MatchResult.is_match
      | xs =>
        let results := xs.map (fun disj => disj.eval context)
        -- Otherwise the target value SHALL be "Match" if all the AnyOf
        -- specified in the target match values in the request context.
        if results.all (fun result => result == MatchResult.is_match) then
          MatchResult.is_match
        -- Otherwise, if any one of the AnyOf specified in the target is “No
        -- Match”, then the target SHALL be “No Match”.
        else if results.any (fun result => result == MatchResult.no_match) then
          MatchResult.no_match
        -- Otherwise, the target SHALL be “Indeterminate”.
        else MatchResult.indeterminate
end Target

structure AttributeAssignment where
  category        : String
  identifier      : String
  issuer          : Option String
deriving BEq, Repr

structure Obligation where
  assignments : List AttributeAssignment
  identifier : String
deriving BEq, Repr

structure Advice where
  assignments : List AttributeAssignment
  identifier : String
deriving BEq, Repr

structure AttributeAssignmentExpression where
  category        : String
  identifier      : String
  issuer          : Option String
  expression      : Expression
deriving BEq, Repr

structure ObligationExpression where
  assignments : List AttributeAssignmentExpression
  identifier : String
  fulfill_on : Decision
deriving BEq, Repr

structure AdviceExpression where
  assignments : List AttributeAssignmentExpression
  identifier : String
  applies_to : Decision
deriving BEq, Repr

structure Rule where
  target      : Target
  condition   : Option Expression
  effect      : EffectType
  obligations : List ObligationExpression
  advice      : List AdviceExpression

namespace Rule
  def eval (rule : Rule) (context : Request) : Decision' :=
    -- The "no target" case is handled within `Target.eval`, returning
    -- `MatchResult.is_match` when the target is empty.
    match rule.target.eval context with
      | MatchResult.is_match =>
        let condition :=
          match rule.condition with
            | some condition =>
              -- The condition value SHALL be "True" if the <Condition> element
              -- evaluates to "True".
              let result := condition.eval context
              if result == some (Value.primitive (#<XmlType.boolean, "True">)) then result
              -- Its value SHALL be "False" if the <Condition> element evaluates to
              -- "False".
              else if result == some (Value.primitive (#<XmlType.boolean, "False">)) then result
              -- The condition value SHALL be "Indeterminate", if the expression
              -- contained in the <Condition> element evaluates to "Indeterminate."
              else Value.primitive (#<XmlType.boolean, "Indeterminate">)
            -- The condition value SHALL be "True" if the <Condition> element is absent.
            | none => Value.primitive (#<XmlType.boolean, "True">)
        match condition with
          | some (Value.primitive (XmlType.boolean, "False")) => Decision'.not_applicable
          | some (Value.primitive (XmlType.boolean, "True")) =>
            match rule.effect with
              | EffectType.permit => Decision'.permit
              | EffectType.deny   => Decision'.deny
          -- | (#<XmlType.boolean, "Indeterminate">) =>
          | _ =>
            if rule.effect == EffectType.permit then
              Decision'.indeterminate_p else
              Decision'.indeterminate_d
      | MatchResult.no_match => Decision'.not_applicable
      | MatchResult.indeterminate =>
        if rule.effect == EffectType.permit then
          Decision'.indeterminate_p else
          Decision'.indeterminate_d
end Rule

structure Policy where
  combinator  : RuleCombinatorAlgorithm
  target      : Target
  rules       : List Rule
  obligations : List ObligationExpression
  advice      : List AdviceExpression

namespace Policy
  def eval (policy : Policy) (context : Request) : Decision' :=
    let results := policy.rules.map (fun rule => rule.eval context)
    let combinator :=
      match policy.combinator with
        | RuleCombinatorAlgorithm.deny_overrides                  => RuleCombinatorAlgorithm.eval_deny_overrides
        | RuleCombinatorAlgorithm.ordered_deny_overrides          => RuleCombinatorAlgorithm.eval_ordered_deny_overrides
        | RuleCombinatorAlgorithm.permit_overrides                => RuleCombinatorAlgorithm.eval_permit_overrides
        | RuleCombinatorAlgorithm.ordered_permit_overrides        => RuleCombinatorAlgorithm.eval_ordered_permit_overrides
        | RuleCombinatorAlgorithm.deny_unless_permit              => RuleCombinatorAlgorithm.eval_deny_unless_permit
        | RuleCombinatorAlgorithm.permit_unless_deny              => RuleCombinatorAlgorithm.eval_permit_unless_deny
        | RuleCombinatorAlgorithm.first_applicable                => RuleCombinatorAlgorithm.eval_first_applicable
        | RuleCombinatorAlgorithm.legacy_deny_overrides           => RuleCombinatorAlgorithm.eval_legacy_deny_overrides
        | RuleCombinatorAlgorithm.legacy_ordered_deny_overrides   => RuleCombinatorAlgorithm.eval_legacy_ordered_deny_overrides
        | RuleCombinatorAlgorithm.legacy_permit_overrides         => RuleCombinatorAlgorithm.eval_legacy_permit_overrides
        | RuleCombinatorAlgorithm.legacy_ordered_permit_overrides => RuleCombinatorAlgorithm.eval_legacy_ordered_permit_overrides
    let decision := combinator results
    match policy.target.eval context with
      | MatchResult.is_match => decision
      | MatchResult.no_match => Decision'.not_applicable
      | MatchResult.indeterminate =>
        match decision with
          | Decision'.not_applicable   => Decision'.not_applicable
          | Decision'.permit           => Decision'.indeterminate_p
          | Decision'.deny             => Decision'.indeterminate_d
          | Decision'.indeterminate    => Decision'.indeterminate_dp
          | Decision'.indeterminate_dp => Decision'.indeterminate_dp
          | Decision'.indeterminate_p  => Decision'.indeterminate_p
          | Decision'.indeterminate_d  => Decision'.indeterminate_d
end Policy

structure PolicySetMetadata where
  combinator  : PolicyCombinatorAlgorithm
  target      : Target
  -- children    : List PolicySetChild
  obligations : List ObligationExpression
  advice      : List AdviceExpression

inductive PolicySetChild where
  | policy_set (metadata : PolicySetMetadata) (xs : List PolicySetChild) : PolicySetChild
  | policy     (inner : Policy)    : PolicySetChild

def PolicySet : Type := PolicySetMetadata × (List PolicySetChild)

namespace PolicySet
  def eval (policyset : PolicySet) (context : Request) : Decision' :=
    let results := policyset.snd.map
      (fun child =>
        match child with
          | PolicySetChild.policy_set ps xs => PolicySet.eval (ps, xs) context
          | PolicySetChild.policy     p  => Policy.eval    p  context)
    let (results : List Decision') := []
    let combinator :=
      match policyset.fst.combinator with
        | PolicyCombinatorAlgorithm.deny_overrides                  => PolicyCombinatorAlgorithm.eval_deny_overrides
        | PolicyCombinatorAlgorithm.ordered_deny_overrides          => PolicyCombinatorAlgorithm.eval_ordered_deny_overrides
        | PolicyCombinatorAlgorithm.permit_overrides                => PolicyCombinatorAlgorithm.eval_permit_overrides
        | PolicyCombinatorAlgorithm.ordered_permit_overrides        => PolicyCombinatorAlgorithm.eval_ordered_permit_overrides
        | PolicyCombinatorAlgorithm.deny_unless_permit              => PolicyCombinatorAlgorithm.eval_deny_unless_permit
        | PolicyCombinatorAlgorithm.permit_unless_deny              => PolicyCombinatorAlgorithm.eval_permit_unless_deny
        | PolicyCombinatorAlgorithm.first_applicable                => PolicyCombinatorAlgorithm.eval_first_applicable
        | PolicyCombinatorAlgorithm.only_one_applicable             => PolicyCombinatorAlgorithm.eval_only_one_applicable
        | PolicyCombinatorAlgorithm.legacy_deny_overrides           => PolicyCombinatorAlgorithm.eval_legacy_deny_overrides
        | PolicyCombinatorAlgorithm.legacy_ordered_deny_overrides   => PolicyCombinatorAlgorithm.eval_legacy_ordered_deny_overrides
        | PolicyCombinatorAlgorithm.legacy_permit_overrides         => PolicyCombinatorAlgorithm.eval_legacy_permit_overrides
        | PolicyCombinatorAlgorithm.legacy_ordered_permit_overrides => PolicyCombinatorAlgorithm.eval_legacy_ordered_permit_overrides
    let decision := combinator results
    match policyset.fst.target.eval context with
      | MatchResult.is_match => decision
      | MatchResult.no_match => Decision'.not_applicable
      | MatchResult.indeterminate =>
        match decision with
          | Decision'.not_applicable   => Decision'.not_applicable
          | Decision'.permit           => Decision'.indeterminate_p
          | Decision'.deny             => Decision'.indeterminate_d
          | Decision'.indeterminate    => Decision'.indeterminate_dp
          | Decision'.indeterminate_dp => Decision'.indeterminate_dp
          | Decision'.indeterminate_p  => Decision'.indeterminate_p
          | Decision'.indeterminate_d  => Decision'.indeterminate_d
end PolicySet

structure ResultAuxiliary where
  status      : Option (List StatusCode)
  obligations : List Obligation
  advice      : List Advice
deriving BEq, Repr

structure MissingAttributeDetail where
  category   : String
  identifier : String
  issuer     : Option String
  value      : Option Value
  type       : XmlType
deriving BEq, Repr

def Result : Type := Decision × (Option ResultAuxiliary)

def is_indeterminate (x : Expression) : Bool :=
  match x with
  | Expression.attribute_value (Value.primitive (XmlType.boolean, "Indeterminate")) => true
  | _ => false

def make_response
  (decision    : Decision)
  (status      : Option (List StatusCode))
  (obligations : List Obligation)
  (advice      : List Advice)
: Decision × ResultAuxiliary :=
  let obligations := obligations.map (fun expr => Obligation.mk expr.assignments expr.identifier)
  let advice      := advice.map      (fun expr => Advice.mk     expr.assignments expr.identifier)
  -- If any of the attribute assignment expressions in an obligation or
  -- advice expression with a matching FulfillOn or AppliesTo attribute
  -- evaluates to “Indeterminate”, then the whole rule, policy, or
  -- policy set SHALL be “Indeterminate”. If the FulfillOn or AppliesTo
  -- attribute does not match the result of the combining algorithm or
  -- the rule evaluation, then any indeterminate in an obligation or
  -- advice expression has no effect.
  -- if obligations.
  let decision :=
    -- if obligations.any
    --      (fun obligation => obligation.assignments.any
    --        (fun assignment => is_indeterminate assignment.expression)) ∨
    --    advice.any
    --      (fun advice => advice.assignments.any
    --        (fun assignment => is_indeterminate assignment.expression))
    -- then
    --   Decision.indeterminate
    -- else
      decision
  (
    decision,
    ResultAuxiliary.mk
      status
      (obligations.map (fun expr => Obligation.mk expr.assignments expr.identifier))
      (advice.map      (fun expr => Advice.mk     expr.assignments expr.identifier))
  )

def combine_response_aux (x y : ResultAuxiliary) : ResultAuxiliary :=
  match (x, y) with
    | (ResultAuxiliary.mk status₁ obligations₁ advice₁,
       ResultAuxiliary.mk status₂ obligations₂ advice₂) =>
      ResultAuxiliary.mk
        status₁
        (obligations₁ ++ obligations₂)
        (advice₁ ++ advice₂)

def Choice : Type := List (Decision × ResultAuxiliary)
deriving BEq, Repr