proposition: Lemma CompileFindSecond : forall vret vtable vkey fpointer (env: Env QsADTs.ADTValue) ext tenv N k1 (table: FiatWBag N) (key: W) (idx2: Fin.t N) (k2 := (Word.natToWord 32 (projT1 (Fin.to_nat idx2)))) (table':= ( results <- {l : list RawTuple | IndexedEnsembles.EnsembleIndexedListEquivalence (IndexedEnsembles.IndexedEnsemble_Intersection table (fun x0 : RawTuple => ((if Word.weq match MakeWordHeading_allWords idx2 in _ = W return W with | eq_refl => GetAttributeRaw x0 idx2 end key then true else false) && true)%bool = true)) l}; ret (table, results))%comp : Comp (_ * list (FiatWTuple N))), GLabelMap.MapsTo fpointer (Axiomatic WBagOfTuples2ADTSpec.FindSecond) env -> Lifted_MapsTo ext tenv vtable (wrapBag k1 k2 table) -> Lifted_MapsTo ext tenv vkey (wrap key) -> Lifted_not_mapsto_adt ext tenv vret -> NoDuplicates [[[vret; vtable; vkey]]] -> vret ∉ ext -> vtable ∉ ext -> BinNat.N.lt (BinNat.N.of_nat N) (Word.Npow2 32) -> TuplesF.functional (IndexedEnsemble_TupleToListW table) -> {{ tenv }} Call vret fpointer (vtable :: vkey :: nil) {{ [[ table' as retv ]] :: [[ NTSomeBag k1 k2 vtable ->> fst retv as _ ]] :: [[ NTSome vret (H := (@WrapInstance _ _ QS_WrapFiatWTupleList)) ->> snd retv as _ ]] :: DropName vret (DropName vtable tenv) }} ∪ {{ ext }} // env.
proof: Proof. repeat (SameValues_Facade_t_step || facade_cleanup_call || LiftPropertyToTelescope_t || PreconditionSet_t). fiat_t. 5:solve[repeat apply DropName_remove; eauto 1]. 4:solve[simpl; eauto using f_equal, ListWToTuple_Truncated_map_keepEq]. 3:solve[fiat_t]. 2:solve[fiat_t]. apply Fiat_Bedrock_Filters_Equivalence; eassumption. Qed.
imports: CertifiedExtraction.Extraction.QueryStructures.FiatBedrockLemmas CertifiedExtraction.Extraction.QueryStructures.CallRules.Core CallRules.Tuple