proposition: Lemma CompileCallFacadeImplementationOfMutation_SCA_Replace: forall `{FacadeWrapper av A} {env} fADT, forall fpointer varg vtmp (arg: W) (target: A) tenv, GLabelMap.MapsTo fpointer (Axiomatic (FacadeImplementationOfMutation_SCA _ fADT)) env -> forall vret ext pSCA, PreconditionSet tenv ext [[[varg; vtmp; vret]]] -> {{ [[ `vret ->> target as _]] :: tenv }} pSCA {{ [[ `vret ->> target as _]] :: [[ `varg ->> arg as _]] :: tenv }} ∪ {{ ext }} // env -> {{ [[ `vret ->> target as _]] :: tenv }} Seq pSCA (Call vtmp fpointer (vret :: varg :: nil)) {{ [[ `vret ->> (fADT arg target) as _]] :: tenv }} ∪ {{ ext }} // env.
proof: Proof. repeat hoare. eauto using CompileCallFacadeImplementationOfMutation_SCA. Qed.
imports: Coq.Lists.List CertifiedExtraction.Extraction.External.Core