Extracting strongly well-formed counterexamples to verification queries

This file defines the function extractOpt?, which turns interpretations into concrete, strongly well-formed counterexamples to verification queries.

See notes on the unoptimized version, extract? in SymCC/Extractor.lean.

This optimized version is proved equivalent to the unoptimized version in Thm/SymCC/Opt.lean.

def Cedar.SymCC.extractOpt? (cpss : List CompiledPolicies) (I : Interpretation) : Option Spec.Env

Optimized version of extract? in SymCC/Extractor.lean.

Caller guarantees that all of the CompiledPolicys and/or CompiledPolicySets were compiled for the same εnv.

Equations

• One or more equations did not get rendered due to their size.
• Cedar.SymCC.extractOpt? [] I = none