This file contains versions of the functions in SymCC/Verifier.lean that operate on compiled policies (from SymCCOpt/CompiledPolicies.lean). Unlike the unoptimized functions in SymCC/Verifier.lean, the functions in this file do not need to call the symbolic compiler.

def Cedar.SymCC.verifyEvaluateOpt (φ : Term → Term) (p : CompiledPolicy) : Asserts

Returns asserts that are unsatisfiable iff the evaluation of p, represented as a Term of type .option .bool, satisfies φ on all inputs drawn from the εnv that p was compiled for.

See also verifyNeverErrorsOpt.

Equations

• One or more equations did not get rendered due to their size.

def Cedar.SymCC.verifyEvaluatePairOpt (φ : Term → Term → Term) (p₁ p₂ : CompiledPolicy) : Asserts

Returns asserts that are unsatisfiable iff the evaluation of p₁ and p₂, represented as Terms of type .option .bool, satisfy φ on all inputs drawn from the εnv that the policies were compiled for. (Caller guarantees that p₁ and p₂ were compiled for the same εnv.)

See also verifyMatchesImpliesOpt, verifyMatchesEquivalentOpt, and verifyMatchesDisjointOpt.

Equations

• One or more equations did not get rendered due to their size.

def Cedar.SymCC.verifyIsAuthorizedOpt (φ : Term → Term → Term) (ps₁ ps₂ : CompiledPolicySet) : Asserts

Returns asserts that are unsatisfiable iff the authorization decisions produced by ps₁ and ps₂, represented as Terms of type .bool, satisfy φ on all inputs drawn from the εnv that the policysets were compiled for. (Caller guarantees that ps₁ and ps₂ were compiled for the same εnv.)

See also verifyAlwaysAllowsOpt, verifyAlwaysDeniesOpt, verifyImpliesOpt, verifyEquivalentOpt, and verifyDisjointOpt.

Equations

• One or more equations did not get rendered due to their size.

def Cedar.SymCC.verifyNeverErrorsOpt (p : CompiledPolicy) : Asserts

Returns asserts that are unsatisfiable iff p does not error on any input in the εnv it was compiled for. If the asserts are satisfiable, then there is some input in εnv on which p errors.

Equations

• Cedar.SymCC.verifyNeverErrorsOpt p = Cedar.SymCC.verifyEvaluateOpt Cedar.SymCC.Factory.isSome p

def Cedar.SymCC.verifyAlwaysMatchesOpt (p : CompiledPolicy) : Asserts

Returns asserts that are unsatisfiable iff p matches all inputs in the εnv it was compiled for. If the asserts are satisfiable, then there is some input in εnv which p doesn't match.

Equations

• Cedar.SymCC.verifyAlwaysMatchesOpt p = Cedar.SymCC.verifyEvaluateOpt (fun (x : Cedar.SymCC.Term) => Cedar.SymCC.Factory.eq x (⊙Cedar.SymCC.Term.prim (Cedar.SymCC.TermPrim.bool true))) p

def Cedar.SymCC.verifyNeverMatchesOpt (p : CompiledPolicy) : Asserts

Returns asserts that are unsatisfiable iff p matches no inputs in εnv. If the asserts are satisfiable, then there is some input in εnv which p does match.

Equations

• One or more equations did not get rendered due to their size.

def Cedar.SymCC.verifyMatchesEquivalentOpt (p₁ p₂ : CompiledPolicy) : Asserts

Returns asserts that are unsatisfiable iff p₁ and p₂ match exactly the same set of inputs in the εnv they were compiled for. (Caller guarantees that p₁ and p₂ were compiled for the same εnv.) If the asserts are satisfiable, then there is some input in εnv on which p₁ and p₂ have different matching behavior.

Equations

• One or more equations did not get rendered due to their size.

def Cedar.SymCC.verifyMatchesImpliesOpt (p₁ p₂ : CompiledPolicy) : Asserts

Returns asserts that are unsatisfiable iff p₁ matching implies that p₂ matches, for every input in the εnv they were compiled for. (Caller guarantees that p₁ and p₂ were compiled for the same εnv.) If the asserts are satisfiable, then there is some input in εnv that is matched by p₁ but not matched by p₂.

