diff options
| -rw-r--r-- | xacml-proofs/lean/Xacml.lean | 102 |
1 files changed, 51 insertions, 51 deletions
diff --git a/xacml-proofs/lean/Xacml.lean b/xacml-proofs/lean/Xacml.lean index 2690134..5a2f536 100644 --- a/xacml-proofs/lean/Xacml.lean +++ b/xacml-proofs/lean/Xacml.lean @@ -322,6 +322,13 @@ namespace PolicyCombinatorAlgorithm 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 @@ -331,7 +338,7 @@ structure AttributeDesignator where deriving BEq, Repr namespace AttributeDesignator - def eval (designator : AttributeDesignator) (context : List Attribute) : Option Value := + 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 := @@ -360,9 +367,9 @@ namespace AttributeDesignator let found := found.map (fun x => x.value) if must_be_present then match found with - | [] => Option.none - | _ => Value.bag (Bag.mk found) - else Value.bag (Bag.mk found) + | [] => 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 := @@ -427,7 +434,10 @@ namespace Expression -- - <xacml:VariableReference> match expression with | Expression.apply name args => apply_eval name args - | Expression.attribute_designator inner => inner.eval context + | 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 @@ -468,46 +478,44 @@ namespace Match def eval (m : Match) (context : Request) : Option Value := match m with | Match.mk fn designator value => - do - let result <- designator.eval context - 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 => + 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 - | (Value.primitive attr) => - -- TODO: Prove that this case is impossible. - let args := [value, Value.primitive attr] - [(Expression.apply fn args).eval context] + [(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". - -- - -- In our case, this is handled by the Option monad, since the assignment - -- to `result` would fail. + 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 @@ -723,14 +731,6 @@ namespace PolicySet | Decision'.indeterminate_d => Decision'.indeterminate_d end PolicySet - -inductive StatusCode - | ok : StatusCode - | missing_attribute : StatusCode - | syntax_error : StatusCode - | processing_error : StatusCode -deriving BEq, Repr - structure ResultAuxiliary where status : Option (List StatusCode) obligations : List Obligation |