proposition: Lemma CompileNew : forall (v1 v2 v3 o1 o2 o3 vlen vtup vtmp : StringMap.key) (env : GLabelMap.t (FuncSpec QsADTs.ADTValue)) (tenv: Telescope QsADTs.ADTValue) ext (val1 val2 val3: W) (fnew fset : GLabelMap.key), NoDuplicates [[[v1;v2;v3;o1;o2;o3;vtup;vlen;vtmp]]] -> StringMap.MapsTo v1 (wrap (FacadeWrapper := @FacadeWrapper_SCA QsADTs.ADTValue) val1) ext -> StringMap.MapsTo v2 (wrap (FacadeWrapper := @FacadeWrapper_SCA QsADTs.ADTValue) val2) ext -> StringMap.MapsTo v3 (wrap (FacadeWrapper := @FacadeWrapper_SCA QsADTs.ADTValue) val3) ext -> StringMap.MapsTo o1 (wrap (FacadeWrapper := @FacadeWrapper_SCA QsADTs.ADTValue) (Word.natToWord 32 0)) ext -> StringMap.MapsTo o2 (wrap (FacadeWrapper := @FacadeWrapper_SCA QsADTs.ADTValue) (Word.natToWord 32 1)) ext -> StringMap.MapsTo o3 (wrap (FacadeWrapper := @FacadeWrapper_SCA QsADTs.ADTValue) (Word.natToWord 32 2)) ext -> StringMap.MapsTo vlen (wrap (FacadeWrapper := @FacadeWrapper_SCA QsADTs.ADTValue) (Word.natToWord 32 3)) ext -> NotInTelescope vtup tenv -> NotInTelescope vtmp tenv -> vtup ∉ ext -> vtmp ∉ ext -> GLabelMap.MapsTo fnew (Axiomatic WTupleADTSpec.New) env -> GLabelMap.MapsTo fset (Axiomatic WTupleADTSpec.Put) env -> {{ tenv }} (Seq (Call vtup fnew (vlen :: nil)) (Seq (Call vtmp fset (vtup :: o1 :: v1 :: nil)) (Seq (Call vtmp fset (vtup :: o2 :: v2 :: nil)) (Call vtmp fset (vtup :: o3 :: v3 :: nil))))) {{ [[(NTSome (H := WrapInstance (H := FiatWrapper)) vtup) ->> ListWToTuple [[[val1;val2;val3]]] : FiatTuple 3 as _]] :: [[(NTSome (H := @FacadeWrapper_SCA QsADTs.ADTValue) vtmp) ->> (Word.natToWord 32 0) as _]] :: (DropName vtup (DropName vtmp tenv)) }} ∪ {{ ext }} // env.
proof: Proof. unfold ProgOk. repeat repeat match goal with | _ => cleanup | _ => reflexivity | _ => progress unfold WTupleADTSpecParams.FieldType in * | |- Safe _ (Seq _ _) _ => econstructor | [ H: RunsTo _ (Seq _ _) _ _ |- _ ] => inversion' H | _ => eapply SameValues_MapsTo_Ext_State; eassumption | _ => eapply StringMap.add_1; [ congruence ] | _ => eapply StringMap.add_2; [ PreconditionSet_t; congruence | ] | [ |- context[Datatypes.length (Array.upd _ _ _)] ] => rewrite Arrays.upd_length | [ H: RunsTo _ _ _ _ |- _ ] => eapply New_RunsTo_characterization in H; [ | clear H; try eassumption.. ] | [ H: RunsTo _ _ _ _ |- _ ] => eapply Set_RunsTo_characterization in H; [ | clear H; try eassumption.. ] | [ |- Safe _ _ _ ] => eapply New_Safe | [ |- Safe _ _ _ ] => eapply Set_Safe | [ H: StringMap.Equal ?m1 ?m2 |- StringMap.MapsTo _ _ ?m1 ] => rewrite H | [ H: StringMap.Equal ?m1 ?m2 |- not_mapsto_adt _ _ = _ ] => rewrite H | [ H: StringMap.Equal ?m1 ?m2 |- Safe _ _ ?m1 ] => rewrite H | [ H: ?a = _ |- context[?a] ] => rewrite H | [ |- not_mapsto_adt _ _ = true ] => solve [not_mapsto_adt_external_t; facade_eauto] end. repeat StringMap_t. Ltac cleanup_StringMap_head := repeat ((rewrite <- add_remove_comm; [ | PreconditionSet_t; congruence ]) || (rewrite remove_trickle; [ | reflexivity])). apply TelEq_swap. wipe. repeat match goal with | [ H: _ <> _ |- _ ] => clear dependent H end. change QsADTs.SCAZero with (wrap (WrappingType := (Value QsADTs.ADTValue)) (Word.natToWord 32 0)). apply SameValues_Pop_Both; [ apply (eq_ret_compute eq_refl) | ]. cleanup_StringMap_head. replace (Array.upd (Array.upd (Array.upd x (Word.natToWord 32 0) val1) (Word.natToWord 32 1) val2) (Word.natToWord 32 2) val3) with [[[val1; val2; val3]]]. change (ADT (QsADTs.WTuple [[[val1; val2; val3]]])) with (wrap (WrappingType := (Value QsADTs.ADTValue)) (ListWToTuple [[[val1; val2; val3]]])). apply SameValues_Pop_Both; [ apply (eq_ret_compute eq_refl) | ]. cleanup_StringMap_head. repeat apply DropName_remove; try eassumption. do 4 try destruct x as [ | ? x ]; match goal with | [ H: context[Datatypes.length] |- _ ] => simpl in H; try discriminate H end. reflexivity. Qed.
imports: Fiat.Computation.Notations CertifiedExtraction.Extraction.QueryStructures.CallRules.Core