diff options
| author | Jakob L. Kreuze | 2023-09-20 18:16:10 -0400 |
|---|---|---|
| committer | Jakob L. Kreuze | 2023-09-20 18:16:10 -0400 |
| commit | 7bd1a920de9ee34139bf40b75f2c812e16b2de45 (patch) | |
| tree | 73dbefd889d8be63f270834f5d5fa6091f859c21 /xacml-proofs/lean | |
| parent | d04e5cb8377384f920ff9d4b689836e1dc99e152 (diff) | |
Rule evaluation
Diffstat (limited to 'xacml-proofs/lean')
| -rw-r--r-- | xacml-proofs/lean/Xacml.lean | 54 |
1 files changed, 36 insertions, 18 deletions
diff --git a/xacml-proofs/lean/Xacml.lean b/xacml-proofs/lean/Xacml.lean index 8aadefd..9950b1a 100644 --- a/xacml-proofs/lean/Xacml.lean +++ b/xacml-proofs/lean/Xacml.lean @@ -453,7 +453,6 @@ structure AdviceExpression where applies_to : Decision deriving BEq, Repr --- n.b. "The <Condition> contains one <Expression> element" structure Rule where target : Target condition : Option Expression @@ -462,23 +461,42 @@ structure Rule where 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 + 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 PolicySet where |