proposition: Lemma CompileGet_spec: 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), PreconditionSet tenv ext [[[vtup; vret; vpos]]] -> vret ∉ ext -> vtup ∉ ext -> NotInTelescope vret tenv -> BinNat.N.lt (BinNat.N.of_nat N) (Word.Npow2 32) -> GLabelMap.MapsTo fpointer (Axiomatic WTupleADTSpec.Get) env -> {{ [[ `vtup ->> tup as _ ]] :: tenv }} (Seq (Assign vpos (Const (Word.natToWord 32 (proj1_sig (Fin.to_nat idx))))) (Call vret fpointer (vtup :: vpos :: nil))) {{ [[ `vtup ->> tup as _]] :: [[(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 _]] :: tenv }} ∪ {{ ext }} // env.
proof: Proof. intros. hoare. apply CompileConstant; try compile_do_side_conditions. apply CompileDeallocW_discretely; try compile_do_side_conditions. apply ProgOk_Chomp_Some; try compile_do_side_conditions; intros. apply ProgOk_Chomp_Some; try compile_do_side_conditions; intros. remember (match CompileGet_helper idx in (_ = W) return (Vector.nth (AttrList (MakeWordHeading N)) idx -> W) with | eq_refl => fun t : Vector.nth (AttrList (MakeWordHeading N)) idx => t end (ilist2.ith2 tup idx)). setoid_replace tenv with (DropName vret tenv) using relation (@TelStrongEq QsADTs.ADTValue) at 2. computes_to_inv; subst; apply CompileGet; repeat (PreconditionSet_t || compile_do_side_conditions || decide_not_in || Lifted_t). apply Lifted_MapsTo_Ext; decide_mapsto_maybe_instantiate. apply Lifted_MapsTo_Ext; decide_mapsto_maybe_instantiate. symmetry; apply DropName_NotInTelescope; assumption. Qed.
imports: Fiat.Computation.Notations CertifiedExtraction.Extraction.QueryStructures.CallRules.Core