diff options
| -rw-r--r-- | xacml-proofs/lean/Xacml.lean | 22 |
1 files changed, 21 insertions, 1 deletions
diff --git a/xacml-proofs/lean/Xacml.lean b/xacml-proofs/lean/Xacml.lean index 8a7a40e..8aadefd 100644 --- a/xacml-proofs/lean/Xacml.lean +++ b/xacml-proofs/lean/Xacml.lean @@ -456,11 +456,31 @@ deriving BEq, Repr -- n.b. "The <Condition> contains one <Expression> element" structure Rule where target : Target - condition : Expression + condition : Option Expression effect : EffectType obligations : List ObligationExpression advice : List AdviceExpression +namespace Rule + def eval (rule : Rule) (context : Request) : MatchResult := + 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">) + sorry +end Rule + structure PolicySet where combinator : CombinatorAlgorithm target : Target |