proposition: Lemma CompileGet: forall (vret vtup vpos : StringMap.key) (env : GLabelMap.t (FuncSpec QsADTs.ADTValue)) (tenv: Telescope QsADTs.ADTValue) ext N (fpointer : GLabelMap.key) (tup : FiatTuple N) (idx: Fin.t N), vtup <> vret -> vret ∉ ext -> Lifted_MapsTo ext tenv vtup (wrap (FacadeWrapper := WrapInstance (H := (FiatWrapper))) tup) -> Lifted_MapsTo ext tenv vpos (wrap (Word.natToWord 32 (proj1_sig (Fin.to_nat idx)))) -> Lifted_not_mapsto_adt ext tenv vret -> BinNat.N.lt (BinNat.N.of_nat N) (Word.Npow2 32) -> GLabelMap.MapsTo fpointer (Axiomatic WTupleADTSpec.Get) env -> {{ tenv }} Call vret fpointer (vtup :: vpos :: nil) {{ [[(NTSome (H := FacadeWrapper_SCA) vret) ->> (match CompileGet_helper idx in _ = W return _ -> W with | eq_refl => fun t => t end) (ilist2.ith2 tup idx) as _]] :: (DropName vret tenv) }} ∪ {{ ext }} // env.
proof: Proof. repeat (SameValues_Facade_t_step || facade_cleanup_call || LiftPropertyToTelescope_t || PreconditionSet_t). facade_eauto. rewrite Word.wordToNat_natToWord_idempotent by (apply (CompileGet_goodSize_helper idx); assumption). rewrite CompileGet_helper'' by congruence; reflexivity. rewrite <- remove_add_comm by congruence. setoid_rewrite <- add_redundant_cancel; try eassumption. repeat apply DropName_remove; eauto 1. Qed.
imports: Fiat.Computation.Notations CertifiedExtraction.Extraction.QueryStructures.CallRules.Core