proposition: Lemma CompileNew_spec : 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) setup (fnew fset : GLabelMap.key), NoDuplicates [[[v1;v2;v3;o1;o2;o3;vtup;vlen;vtmp]]] -> vlen ∉ ext -> NotInTelescope vlen tenv -> o3 ∉ ext -> NotInTelescope o3 tenv -> o2 ∉ ext -> NotInTelescope o2 tenv -> o1 ∉ ext -> NotInTelescope o1 tenv -> v3 ∉ ext -> NotInTelescope v3 tenv -> v2 ∉ ext -> NotInTelescope v2 tenv -> v1 ∉ ext -> NotInTelescope v1 tenv -> NotInTelescope vtup tenv -> NotInTelescope vtmp tenv -> vtup ∉ ext -> vtmp ∉ ext -> GLabelMap.MapsTo (elt:=FuncSpec QsADTs.ADTValue) fnew (Axiomatic WTupleADTSpec.New) env -> GLabelMap.MapsTo (elt:=FuncSpec QsADTs.ADTValue) fset (Axiomatic WTupleADTSpec.Put) env -> {{ tenv }} setup {{ [[`v1 ->> val1 as _]] :: [[`v2 ->> val2 as _]] :: [[`v3 ->> val3 as _]] :: [[`o1 ->> (Word.natToWord 32 0) as _]] :: [[`o2 ->> (Word.natToWord 32 1) as _]] :: [[`o3 ->> (Word.natToWord 32 2) as _]] :: [[`vlen ->> (Word.natToWord 32 3) as _]] :: tenv }} ∪ {{ ext }} // env -> {{ tenv }} (Seq setup (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)))))) {{ [[`vtup ->> ListWToTuple [[[val1;val2;val3]]] : FiatTuple 3 as _]] :: tenv }} ∪ {{ ext }} // env.
proof: Proof. intros. apply ProgOk_Remove_Skip_R. hoare. hoare. PreconditionSet_t. side_conditions_fast. computes_to_inv; subst. apply generalized CompileNew; repeat match goal with | _ => congruence | _ => decide_not_in | _ => decide_mapsto_maybe_instantiate | _ => compile_do_side_conditions end. apply ProgOk_Chomp_Some; try side_conditions_fast. intros. PreconditionSet_t; side_conditions_fast; apply CompileSkip. Qed.
imports: Fiat.Computation.Notations CertifiedExtraction.Extraction.QueryStructures.CallRules.Core