Research proof index

Concrete version of verifyMatchesImplies_is_complete.

Concrete version of verifyMatchesImplies_is_sound.

The verifyMatchesImplies analysis is sound: if the assertions verifyMatchesImplies p₁ p₂ εnv are unsatisfiable for the policies p₁ and p₂ and the strongly well-formed symbolic environment εnv, then if p₁ matches in any strongly well-formed concrete environment env ∈ᵢ εnv, then p₂ also matches.

Concrete version of verifyNeverErrors_is_complete.

Concrete version of verifyNeverErrors_is_sound. NOTE: This theorem and many of the following soundness theorems use env.StronglyWellFormedForPolicy p' in the conclusion rather than env.StronglyWellFormedForPolicy p. One can obtain a weaker version with env.StronglyWellFormedForPolicy p, using the lemma `wellTypedPolicy_preserves_StronglyWellFormed...

The verifyNeverMatches analysis is complete: if the assertions verifyNeverMatches p εnv are satisfiable for the policy p and the strongly well-formed symbolic environment εnv, then there exists a strongly well-formed concrete environment env ∈ᵢ εnv such that the evaluator will return .ok true when applied to p and env.