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 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 BEq, 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 Obligation where
  assignments : List Attribute
  identifier : String
deriving BEq, Repr

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

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

namespace AttributeAssignmentExpression
  def eval (assignment : AttributeAssignmentExpression) (context : Request) : Option Attribute :=
    match assignment.expression.eval context with
      | some (Value.primitive inner) =>
          Attribute.mk
            assignment.category
            assignment.identifier
            assignment.issuer
            inner
      | _ => none
end AttributeAssignmentExpression

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

namespace ObligationExpression
  def eval (obligation : ObligationExpression) (context : Request) : Option Obligation :=
    let assignments := obligation.assignments.map (fun x => AttributeAssignmentExpression.eval x context)
    if assignments.all Option.isSome then
      Obligation.mk
        (List.filterMap id assignments)
        obligation.identifier
    else none
end ObligationExpression

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

namespace AdviceExpression
  def eval (advice : AdviceExpression) (context : Request) : Option Advice :=
    let assignments := advice.assignments.map (fun x => AttributeAssignmentExpression.eval x context)
    if assignments.all Option.isSome then
      Advice.mk
        (List.filterMap id assignments)
        advice.identifier
    else none
end AdviceExpression

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

structure ResultAuxiliary' where
  status      : Option (List StatusCode)
  obligations : List ObligationExpression
  advice      : List AdviceExpression
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 Result' : Type := Decision' × (Option ResultAuxiliary')

namespace Result'
  def eval (result : Result') (context : Request) : Result :=
    match result.snd with
    | some aux =>
      let advices := aux.advice.map (fun advice => AdviceExpression.eval advice context)
      let obligations := aux.obligations.map (fun x => ObligationExpression.eval x context)
      if advices.any Option.isNone || obligations.any Option.isNone then
         (Decision'.indeterminate, none)
      else
        (
          result.fst,
          ResultAuxiliary.mk
            aux.status
            (List.filterMap id obligations)
            (List.filterMap id advices)
        )
    | none => (result.fst, none)
end Result'

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

namespace Rule
  def eval (rule : Rule) (context : Request) : Result' :=
    let (decision : 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
    let advices :=
      rule.advice.filter
        (fun advice => advice.applies_to == (decision : Decision))
    let obligations :=
      rule.obligations.filter
        (fun obligation => obligation.fulfill_on == (decision : Decision))
    (
      decision,
      ResultAuxiliary'.mk
        none
        obligations
        advices
    )
end Rule

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

namespace Policy
  def eval (policy : Policy) (child_results : List Result') (context : Request) : Result' :=
    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 : Decision') := combinator (List.map Prod.fst child_results)
    let (decision : Decision') :=
      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
    let advices :=
      policy.advice.filter
        (fun advice => advice.applies_to == (decision : Decision))
      ++
      List.join
        (child_results.filterMap
          (fun x => match x.snd with
                      | some y => y.advice
                      | none => none))
    let obligations :=
      policy.obligations.filter
        (fun obligation => obligation.fulfill_on == (decision : Decision))
      ++
      List.join
        (child_results.filterMap
          (fun x => match x.snd with
                      | some y => y.obligations
                      | none => none))
    (
      decision,
      ResultAuxiliary'.mk
        none
        obligations
        advices
    )
end Policy

structure PolicySet where
  combinator  : PolicyCombinatorAlgorithm
  target      : Target
  obligations : List ObligationExpression
  advice      : List AdviceExpression

namespace PolicySet
  def eval (policyset : PolicySet) (child_results : List Result') (context : Request) : Result' :=
    let combinator :=
      match policyset.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 : Decision') := combinator (List.map Prod.fst child_results)
    let (decision : Decision') :=
    match policyset.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
    let advices :=
      policyset.advice.filter
        (fun advice => advice.applies_to == (decision : Decision))
      ++
      List.join
        (child_results.filterMap
          (fun x => match x.snd with
                      | some y => y.advice
                      | none => none))
    let obligations :=
      policyset.obligations.filter
        (fun obligation => obligation.fulfill_on == (decision : Decision))
      ++
      List.join
        (child_results.filterMap
          (fun x => match x.snd with
                      | some y => y.obligations
                      | none => none))
    (
      decision,
      ResultAuxiliary'.mk
        none
        obligations
        advices
    )
end PolicySet

inductive PolicyElement where
  | PolicySet (ps : PolicySet)
  | Policy    (p : Policy)
  | Rule      (r : Rule)

def PolicyElement.eval (context : Request) : PolicyElement -> List Result' -> Result'
  | PolicySet ps, results => ps.eval results context
  | Policy p, results => p.eval results context
  | Rule r, _ => r.eval context

inductive ElementTree where
  | Node (e : PolicyElement) (xs : List ElementTree)

def ElementTree.eval' (context : Request) : ElementTree -> List Result' -> Result'
  | ElementTree.Node e [], results => PolicyElement.eval context e results
  | ElementTree.Node e (x :: xs), results =>
      ElementTree.eval'
        context
        (ElementTree.Node e xs)
        ((ElementTree.eval' context x []) :: results)

def ElementTree.eval (context : Request) (et : ElementTree) : Result' :=
  ElementTree.eval' context et []

-- let results := policy.rules.map (fun rule => rule.eval context)

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