proposition: Lemma CompileFindSecond_spec : 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 -> StringMap.MapsTo vkey (wrap key) ext -> PreconditionSet tenv ext [[[vret; vtable]]] -> vret <> vkey -> vtable <> vkey -> BinNat.N.lt (BinNat.N.of_nat N) (Word.Npow2 32) -> TuplesF.functional (IndexedEnsemble_TupleToListW table) -> {{ [[ NTSomeBag k1 k2 vtable ->> table as _]] :: 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 _ ]] :: tenv }} ∪ {{ ext }} // env.
proof: Proof. intros. apply generalized CompileFindSecond; repeat (compile_do_side_conditions || Lifted_t || PreconditionSet_t). setoid_rewrite (DropName_NotInTelescope _ _ H12). rewrite DropName_Cons_None. setoid_rewrite (DropName_NotInTelescope _ _ H10). decide_TelEq_instantiate. Qed.
imports: CertifiedExtraction.Extraction.QueryStructures.FiatBedrockLemmas CertifiedExtraction.Extraction.QueryStructures.CallRules.Core CallRules.Tuple