Proofs that the optimized functions in SymCCOpt.Extractor are equivalent to the unoptimized ones in SymCC.Extractor.

theorem Cedar.Thm.extractOpt?_eqv_extract? {cpsets : List SymCC.CompiledPolicies} {I : SymCC.Interpretation} {εnv : SymCC.SymEnv} : cpsets ≠ [] → (∀ (cpset : SymCC.CompiledPolicies), cpset ∈ cpsets → cpset.εnv = εnv) → (∀ (cpset : SymCC.CompiledPolicies), cpset ∈ cpsets → match cpset with | SymCC.CompiledPolicies.policy cp => ∃ (p : Spec.Policy), ∃ (Γ : Validation.TypeEnv), SymCC.CompiledPolicy.compile p Γ = Except.ok cp | SymCC.CompiledPolicies.pset cpset => ∃ (ps : Spec.Policies), ∃ (Γ : Validation.TypeEnv), SymCC.CompiledPolicySet.compile ps Γ = Except.ok cpset) → SymCC.extractOpt? cpsets I = SymCC.SymEnv.extract? (List.map Spec.Policy.toExpr (List.flatMap SymCC.CompiledPolicies.allPolicies cpsets)) I εnv