Equations

• One or more equations did not get rendered due to their size.

def Cedar.SymCC.verifyMatchesDisjointOpt (p₁ p₂ : CompiledPolicy) : Asserts

Returns asserts that are unsatisfiable iff there is no input in the εnv they were compiled for that is matched by both p₁ and p₂. (Caller guarantees that p₁ and p₂ were compiled for the same εnv.) If the asserts are satisfiable, then there is some input in εnv that is matched by both p₁ and p₂.

Equations

• One or more equations did not get rendered due to their size.

def Cedar.SymCC.verifyMatchesDisjointOpt.disjoint (t₁ t₂ : Term) : Term

Equations

• Cedar.SymCC.verifyMatchesDisjointOpt.disjoint t₁ t₂ = Cedar.SymCC.Factory.not (Cedar.SymCC.Factory.and t₁ t₂)

def Cedar.SymCC.verifyImpliesOpt (ps₁ ps₂ : CompiledPolicySet) : Asserts

Returns asserts that are unsatisfiable iff the authorization decision of ps₁ implies that of ps₂ for every input in the εnv that the policysets were compiled for. (Caller guarantees that ps₁ and ps₂ were compiled for the same εnv.) In other words, every input allowed by ps₁ is allowed by ps₂.

Equations

• Cedar.SymCC.verifyImpliesOpt ps₁ ps₂ = Cedar.SymCC.verifyIsAuthorizedOpt Cedar.SymCC.Factory.implies ps₁ ps₂

def Cedar.SymCC.verifyAlwaysAllowsOpt (ps : CompiledPolicySet) : Asserts

Returns asserts that are unsatisfiable iff ps allows all inputs in the εnv it was compiled for.

Equations

• Cedar.SymCC.verifyAlwaysAllowsOpt ps = Cedar.SymCC.verifyImpliesOpt (Cedar.SymCC.CompiledPolicySet.allowAll ps.εnv) ps

def Cedar.SymCC.verifyAlwaysDeniesOpt (ps : CompiledPolicySet) : Asserts

Returns asserts that are unsatisfiable iff ps denies all inputs in the εnv it was compiled for.

Equations

• Cedar.SymCC.verifyAlwaysDeniesOpt ps = Cedar.SymCC.verifyImpliesOpt ps (Cedar.SymCC.CompiledPolicySet.denyAll ps.εnv)

def Cedar.SymCC.verifyEquivalentOpt (ps₁ ps₂ : CompiledPolicySet) : Asserts

Returns asserts that are unsatisfiable iff ps₁ and ps₂ produce the same authorization decision on all inputs in the εnv that the policysets were compiled for. (Caller guarantees that ps₁ and ps₂ were compiled for the same εnv.)

Equations

• Cedar.SymCC.verifyEquivalentOpt ps₁ ps₂ = Cedar.SymCC.verifyIsAuthorizedOpt Cedar.SymCC.Factory.eq ps₁ ps₂

def Cedar.SymCC.verifyDisjointOpt (ps₁ ps₂ : CompiledPolicySet) : Asserts

Returns asserts that are unsatisfiable iff there is no input in the εnv that is allowed by both ps₁ and ps₂. (Caller guarantees that ps₁ and ps₂ were compiled for the same εnv.) This checks that the authorization semantics of ps₁ and ps₂ are disjoint. If this query is satisfiable, then there is at least one input in this εnv that is allowed by both ps₁ and ps₂.

Equations

• Cedar.SymCC.verifyDisjointOpt ps₁ ps₂ = Cedar.SymCC.verifyIsAuthorizedOpt Cedar.SymCC.verifyDisjointOpt.disjoint ps₁ ps₂

def Cedar.SymCC.verifyDisjointOpt.disjoint (t₁ t₂ : Term) : Term

Equations

• Cedar.SymCC.verifyDisjointOpt.disjoint t₁ t₂ = Cedar.SymCC.Factory.not (Cedar.SymCC.Factory.and t₁ t₂)