Library Malfunction.Interpreter
From Stdlib Require Import ssreflect ZArith Array.PArray List Floats Lia.
Import ListNotations.
Require Import Malfunction.Malfunction Malfunction.SemanticsSpec Malfunction.utils_array.
From MetaRocq.Utils Require Import bytestring.
Open Scope bs.
From Stdlib Require Import Uint63.
Class Heap `{Pointer} := {
heapGen : ∀ (value : Type), Type;
fresh : ∀ {value : Type}, heapGen value → pointer × heapGen value;
deref : ∀ {value : Type}, heapGen value → pointer → array value;
update : ∀ {value : Type}, heapGen value → pointer → array value → heapGen value
}.
Definition CanonicalHeap : @Heap CanonicalPointer :=
{| heapGen := fun value ⇒ (int × (int → array value))%type;
fresh := fun _ '(max_ptr , h) ⇒ let ptr := Int63.add max_ptr (int_of_nat 1) : @pointer CanonicalPointer in (ptr ,(ptr, h));
deref := fun _ '(_,h) ptr ⇒ h ptr;
update := fun _ '(max_ptr , h) ptr arr ⇒ (max_ptr , fun ptr' ⇒ if Int63.eqb ptr ptr' then arr else h ptr) |}.
Definition heap `{Heap} := heapGen value.
Definition is_not_evaluated `{Pointer} : value → bool :=
fun v ⇒ match v with | not_evaluated ⇒ true | _ ⇒ false end.
Definition find_match `{Heap} (interpret : heap → @Ident.Map.t value → @Ident.Map.t value → t → heap × value)
:= fun h iglobals ilocals scr ⇒ fix find_match x := match x with
| (cases, e) :: rest ⇒
if List.existsb (cond scr) cases then
interpret h iglobals ilocals e
else
find_match rest
| [] ⇒ (h, fail "no case matches") end.
#[bypass_check(guard)]
Fixpoint interpret `{Pointer} `{Heap} (h : heap)
(globals : @Ident.Map.t value)
(locals : @Ident.Map.t value)
(x : t) {struct x} : heap × value :=
match x with
| Mvar v ⇒ (h, Ident.Map.find v locals)
| Mlambda (xs, e) ⇒
(h, match xs with
| [ ] ⇒ fail "assert false"
| x :: xs ⇒
let (x , e) := match xs with
| [] ⇒ (x , e)
| _ :: _ ⇒ (x , Mlambda (xs, e)) end
in Func (locals, x , e)
end)
| Mapply (f_, vs) ⇒
List.fold_left (fun f v ⇒ match f with
| (h , Func (locals', x, e)) ⇒
let (h' , v') := interpret h globals locals v
in interpret h' globals (Ident.Map.add x v' locals') e
| (h , (RClos (locals', self, mfix , n))) ⇒
let (h' , v') := interpret h globals locals v in
match nth n mfix Bad_recursive_value with
| RFunc (y , e) ⇒
interpret h' globals (Ident.Map.add y v' (add_self self mfix locals')) e
| _ ⇒ (h', fail "not a function") end
| (h , _) ⇒ (h , fail ("not a function: " ++ " evaluated to: ")) end) vs
(interpret h globals locals f_)
| Mlet (bindings, body) ⇒
let bind :=
fix bind (h : heap) (locals : @Ident.Map.t value) (bindings : list binding) {struct bindings}: heap × value :=
match bindings with
| [] ⇒ interpret h globals locals body
| Unnamed e :: bindings ⇒
let (h' , _) := interpret h globals locals e in bind h' locals bindings
| Named (x, e) :: bindings ⇒
let (h' ,v) := interpret h globals locals e in
bind h' (Ident.Map.add x v (locals)) bindings
| Recursive recs :: bindings ⇒
let self := map fst recs in
let rfunc := RFunc_build (map snd recs) in
bind h (add_self self rfunc locals) bindings
end
in
bind h locals bindings
| Mnum (numconst_Int n) ⇒ (h , value_Int (Int, Int63.to_Z n))
| Mnum (numconst_Bigint n) ⇒ (h , value_Int (Bigint, n))
| Mnum (numconst_Float64 f) ⇒ (h, Float f)
| Mstring s ⇒
let (ptr,h') := fresh h in
let str := Array_init (Int63.of_Z (Z.of_nat (String.length s)))
(fun i ⇒ value_Int (Int, (Z.of_nat (Byte.to_nat (option_def (Ascii.byte_of_ascii Ascii.Space) (get (Z.to_nat (Int63.to_Z i)) s)))))) in
(update h' ptr str , Vec (Bytevec, ptr))
| Mglobal v ⇒ (h , Ident.Map.find v globals)
| Mswitch (scr, cases) ⇒
let (h', scr') := interpret h globals locals scr in
find_match interpret h' globals locals scr' cases
| Mnumop1 (op, embed_inttype ty, e) ⇒
let (h',v) := interpret h globals locals e in
let n := as_ty ty v in
(h', truncate ty (match op with Malfunction.Neg ⇒ Z.mul (-1) n | Not ⇒ Z.lnot n end))
| Mnumop2 (op, embed_inttype ty, e1, e2) ⇒
let (h1 , e1) := interpret h globals locals e1 in
let (h2 , e2) := interpret h1 globals locals e2 in
(h2, match op with
| embed_binary_arith_op op ⇒
let f := match op with
| Add ⇒ Z.add | Sub ⇒ Z.sub
| Mul ⇒ Z.mul | Div ⇒ Z.div | Mod ⇒ Z.rem
end in
truncate ty (f (as_ty ty e1) (as_ty ty e2))
| embed_binary_bitwise_op op ⇒
let n := as_ty ty e1 in
let c := as_ty Int e2 in
truncate ty (match op with
| And ⇒ Z.land (as_ty ty e1) (as_ty ty e2)
| Or ⇒ Z.lor (as_ty ty e1) (as_ty ty e2)
| Xor ⇒ Z.lxor (as_ty ty e1) (as_ty ty e2)
| Lsl ⇒ Z.shiftl n c
| Asr ⇒ Z.shiftr n c
| Lsr ⇒
let n := match ty with
| Bigint ⇒ n
| _op ⇒
let w := bitwidth ty in
Z.land n (Z.sub (Z.shiftl (Z.of_nat 1) w) (Z.of_nat 1)) end in
Z.shiftr n c end)
| embed_binary_comparison op ⇒
let cmp := Z.compare (as_ty ty e1) (as_ty ty e2) in
let res := match op with
| Lt ⇒ comparison_eqb cmp Datatypes.Lt
| Gt ⇒ comparison_eqb cmp Datatypes.Gt
| Lte ⇒ negb (comparison_eqb cmp Datatypes.Gt)
| Gte ⇒ negb (comparison_eqb cmp Datatypes.Lt)
| Eq ⇒ comparison_eqb cmp Datatypes.Eq
end in
value_Int (Int, if res then 1%Z else 0%Z)
end)
| Mnumop1 (Malfunction.Neg, Float64, e) ⇒
let (h' , v) := interpret h globals locals e in (h' , Float (- as_float v))
| Mnumop1 (Not, Float64, _)
| Mnumop2 (embed_binary_bitwise_op _, Float64, _, _) ⇒
(h , fail "invalid bitwise float operation")
| Mnumop2 (embed_binary_arith_op op, Float64, e1, e2) ⇒
let (h1,e1') := interpret h globals locals e1 in
let (h2,e2') := interpret h1 globals locals e2 in
let e1 := as_float e1' in
let e2 := as_float e2' in
(h2, Float (match op with
| Add ⇒ e1 + e2
| Sub ⇒ e1 - e2
| Mul ⇒ e1 × e2
| Div ⇒ e1 / e2
| Mod ⇒ fail_float "mod on floats not supported" end))
| Mnumop2 (embed_binary_comparison op, Float64, e1, e2) ⇒
let (h1,e1') := interpret h globals locals e1 in
let (h2,e2') := interpret h1 globals locals e2 in
let e1 := as_float e1' in
let e2 := as_float e2' in
let res := match op with
| Lt ⇒ PrimFloat.ltb e1 e2
| Gt ⇒ PrimFloat.ltb e2 e2
| Lte ⇒ PrimFloat.leb e1 e2
| Gte ⇒ PrimFloat.leb e2 e1
| Eq ⇒ PrimFloat.eqb e1 e2
end in
(h2, value_Int (Int, if res then 1%Z else 0%Z))
| Mconvert (embed_inttype src, embed_inttype dst, e) ⇒
let (h',v) := interpret h globals locals e in
(h', truncate dst (as_ty src v))
| Mconvert (embed_inttype src, Float64, e) ⇒
let (h',v) := interpret h globals locals e in
(h',Float (PrimFloat.of_uint63 (Int63.of_Z (as_ty src v))))
| Mconvert (Float64, Float64, e) ⇒
let (h',v) := interpret h globals locals e in
(h',Float (as_float v))
| Mvecnew (ty, len, def) ⇒
let (h1,len') := interpret h globals locals len in
let (h2,def') := interpret h1 globals locals def in
let (ptr,h3) := fresh h2 in
match ty, len' , def' with
| Array, value_Int (Int, len), v ⇒
(update h3 ptr (PArray.make (Int63.of_Z len) v), Vec (Array, ptr))
| Bytevec, value_Int (Int, len), (value_Int (Int, k)) as v ⇒
if Z.leb 0%Z k && Z.ltb k 256 then
(update h3 ptr (PArray.make (Int63.of_Z len) v), Vec (Bytevec, ptr))
else
(h3,fail "bad vector creation")
| _, _, _ ⇒ (h2,fail "bad vector creation")
end
| Mvecget (ty, vec, idx) ⇒
let (h1,vec') := interpret h globals locals vec in
let (h2,idx') := interpret h1 globals locals idx in
(h2, match vec', idx' with
| Vec (ty', ptr), value_Int (Int,i) ⇒
if vector_type_eqb ty ty' then
if Z.leb 0 i && Z.ltb i (Int63.to_Z (PArray.length (deref h ptr))) then
PArray.get (deref h ptr) (Int63.of_Z i)
else
fail "index out of bounds: %d"
else
fail "wrong vector type"
| _, _ ⇒ fail "wrong vector type"
end)
| Mvecset (ty, vec, idx, e) ⇒
let (h1,vec') := interpret h globals locals vec in
let (h2,idx') := interpret h1 globals locals idx in
let (h3,v) := interpret h2 globals locals e in
match vec', idx', v with
| Vec (ty', ptr), value_Int (Int, i), v ⇒
if vector_type_eqb ty ty' then
let i' := Int63.of_Z i in
if Z.leb 0 i && Z.ltb i (Int63.to_Z (PArray.length (deref h ptr))) then
match ty, v with
| Array, _ ⇒ (update h3 ptr (PArray.set (deref h ptr) i' v), value_Int (Int, 0%Z))
| Bytevec, value_Int (Int, val) ⇒
if (Z.leb 0 val) && (Z.ltb val 256)
then
(update h3 ptr (PArray.set (deref h ptr) i' v), value_Int (Int, 0%Z))
else (h3, fail "not a byte")
| Bytevec, _ ⇒ (h3, fail "not a byte")
end
else (h3, fail "index out of bounds: %d")
else (h3, fail "wrong vector type")
| _ , _ , _ ⇒ (h3, fail "wrong vector type")
end
| Mveclen (ty, vec) ⇒
let (h',vec') := interpret h globals locals vec in
(h', match vec' with
| Vec (ty', ptr) ⇒
if vector_type_eqb ty ty' then value_Int (Int, Int63.to_Z (PArray.length (deref h ptr)))
else fail "wrong vector type"
| _ ⇒ fail "wrong vector type"
end)
| Mblock (tag, vals) ⇒
let (h',vals') := map_acc (fun h e ⇒ interpret h globals locals e) h vals in
(h', if (int_of_nat (Datatypes.length vals) ≤? max_length)%uint63
then Block (tag, vals')
else fail "vals is a too big array")
| Mfield (idx, b) ⇒
let (h',b') := interpret h globals locals b in
(h', match b' with
| Block (_, vals) ⇒ nth (int_to_nat idx) vals (fail "")
| _ ⇒ fail "not a block"
end)
| Mlazy e ⇒
let (ptr,h') := fresh h in
let init := PArray.make (Int63.of_Z 2) not_evaluated in
let arr := PArray.set init (Int63.of_Z 1) (Lazy (locals , e)) in
(update h' ptr arr, Thunk ptr)
| Mforce e ⇒
let (h',v) := interpret h globals locals e in
match v with
| Thunk ptr ⇒ let arr := deref h' ptr in
let lazy := PArray.get arr (Int63.of_Z 0) in
if is_not_evaluated lazy
then
match PArray.get arr (Int63.of_Z 1) with
| Lazy (locals , e) ⇒
let (h'' , v') := interpret h' globals locals e in
(update h'' ptr (PArray.set arr (Int63.of_Z 0) v'), v')
| _ ⇒ (h', fail "not a lazy value")
end
else (h', lazy)
| _ ⇒ (h', fail "not a lazy value")
end
| _ ⇒ (h , fail "assert todo")
end.
Class CompatiblePtr (P P' : Pointer) :=
{ R_ptr : P.(pointer) → P'.(pointer) → Prop }.
Unset Elimination Schemes.
Inductive vrel {P P' : Pointer} {H : CompatiblePtr P P'} : @value P → @value P' → Prop :=
| vBlock : ∀ tag vals vals', Forall2 vrel vals vals' →
vrel (Block (tag, vals)) (Block (tag, vals'))
| vVec : ∀ ty ptr ptr', R_ptr ptr ptr' → vrel (Vec (ty, ptr)) (Vec (ty, ptr'))
| vFunc : ∀ x locals locals' e,
(∀ x, vrel (locals x) (locals' x)) →
vrel (Func (locals,x,e)) (Func (locals',x,e))
| vRClos : ∀ self mfix mfix' n locals locals',
(∀ x, vrel (locals x) (locals' x)) →
Forall2 (fun a b ⇒
(∀ y e, (a = RFunc (y, e)) ↔ (b = RFunc (y, e))) ∧
(∀ ptr ptr', a = RThunk ptr → b = RThunk ptr' → R_ptr ptr ptr') ∧
(a = Bad_recursive_value ↔ b = Bad_recursive_value)) mfix mfix' →
vrel (RClos (locals,self,mfix,n)) (RClos (locals',self,mfix',n))
| vInt : ∀ ty i ,
vrel (value_Int (ty, i)) (value_Int (ty, i))
| vFloat : ∀ f,
vrel (Float f) (Float f)
| vThunk : ∀ ptr ptr', R_ptr ptr ptr' →
vrel (Thunk ptr) (Thunk ptr')
| vLazy : ∀ e locals locals',
(∀ x, vrel (locals x) (locals' x)) →
vrel (Lazy (locals, e)) (Lazy (locals' , e))
| vFail : ∀ s, vrel (fail s) (fail s)
| vNot_evaluated : vrel not_evaluated not_evaluated.
Lemma vrel_ind : ∀ (P P' : Pointer) (H : CompatiblePtr P P')
(P0 : value → value → Prop),
(∀ (tag : Malfunction.int) (vals vals' : list value),
Forall2 vrel vals vals' →
Forall2 P0 vals vals' →
P0 (Block (tag, vals)) (Block (tag, vals'))) →
(∀ (ty : vector_type) (ptr ptr' : pointer),
R_ptr ptr ptr' → P0 (Vec (ty, ptr)) (Vec (ty, ptr'))) →
(∀ (x : Ident.t) (locals locals' : Ident.t → value) (e : t),
(∀ x0 : Ident.t, vrel (locals x0) (locals' x0)) →
(∀ x0 : Ident.t, P0 (locals x0) (locals' x0)) →
P0 (Func (locals, x, e)) (Func (locals', x, e))) →
(∀ (self : list Ident.t) (mfix mfix' : list rec_value)
(n : nat) (locals locals' : Ident.t → value),
(∀ x : Ident.t, vrel (locals x) (locals' x)) →
(∀ x : Ident.t, P0 (locals x) (locals' x)) →
Forall2
(fun a b : rec_value ⇒
(∀ y e, a = RFunc (y, e) ↔ b = RFunc (y, e)) ∧
(∀ ptr ptr', a = RThunk ptr → b = RThunk ptr' → R_ptr ptr ptr') ∧
(a = Bad_recursive_value ↔ b = Bad_recursive_value)) mfix mfix' →
P0 (RClos (locals, self, mfix, n)) (RClos (locals', self, mfix', n))) →
(∀ (ty : inttype) (i : Z),
P0 (value_Int (ty, i)) (value_Int (ty, i))) →
(∀ f4 : float, P0 (Float f4) (Float f4)) →
(∀ ptr ptr' : pointer,
R_ptr ptr ptr' → P0 (Thunk ptr) (Thunk ptr')) →
(∀ (e : t) (locals locals' : Ident.t → value),
(∀ x : Ident.t, vrel (locals x) (locals' x)) →
(∀ x : Ident.t, P0 (locals x) (locals' x)) →
P0 (Lazy (locals, e)) (Lazy (locals', e))) →
(∀ s : string, P0 (fail s) (fail s)) →
P0 not_evaluated not_evaluated →
∀ v v0 : value, vrel v v0 → P0 v v0.
Proof.
intros.
revert v v0 H10.
fix f 3. intros v V0 [| | | | | | | | | ].
2-10:eauto.
- eapply H0; eauto. induction H10; try econstructor; eauto.
Qed.
Set Elimination Schemes.
Definition CompatiblePtr_sym {P P' : Pointer} `{@CompatiblePtr P P'} : @CompatiblePtr P' P
:= {| R_ptr := fun p' p ⇒ R_ptr p p' |}.
Lemma vrel_sym {P P' : Pointer} `{@CompatiblePtr P P'} v v' :
vrel v v' → @vrel _ _ CompatiblePtr_sym v' v.
Proof.
induction 1; econstructor; eauto.
- induction H1; econstructor; try inversion H0; eauto.
- clear - H2; induction H2; econstructor; eauto. clear -H0.
destruct H0 as [? [? [? ?]]]. repeat split; eauto.
+ eapply H0.
+ eapply H0.
+ intros. eapply H1; eauto.
Qed.
Definition vrel_locals `{CompatiblePtr}
: Ident.Map.t → Ident.Map.t → Prop := fun locals ilocals ⇒ ∀ x, vrel (locals x) (ilocals x).
Class CompatibleHeap {P P' : Pointer} {H : CompatiblePtr P P'}
{HP : @SemanticsSpec.Heap P} {HP' : @Heap P'} :=
{ R_heap : SemanticsSpec.heap → heap → Prop;
fresh_compat : ∀ h ptr h' ih,
R_heap h ih → SemanticsSpec.fresh h ptr h' →
let (iptr,ih') := fresh ih in R_ptr ptr iptr ∧ R_heap h' ih';
update_compat : ∀ default h ih ptr ptr' h' v v',
R_heap h ih → SemanticsSpec.update h ptr v h' →
R_ptr ptr ptr' → Forall2Array vrel v v' default →
let ih' := Interpreter.update ih ptr' v' in R_heap h' ih';
deref_compat : ∀ default h ih ptr ptr' vals,
R_heap h ih → SemanticsSpec.deref h ptr vals →
R_ptr ptr ptr' →
let vals' := Interpreter.deref ih ptr' in
Forall2Array vrel vals vals' default
}.
Lemma cond_correct `{CompatiblePtr}
scr scr' x : vrel scr scr' →
cond scr x = cond scr' x.
Proof.
now destruct x as [ | | [] ]; destruct 1.
Qed.
Lemma existsb_ext {A} (f g : A → bool) l :
(∀ x, f x = g x) →
existsb f l = existsb g l.
Proof.
intros H; induction l; cbn; congruence.
Qed.
Lemma find_match_correct `{CompatibleHeap}
scr scr' cases e h iglobals ilocals :
vrel scr scr' →
SemanticsSpec.find_match scr cases = Some e →
Interpreter.find_match Interpreter.interpret h iglobals ilocals scr' cases = interpret h iglobals ilocals e.
Proof.
induction cases as [ | a cases IHcases ]; cbn [SemanticsSpec.find_match]; intros rel Eq.
- inversion Eq.
- destruct a.
cbn [find_match].
destruct existsb eqn:E.
× inversion Eq. erewrite existsb_ext.
2:{ intros. symmetry. eapply cond_correct. eauto. }
now rewrite E.
× erewrite existsb_ext.
2:{ intros. symmetry. eapply cond_correct. eauto. }
rewrite E. eauto.
Qed.
Lemma vrel_add `{CompatiblePtr} x v iv locals ilocals : vrel v iv → vrel_locals locals ilocals →
vrel_locals (Ident.Map.add x v locals) (Ident.Map.add x iv ilocals).
Proof.
intros Hv Hlocals nm. unfold Ident.Map.add. now destruct Ident.eqb.
Qed.
Lemma isNotEvaluated_vrel `{CompatibleHeap} v v' b :
vrel v v' → isNotEvaluated v = b ↔ is_not_evaluated v' = b.
Proof.
now destruct 1.
Qed.
Ltac fail_case IHeval Hloc Hheap Heq :=
let Hv := fresh "iv1" in cbn; specialize (IHeval _ _ Hloc Hheap); destruct interpret as [? ?];
destruct IHeval as [? Hv]; destruct Hv; inversion Heq; split;eauto; econstructor.
Lemma vrel_locals_add_self `{CompatiblePtr} locals' locals'0 mfix mfix' self :
(∀ x : Ident.t, vrel (locals' x) (locals'0 x)) →
Forall2 (fun a b ⇒
(∀ y e, (a = RFunc (y, e)) ↔ (b = RFunc (y, e))) ∧
(∀ ptr ptr', a = RThunk ptr → b = RThunk ptr' → R_ptr ptr ptr') ∧
(a = Bad_recursive_value ↔ b = Bad_recursive_value)) mfix mfix' →
vrel_locals (SemanticsSpec.add_self self mfix locals') (add_self self mfix' locals'0).
Proof.
intros Hloc ?.
unfold add_self, SemanticsSpec.add_self.
unfold add_recs, SemanticsSpec.add_recs. unfold List.mapi.
generalize 0. generalize self at 1 3.
pose proof (Hcopy := Hloc). revert Hcopy.
generalize locals' at 1 3. generalize locals'0 at 1 3.
revert locals' locals'0 Hloc.
induction self; eauto; cbn; intros.
intro. unfold Ident.Map.add. case_eq (Ident.eqb x a); intro; eauto.
- econstructor; eauto.
- apply IHself; eauto.
Qed.
Lemma as_ty_vrel `{CompatiblePtr} ty v v' :
vrel v v' → as_ty ty v = as_ty ty v'.
Proof.
inversion 1; destruct ty; cbn; try reflexivity.
Defined.
Lemma as_float_vrel `{CompatiblePtr} v v' :
vrel v v' → as_float v = as_float v'.
Proof.
inversion 1; cbn; try reflexivity.
Defined.
Lemma truncate_vrel `{CompatiblePtr} ty z :
vrel (SemanticsSpec.truncate ty z) (truncate ty z).
destruct ty; econstructor.
Qed.
Lemma eval_correct `{CompatibleHeap}
globals locals ilocals iglobals e h h' ih v :
(∀ nm val, In (nm, val) globals → vrel val (iglobals nm)) →
vrel_locals locals ilocals →
R_heap h ih →
eval _ _ globals locals h e h' v →
let (ih',iv) := interpret ih iglobals ilocals e in R_heap h' ih' ∧ vrel v iv.
Proof.
rename H into _CPtr; rename H0 into _CHeap.
intros Hglob Hloc Hheap.
induction 1 as [ locals h x e
| locals h x ids e H
| locals h1 h2 h3 h4 x locals' e e2 v2 e1 v H IHeval1 H0 IHeval2 H1 IHeval3
| locals h1 h2 h3 h4 mfix n y e locals' self e2 v2 e1 v H IHeval1 H0 IHeval2 Hnth H1 IHeval3
| locals h h' e2 e v Heval IHeval Heq
| locals h h' e3 e2 e1 v vals tag IHeval
|
| | | |
|
|
| locals h h' idx b vals tag H IHeval | | | | | |
| | | | | | | | | | | | | | | | | | | ]
in ih, Hheap, ilocals, Hloc |- ×.
- split; eauto. econstructor; eauto.
- split; eauto.
destruct ids as [ | t ids ]; cbn in H. 1:inversion H. clear H.
econstructor; eauto.
- cbn; specialize (IHeval1 _ _ Hloc Hheap). destruct interpret as [ih1 iv1]; destruct IHeval1 as [Hheap1 Hiv1].
specialize (IHeval2 _ _ Hloc Hheap1). destruct interpret as [ih2 iv2]; destruct IHeval2 as [Hheap2 Hiv2].
inversion Hiv1 ; subst.
specialize (IHeval3 (Ident.Map.add x iv2 locals'0) ih2).
destruct interpret as [ih3 iv3]; cbn in ×.
apply IHeval3; eauto. now apply vrel_add.
- cbn; specialize (IHeval1 _ _ Hloc Hheap). destruct interpret as [ih1 iv1]; destruct IHeval1 as [Hheap1 Hiv1].
specialize (IHeval2 _ _ Hloc Hheap1). destruct interpret as [ih2 iv2]; destruct IHeval2 as [Hheap2 Hiv2].
inversion Hiv1 ; subst. clear -H8 Hiv2 H7 Hheap2 Hnth IHeval3.
pose proof (Hmfix := H8).
eapply (All_Forall.Forall2_nth _ _ _ mfix mfix' n Bad_recursive_value Bad_recursive_value) in H8 as [? ?].
edestruct H. specialize (H1 Hnth). rewrite H1.
specialize (IHeval3 (Ident.Map.add y iv2 (add_self self mfix' locals'0)) ih2).
destruct interpret as [ih3 iv3]; cbn in ×.
apply IHeval3; eauto. apply vrel_add; eauto.
apply vrel_locals_add_self; eauto. split; now intros.
- fail_case IHeval Hloc Hheap Heq.
- now apply IHeval.
- cbn; eauto.
- now eapply IHeval.
- cbn; specialize (IHeval1 _ _ Hloc Hheap). destruct interpret as [ih1 iv1]; destruct IHeval1 as [Hheap1 Hiv1].
now eapply IHeval2.
- cbn; specialize (IHeval1 _ _ Hloc Hheap). destruct interpret as [ih1 iv1]; destruct IHeval1 as [Hheap1 Hiv1].
eapply IHeval2; eauto. now apply vrel_add.
- cbn; eapply IHeval; eauto. intros x. clear IHeval. subst.
apply vrel_locals_add_self; eauto.
intros. unfold rfunc. set (l := map snd recs). clearbody self l.
induction l; econstructor; eauto. repeat split.
+ intro H. destruct a; inversion H. destruct p. destruct l0 ; inversion H.
destruct l0 ; now inversion H.
+ intro H; destruct a; inversion H. destruct p. destruct l0 ; inversion H.
destruct l0 ; now inversion H.
+ intros. destruct a; inversion H. destruct p. destruct l0 ; inversion H.
destruct l0 ; now inversion H.
+ destruct a; eauto. destruct p. destruct l0 ; eauto.
destruct l0; inversion 1.
+ destruct a; eauto. destruct p. destruct l0 ; eauto.
destruct l0; inversion 1.
- cbn.
specialize (IHeval1 _ _ Hloc Hheap). destruct interpret as [ih1 iv1]; destruct IHeval1 as [Hheap1 Hiv1].
erewrite find_match_correct; eauto. now apply IHeval2.
- cbn. revert ih Hheap H. induction H0.
+ intros ih Hheap. split ; eauto. econstructor. econstructor.
+ intros ih Hheap. simpl. destruct H as [Heval H].
specialize (H _ _ Hloc Hheap). destruct interpret as [ih1 iv1]; destruct H as [Hheap1 Hiv1].
specialize (IHForall2_acc ih1 Hheap1).
unshelve epose proof (Forall2_acc_map R_heap vrel
(fun (h : Interpreter.heap) (e : t) ⇒ interpret h iglobals ilocals e) _ _ _ _ _ _ H0 _ Hheap1).
{ clear -Hloc. intros. cbn in ×. destruct H0 as [? H0]. specialize (H0 ilocals x'). destruct interpret. apply H0; eauto. }
set (p := map_acc _ ih1 l) in ×. destruct p. destruct H as [Heahp2 Hl0]. split; eauto.
destruct IHForall2_acc as [? IHForall2_acc]. lia. inversion IHForall2_acc; clear IHForall2_acc.
assert (Hl: (int_of_nat (Datatypes.length l) ≤? max_length)%uint63 = true).
{ apply leb_spec. rewrite Int63.of_Z_spec.
rewrite (Forall2_acc_length H0). rewrite Z.mod_small; [lia_max_length |].
unfold max_length in ×. cbn in ×. lia. }
assert (Hl': (int_of_nat (S (Datatypes.length l)) ≤? max_length)%uint63 = true).
{ apply leb_spec. rewrite Int63.of_Z_spec. rewrite (Forall2_acc_length H0).
rewrite Z.mod_small; lia_max_length. }
rewrite Hl in H5. rewrite Hl'. inversion H5; subst. clear H5.
econstructor. econstructor; eauto.
- cbn. specialize (IHeval _ _ Hloc Hheap). destruct interpret as [ih1 iv1]; destruct IHeval as [Hheap1 Hiv1].
split; eauto. inversion Hiv1; subst. clear Hiv1.
eapply All_Forall.Forall2_nth; eauto. econstructor.
- fail_case IHeval Hloc Hheap H0.
- cbn. pose proof (fresh_compat _ _ _ _ Hheap H).
set (Interpreter.fresh ih) in ×. destruct p.
destruct H1; split; [| now econstructor].
eapply update_compat with (default := SemanticsSpec.fail ""); eauto.
split; [reflexivity|].
intros idx Hidx. rewrite <- (int_of_to_nat idx). destruct int_to_nat.
× cbn. econstructor; eauto.
× cbn in Hidx. destruct n; [compute|lia].
econstructor; eauto.
- cbn. specialize (IHeval _ _ Hloc Hheap). destruct interpret as [ih1 iv1]; destruct IHeval as [Hheap1 Hiv1].
inversion Hiv1; subst; clear Hiv1.
pose proof (deref_compat (SemanticsSpec.fail "") _ _ _ _ _ Hheap1 H0 H5).
destruct H2 as [? Hderef]. pose proof (Hderef (int_of_nat 0)).
cbn in H4. rewrite isNotEvaluated_vrel in H3; eauto.
+ eapply H4. lia.
+ destruct is_not_evaluated; inversion H3.
split; eauto. eapply H4. lia.
- cbn; specialize (IHeval1 _ _ Hloc Hheap). destruct interpret as [ih1 iv1]; destruct IHeval1 as [Hheap1 Hiv1].
inversion Hiv1; subst; clear Hiv1.
pose proof (deref_compat (SemanticsSpec.fail "") _ _ _ _ _ Hheap1 H0 H7).
destruct H6 as [? Hderef]. pose proof (Hderef (int_of_nat 0)).
cbn in H8. rewrite isNotEvaluated_vrel in H2; [eapply H8; lia|].
destruct is_not_evaluated; inversion H2. clear H2.
rewrite H1 in Hderef.
specialize (Hderef (int_of_nat 1) (ltac:(eauto))).
rewrite H3 in Hderef. cbn in Hderef. set _.[1] in ×.
inversion Hderef. subst. rewrite <- H11 in Hderef.
specialize (IHeval2 _ _ H9 Hheap1).
destruct interpret as [ih2 iv2]; destruct IHeval2 as [Hheap2 Hiv2].
split; eauto.
eapply update_compat with (default := SemanticsSpec.fail ""); eauto. split; cbn.
× rewrite PArray.length_set. lia.
× intro i. pose proof (int_of_to_nat i). destruct (int_to_nat i); [| destruct n].
+ subst. intros _. rewrite get_set_same; eauto.
rewrite <- (int_of_to_nat (PArray.length _)). rewrite <- H6.
rewrite H1. cbn; lia.
+ subst; intros _. rewrite get_set_other; [now apply eqb_false_spec|]. cbn.
rewrite -/y. rewrite <- H11. econstructor; eauto.
+ lia.
- fail_case IHeval Hloc Hheap H0.
- cbn. split; eauto.
- cbn [interpret]; split; eauto; econstructor.
- cbn [interpret]; split; eauto; econstructor.
- cbn [interpret]; split; eauto; econstructor.
- cbn [interpret]. pose proof (fresh_compat _ _ _ _ Hheap H0).
set (Interpreter.fresh ih) in ×. destruct p.
destruct H2; split; [| now econstructor].
eapply update_compat with (default := SemanticsSpec.fail ""); eauto.
apply Forall2Array_init; eauto.
intros k Hk. pose (int_to_of_nat k).
unfold int_to_nat in e. rewrite e; [lia_max_length| econstructor].
- cbn [interpret]; destruct op; cbn [interpret];
specialize (IHeval _ _ Hloc Hheap); destruct interpret as [ih1 iv1]; destruct IHeval as [Hheap1 Hiv1];
split; eauto; erewrite <- as_ty_vrel; eauto; eapply truncate_vrel.
- cbn [interpret]; destruct op; cbn [interpret];
specialize (IHeval1 _ _ Hloc Hheap); destruct interpret as [ih1 iv1]; destruct IHeval1 as [Hheap1 Hiv1];
specialize (IHeval2 _ _ Hloc Hheap1); destruct interpret as [ih2 iv2]; destruct IHeval2 as [Hheap2 Hiv2];
split; eauto.
1-2: destruct b; repeat erewrite <- (@as_ty_vrel P P'); eauto; eapply truncate_vrel.
destruct b; repeat erewrite <- (@as_ty_vrel P P'); eauto; econstructor.
- cbn [interpret].
specialize (IHeval _ _ Hloc Hheap); destruct interpret as [ih1 iv1]; destruct IHeval as [Hheap1 Hiv1].
split; eauto; erewrite as_float_vrel; eauto; econstructor.
- cbn [interpret]; split; eauto; econstructor.
- cbn [interpret]; split; eauto; econstructor.
- cbn [interpret]; destruct op; cbn [interpret];
specialize (IHeval1 _ _ Hloc Hheap); destruct interpret as [ih1 iv1]; destruct IHeval1 as [Hheap1 Hiv1];
specialize (IHeval2 _ _ Hloc Hheap1); destruct interpret as [ih2 iv2]; destruct IHeval2 as [Hheap2 Hiv2];
split; eauto;cbn; repeat erewrite <- (@as_float_vrel P P'); eauto; econstructor.
- cbn [interpret]; destruct op; cbn [interpret];
specialize (IHeval1 _ _ Hloc Hheap); destruct interpret as [ih1 iv1]; destruct IHeval1 as [Hheap1 Hiv1];
specialize (IHeval2 _ _ Hloc Hheap1); destruct interpret as [ih2 iv2]; destruct IHeval2 as [Hheap2 Hiv2];
split; eauto;cbn; repeat erewrite <- (@as_float_vrel P P'); eauto; econstructor.
- cbn [interpret].
specialize (IHeval _ _ Hloc Hheap); destruct interpret as [ih1 iv1]; destruct IHeval as [Hheap1 Hiv1].
split; eauto. erewrite <- (@as_ty_vrel P P'); eauto; eapply truncate_vrel.
- cbn [interpret].
specialize (IHeval _ _ Hloc Hheap); destruct interpret as [ih1 iv1]; destruct IHeval as [Hheap1 Hiv1].
split; eauto. erewrite <- (@as_ty_vrel P P'); eauto; econstructor.
- cbn [interpret].
specialize (IHeval _ _ Hloc Hheap); destruct interpret as [ih1 iv1]; destruct IHeval as [Hheap1 Hiv1].
split; eauto. erewrite <- (@as_float_vrel P P'); eauto; econstructor.
- cbn [interpret];
specialize (IHeval1 _ _ Hloc Hheap); destruct interpret as [ih1 iv1]; destruct IHeval1 as [Hheap1 Hiv1];
specialize (IHeval2 _ _ Hloc Hheap1); destruct interpret as [ih2 iv2]; destruct IHeval2 as [Hheap2 Hiv2];
inversion Hiv1; subst; clear Hiv1.
pose proof (fresh_compat _ _ _ _ Hheap2 H3).
set (Interpreter.fresh ih2) in ×. destruct p.
destruct H5; split; [| now econstructor].
eapply update_compat with (default := SemanticsSpec.fail ""); eauto.
assert (Hlen' : Int63.of_Z len' = int_of_nat (Z.to_nat len')).
{ unfold int_of_nat. rewrite Z2Nat.id; eauto. }
rewrite Hlen'. apply (Forall2Array_cst _ (Z.to_nat len') _ iv2); eauto.
- cbn [interpret];
specialize (IHeval1 _ _ Hloc Hheap); destruct interpret as [ih1 iv1]; destruct IHeval1 as [Hheap1 Hiv1];
specialize (IHeval2 _ _ Hloc Hheap1); destruct interpret as [ih2 iv2]; destruct IHeval2 as [Hheap2 Hiv2];
inversion Hiv1; subst; clear Hiv1.
inversion Hiv2; subst; clear Hiv2. rewrite H3.
pose proof (fresh_compat _ _ _ _ Hheap2 H4).
set (Interpreter.fresh ih2) in ×. destruct p.
destruct H6; split; [| now econstructor].
eapply update_compat with (default := SemanticsSpec.fail ""); eauto.
unfold List.init. unfold Forall2Array.
assert (Hlen' : Int63.of_Z len' = int_of_nat (Z.to_nat len')).
{ unfold int_of_nat. rewrite Z2Nat.id; eauto. }
rewrite Hlen'. apply Forall2Array_cst; eauto.
econstructor.
- cbn [interpret];
specialize (IHeval1 _ _ Hloc Hheap); destruct interpret as [ih1 iv1]; destruct IHeval1 as [Hheap1 Hiv1];
specialize (IHeval2 _ _ Hloc Hheap1); destruct interpret as [ih2 iv2]; destruct IHeval2 as [Hheap2 Hiv2];
inversion Hiv1; subst; clear Hiv1.
split; eauto.
pose proof (deref_compat (SemanticsSpec.fail "") _ _ _ _ _ Hheap H1 H5).
destruct H2 as [? Hderef].
case (vector_type_eqb ty ty').
2: {
destruct idx'; destruct iv2; try (destruct p as [i0 ?]; destruct i0);
try (destruct p0 as [i1 ?]; destruct i1); try econstructor. }
destruct idx'; destruct iv2;
try (destruct p as [i0 n]; destruct i0);
try (destruct p0 as [i1 n']; destruct i1); try econstructor;
try inversion Hiv2. subst.
pose proof (leb_length _ (deref ih ptr')).
case_eq ((0 <=? n')%Z); intro; simpl; try econstructor.
case_eq (n' <? Z.of_nat (Datatypes.length arr))%Z;
case_eq (n' <? φ (PArray.length (deref ih ptr'))%uint63)%Z; intros.
+ assert (Hn': (0 ≤ n' < Int63.wB)%Z).
{split; [lia|]. clear -H3 H4 H6.
apply leb_spec in H3. apply Z.ltb_lt in H6.
set (PArray.length _) in ×. clearbody i.
clear H4. lia_max_length. }
assert (Heqn' : Z.to_nat n' = int_to_nat (Int63.of_Z n')).
{ unfold int_to_nat. f_equal. rewrite Int63.of_Z_spec.
rewrite Z.mod_small; eauto. }
rewrite Heqn'. apply Hderef. unfold int_to_nat. rewrite Int63.of_Z_spec.
rewrite Z.mod_small; eauto. apply Z.ltb_lt in H7.
lia.
+ rewrite H2 in H7. unfold int_to_nat in H7.
rewrite Z2Nat.id in H7. apply to_Z_bounded.
rewrite H7 in H6. inversion H6.
+ rewrite H2 in H7. unfold int_to_nat in H7.
rewrite Z2Nat.id in H7. apply to_Z_bounded.
rewrite H7 in H6. inversion H6.
+ econstructor.
- cbn [interpret]; specialize (IHeval1 _ _ Hloc Hheap). destruct interpret as [ih1 iv1]; destruct IHeval1 as [Hheap1 Hiv1].
specialize (IHeval2 _ _ Hloc Hheap1).
destruct interpret as [ih2 iv2]; destruct IHeval2 as [Hheap2 Hiv2].
inversion Hiv1 ; subst. inversion Hiv2 ; subst. specialize (IHeval3 _ _ Hloc Hheap2).
destruct interpret as [ih3 iv3]. destruct IHeval3 as [Hheap3 Hiv3].
case_eq (vector_type_eqb ty ty'); [| repeat econstructor; eauto].
pose proof (deref_compat (SemanticsSpec.fail "") _ _ _ _ _ Hheap H2 H7).
destruct H4 as [Hsize Hderef].
rewrite Hsize. unfold int_to_nat. rewrite Z2Nat.id.
pose (to_Z_bounded (PArray.length (deref ih ptr'))); lia.
intro Htyty'.
case_eq (Z.leb 0 i && (Z.ltb i (Int63.to_Z (PArray.length (deref ih ptr')))))%bool;
[| repeat econstructor; eauto].
rename i into z. intro Harr. apply MRProd.andb_and in Harr.
destruct Harr as [Hz0 Harr]. apply Z.leb_le in Hz0.
apply Z.ltb_lt in Harr.
pose proof (Hmax := leb_length _ (deref ih ptr')).
apply leb_spec in Hmax.
destruct ty.
+ split; [| econstructor; eauto].
eapply update_compat with (default := SemanticsSpec.fail ""); eauto.
split. now rewrite List.length_set PArray.length_set.
intros i Hi. set (arr' := deref _ _) in ×. clearbody arr'.
case_eq (i =? Int63.of_Z z)%uint63.
× intro eq; apply eqb_correct in eq. subst.
unfold int_to_nat. rewrite Int63.of_Z_spec Z.mod_small;
[ lia_max_length |].
rewrite get_set_same; eauto.
apply ltb_spec.
rewrite Int63.of_Z_spec Z.mod_small; lia_max_length.
pose (Hnth := List.nth_set_same). rewrite Hnth; eauto.
rewrite Hsize. unfold int_to_nat. apply Z2Nat.inj_lt; cbn in *; lia.
× rewrite eqb_false_spec. intro Hneq. rewrite get_set_other; eauto.
rewrite List.nth_set_other. intro Hneq'; apply Hneq.
assert (int_of_nat (Z.to_nat z) = int_of_nat (int_to_nat i)) by now f_equal.
rewrite int_of_to_nat in H4. unfold int_of_nat in H4.
rewrite Z2Nat.id in H4; [lia | eauto].
eapply Hderef. now rewrite List.length_set in Hi.
+ destruct iv3; inversion Hiv3; try repeat econstructor; eauto.
destruct ty; try repeat econstructor; eauto.
case_eq ((0 <=? i)%Z && (i <? 256)%Z)%bool; try repeat econstructor; eauto.
eapply update_compat with (default := SemanticsSpec.fail ""); eauto.
split. now rewrite List.length_set PArray.length_set. rename i into z'.
intros i Hi. set (arr' := deref _ _) in ×. clearbody arr'.
case_eq (i =? Int63.of_Z z)%uint63.
× intro eq; apply eqb_correct in eq. subst.
unfold int_to_nat. rewrite Int63.of_Z_spec Z.mod_small; [lia_max_length |].
rewrite get_set_same; eauto.
apply ltb_spec. rewrite Int63.of_Z_spec Z.mod_small; lia_max_length.
pose (Hnth := List.nth_set_same). rewrite Hnth; eauto.
rewrite Hsize. unfold int_to_nat. apply Z2Nat.inj_lt; cbn in *; lia.
× rewrite eqb_false_spec. intro Hneq. rewrite get_set_other; eauto.
rewrite List.nth_set_other. intro Hneq'; apply Hneq.
assert (int_of_nat (Z.to_nat z) = int_of_nat (int_to_nat i)) by now f_equal.
rewrite int_of_to_nat in H8. unfold int_of_nat in H8.
rewrite Z2Nat.id in H8; [lia | eauto].
eapply Hderef. now rewrite List.length_set in Hi.
- cbn [interpret].
specialize (IHeval _ _ Hloc Hheap); destruct interpret as [ih1 iv1]; destruct IHeval as [Hheap1 Hiv1].
split; eauto. inversion Hiv1; subst.
destruct (vector_type_eqb ty ty'); try econstructor.
pose proof (deref_compat (SemanticsSpec.fail "") _ _ _ _ _ Hheap H0 H4).
destruct H1 as [Hsize Hderef]. rewrite Hsize.
unfold int_to_nat. rewrite Z2Nat.id.
pose (to_Z_bounded (PArray.length (deref ih ptr'))); lia.
econstructor.
Qed.
Set Guard Checking.
Import ListNotations.
Require Import Malfunction.Malfunction Malfunction.SemanticsSpec Malfunction.utils_array.
From MetaRocq.Utils Require Import bytestring.
Open Scope bs.
From Stdlib Require Import Uint63.
Class Heap `{Pointer} := {
heapGen : ∀ (value : Type), Type;
fresh : ∀ {value : Type}, heapGen value → pointer × heapGen value;
deref : ∀ {value : Type}, heapGen value → pointer → array value;
update : ∀ {value : Type}, heapGen value → pointer → array value → heapGen value
}.
Definition CanonicalHeap : @Heap CanonicalPointer :=
{| heapGen := fun value ⇒ (int × (int → array value))%type;
fresh := fun _ '(max_ptr , h) ⇒ let ptr := Int63.add max_ptr (int_of_nat 1) : @pointer CanonicalPointer in (ptr ,(ptr, h));
deref := fun _ '(_,h) ptr ⇒ h ptr;
update := fun _ '(max_ptr , h) ptr arr ⇒ (max_ptr , fun ptr' ⇒ if Int63.eqb ptr ptr' then arr else h ptr) |}.
Definition heap `{Heap} := heapGen value.
Definition is_not_evaluated `{Pointer} : value → bool :=
fun v ⇒ match v with | not_evaluated ⇒ true | _ ⇒ false end.
Definition find_match `{Heap} (interpret : heap → @Ident.Map.t value → @Ident.Map.t value → t → heap × value)
:= fun h iglobals ilocals scr ⇒ fix find_match x := match x with
| (cases, e) :: rest ⇒
if List.existsb (cond scr) cases then
interpret h iglobals ilocals e
else
find_match rest
| [] ⇒ (h, fail "no case matches") end.
#[bypass_check(guard)]
Fixpoint interpret `{Pointer} `{Heap} (h : heap)
(globals : @Ident.Map.t value)
(locals : @Ident.Map.t value)
(x : t) {struct x} : heap × value :=
match x with
| Mvar v ⇒ (h, Ident.Map.find v locals)
| Mlambda (xs, e) ⇒
(h, match xs with
| [ ] ⇒ fail "assert false"
| x :: xs ⇒
let (x , e) := match xs with
| [] ⇒ (x , e)
| _ :: _ ⇒ (x , Mlambda (xs, e)) end
in Func (locals, x , e)
end)
| Mapply (f_, vs) ⇒
List.fold_left (fun f v ⇒ match f with
| (h , Func (locals', x, e)) ⇒
let (h' , v') := interpret h globals locals v
in interpret h' globals (Ident.Map.add x v' locals') e
| (h , (RClos (locals', self, mfix , n))) ⇒
let (h' , v') := interpret h globals locals v in
match nth n mfix Bad_recursive_value with
| RFunc (y , e) ⇒
interpret h' globals (Ident.Map.add y v' (add_self self mfix locals')) e
| _ ⇒ (h', fail "not a function") end
| (h , _) ⇒ (h , fail ("not a function: " ++ " evaluated to: ")) end) vs
(interpret h globals locals f_)
| Mlet (bindings, body) ⇒
let bind :=
fix bind (h : heap) (locals : @Ident.Map.t value) (bindings : list binding) {struct bindings}: heap × value :=
match bindings with
| [] ⇒ interpret h globals locals body
| Unnamed e :: bindings ⇒
let (h' , _) := interpret h globals locals e in bind h' locals bindings
| Named (x, e) :: bindings ⇒
let (h' ,v) := interpret h globals locals e in
bind h' (Ident.Map.add x v (locals)) bindings
| Recursive recs :: bindings ⇒
let self := map fst recs in
let rfunc := RFunc_build (map snd recs) in
bind h (add_self self rfunc locals) bindings
end
in
bind h locals bindings
| Mnum (numconst_Int n) ⇒ (h , value_Int (Int, Int63.to_Z n))
| Mnum (numconst_Bigint n) ⇒ (h , value_Int (Bigint, n))
| Mnum (numconst_Float64 f) ⇒ (h, Float f)
| Mstring s ⇒
let (ptr,h') := fresh h in
let str := Array_init (Int63.of_Z (Z.of_nat (String.length s)))
(fun i ⇒ value_Int (Int, (Z.of_nat (Byte.to_nat (option_def (Ascii.byte_of_ascii Ascii.Space) (get (Z.to_nat (Int63.to_Z i)) s)))))) in
(update h' ptr str , Vec (Bytevec, ptr))
| Mglobal v ⇒ (h , Ident.Map.find v globals)
| Mswitch (scr, cases) ⇒
let (h', scr') := interpret h globals locals scr in
find_match interpret h' globals locals scr' cases
| Mnumop1 (op, embed_inttype ty, e) ⇒
let (h',v) := interpret h globals locals e in
let n := as_ty ty v in
(h', truncate ty (match op with Malfunction.Neg ⇒ Z.mul (-1) n | Not ⇒ Z.lnot n end))
| Mnumop2 (op, embed_inttype ty, e1, e2) ⇒
let (h1 , e1) := interpret h globals locals e1 in
let (h2 , e2) := interpret h1 globals locals e2 in
(h2, match op with
| embed_binary_arith_op op ⇒
let f := match op with
| Add ⇒ Z.add | Sub ⇒ Z.sub
| Mul ⇒ Z.mul | Div ⇒ Z.div | Mod ⇒ Z.rem
end in
truncate ty (f (as_ty ty e1) (as_ty ty e2))
| embed_binary_bitwise_op op ⇒
let n := as_ty ty e1 in
let c := as_ty Int e2 in
truncate ty (match op with
| And ⇒ Z.land (as_ty ty e1) (as_ty ty e2)
| Or ⇒ Z.lor (as_ty ty e1) (as_ty ty e2)
| Xor ⇒ Z.lxor (as_ty ty e1) (as_ty ty e2)
| Lsl ⇒ Z.shiftl n c
| Asr ⇒ Z.shiftr n c
| Lsr ⇒
let n := match ty with
| Bigint ⇒ n
| _op ⇒
let w := bitwidth ty in
Z.land n (Z.sub (Z.shiftl (Z.of_nat 1) w) (Z.of_nat 1)) end in
Z.shiftr n c end)
| embed_binary_comparison op ⇒
let cmp := Z.compare (as_ty ty e1) (as_ty ty e2) in
let res := match op with
| Lt ⇒ comparison_eqb cmp Datatypes.Lt
| Gt ⇒ comparison_eqb cmp Datatypes.Gt
| Lte ⇒ negb (comparison_eqb cmp Datatypes.Gt)
| Gte ⇒ negb (comparison_eqb cmp Datatypes.Lt)
| Eq ⇒ comparison_eqb cmp Datatypes.Eq
end in
value_Int (Int, if res then 1%Z else 0%Z)
end)
| Mnumop1 (Malfunction.Neg, Float64, e) ⇒
let (h' , v) := interpret h globals locals e in (h' , Float (- as_float v))
| Mnumop1 (Not, Float64, _)
| Mnumop2 (embed_binary_bitwise_op _, Float64, _, _) ⇒
(h , fail "invalid bitwise float operation")
| Mnumop2 (embed_binary_arith_op op, Float64, e1, e2) ⇒
let (h1,e1') := interpret h globals locals e1 in
let (h2,e2') := interpret h1 globals locals e2 in
let e1 := as_float e1' in
let e2 := as_float e2' in
(h2, Float (match op with
| Add ⇒ e1 + e2
| Sub ⇒ e1 - e2
| Mul ⇒ e1 × e2
| Div ⇒ e1 / e2
| Mod ⇒ fail_float "mod on floats not supported" end))
| Mnumop2 (embed_binary_comparison op, Float64, e1, e2) ⇒
let (h1,e1') := interpret h globals locals e1 in
let (h2,e2') := interpret h1 globals locals e2 in
let e1 := as_float e1' in
let e2 := as_float e2' in
let res := match op with
| Lt ⇒ PrimFloat.ltb e1 e2
| Gt ⇒ PrimFloat.ltb e2 e2
| Lte ⇒ PrimFloat.leb e1 e2
| Gte ⇒ PrimFloat.leb e2 e1
| Eq ⇒ PrimFloat.eqb e1 e2
end in
(h2, value_Int (Int, if res then 1%Z else 0%Z))
| Mconvert (embed_inttype src, embed_inttype dst, e) ⇒
let (h',v) := interpret h globals locals e in
(h', truncate dst (as_ty src v))
| Mconvert (embed_inttype src, Float64, e) ⇒
let (h',v) := interpret h globals locals e in
(h',Float (PrimFloat.of_uint63 (Int63.of_Z (as_ty src v))))
| Mconvert (Float64, Float64, e) ⇒
let (h',v) := interpret h globals locals e in
(h',Float (as_float v))
| Mvecnew (ty, len, def) ⇒
let (h1,len') := interpret h globals locals len in
let (h2,def') := interpret h1 globals locals def in
let (ptr,h3) := fresh h2 in
match ty, len' , def' with
| Array, value_Int (Int, len), v ⇒
(update h3 ptr (PArray.make (Int63.of_Z len) v), Vec (Array, ptr))
| Bytevec, value_Int (Int, len), (value_Int (Int, k)) as v ⇒
if Z.leb 0%Z k && Z.ltb k 256 then
(update h3 ptr (PArray.make (Int63.of_Z len) v), Vec (Bytevec, ptr))
else
(h3,fail "bad vector creation")
| _, _, _ ⇒ (h2,fail "bad vector creation")
end
| Mvecget (ty, vec, idx) ⇒
let (h1,vec') := interpret h globals locals vec in
let (h2,idx') := interpret h1 globals locals idx in
(h2, match vec', idx' with
| Vec (ty', ptr), value_Int (Int,i) ⇒
if vector_type_eqb ty ty' then
if Z.leb 0 i && Z.ltb i (Int63.to_Z (PArray.length (deref h ptr))) then
PArray.get (deref h ptr) (Int63.of_Z i)
else
fail "index out of bounds: %d"
else
fail "wrong vector type"
| _, _ ⇒ fail "wrong vector type"
end)
| Mvecset (ty, vec, idx, e) ⇒
let (h1,vec') := interpret h globals locals vec in
let (h2,idx') := interpret h1 globals locals idx in
let (h3,v) := interpret h2 globals locals e in
match vec', idx', v with
| Vec (ty', ptr), value_Int (Int, i), v ⇒
if vector_type_eqb ty ty' then
let i' := Int63.of_Z i in
if Z.leb 0 i && Z.ltb i (Int63.to_Z (PArray.length (deref h ptr))) then
match ty, v with
| Array, _ ⇒ (update h3 ptr (PArray.set (deref h ptr) i' v), value_Int (Int, 0%Z))
| Bytevec, value_Int (Int, val) ⇒
if (Z.leb 0 val) && (Z.ltb val 256)
then
(update h3 ptr (PArray.set (deref h ptr) i' v), value_Int (Int, 0%Z))
else (h3, fail "not a byte")
| Bytevec, _ ⇒ (h3, fail "not a byte")
end
else (h3, fail "index out of bounds: %d")
else (h3, fail "wrong vector type")
| _ , _ , _ ⇒ (h3, fail "wrong vector type")
end
| Mveclen (ty, vec) ⇒
let (h',vec') := interpret h globals locals vec in
(h', match vec' with
| Vec (ty', ptr) ⇒
if vector_type_eqb ty ty' then value_Int (Int, Int63.to_Z (PArray.length (deref h ptr)))
else fail "wrong vector type"
| _ ⇒ fail "wrong vector type"
end)
| Mblock (tag, vals) ⇒
let (h',vals') := map_acc (fun h e ⇒ interpret h globals locals e) h vals in
(h', if (int_of_nat (Datatypes.length vals) ≤? max_length)%uint63
then Block (tag, vals')
else fail "vals is a too big array")
| Mfield (idx, b) ⇒
let (h',b') := interpret h globals locals b in
(h', match b' with
| Block (_, vals) ⇒ nth (int_to_nat idx) vals (fail "")
| _ ⇒ fail "not a block"
end)
| Mlazy e ⇒
let (ptr,h') := fresh h in
let init := PArray.make (Int63.of_Z 2) not_evaluated in
let arr := PArray.set init (Int63.of_Z 1) (Lazy (locals , e)) in
(update h' ptr arr, Thunk ptr)
| Mforce e ⇒
let (h',v) := interpret h globals locals e in
match v with
| Thunk ptr ⇒ let arr := deref h' ptr in
let lazy := PArray.get arr (Int63.of_Z 0) in
if is_not_evaluated lazy
then
match PArray.get arr (Int63.of_Z 1) with
| Lazy (locals , e) ⇒
let (h'' , v') := interpret h' globals locals e in
(update h'' ptr (PArray.set arr (Int63.of_Z 0) v'), v')
| _ ⇒ (h', fail "not a lazy value")
end
else (h', lazy)
| _ ⇒ (h', fail "not a lazy value")
end
| _ ⇒ (h , fail "assert todo")
end.
Class CompatiblePtr (P P' : Pointer) :=
{ R_ptr : P.(pointer) → P'.(pointer) → Prop }.
Unset Elimination Schemes.
Inductive vrel {P P' : Pointer} {H : CompatiblePtr P P'} : @value P → @value P' → Prop :=
| vBlock : ∀ tag vals vals', Forall2 vrel vals vals' →
vrel (Block (tag, vals)) (Block (tag, vals'))
| vVec : ∀ ty ptr ptr', R_ptr ptr ptr' → vrel (Vec (ty, ptr)) (Vec (ty, ptr'))
| vFunc : ∀ x locals locals' e,
(∀ x, vrel (locals x) (locals' x)) →
vrel (Func (locals,x,e)) (Func (locals',x,e))
| vRClos : ∀ self mfix mfix' n locals locals',
(∀ x, vrel (locals x) (locals' x)) →
Forall2 (fun a b ⇒
(∀ y e, (a = RFunc (y, e)) ↔ (b = RFunc (y, e))) ∧
(∀ ptr ptr', a = RThunk ptr → b = RThunk ptr' → R_ptr ptr ptr') ∧
(a = Bad_recursive_value ↔ b = Bad_recursive_value)) mfix mfix' →
vrel (RClos (locals,self,mfix,n)) (RClos (locals',self,mfix',n))
| vInt : ∀ ty i ,
vrel (value_Int (ty, i)) (value_Int (ty, i))
| vFloat : ∀ f,
vrel (Float f) (Float f)
| vThunk : ∀ ptr ptr', R_ptr ptr ptr' →
vrel (Thunk ptr) (Thunk ptr')
| vLazy : ∀ e locals locals',
(∀ x, vrel (locals x) (locals' x)) →
vrel (Lazy (locals, e)) (Lazy (locals' , e))
| vFail : ∀ s, vrel (fail s) (fail s)
| vNot_evaluated : vrel not_evaluated not_evaluated.
Lemma vrel_ind : ∀ (P P' : Pointer) (H : CompatiblePtr P P')
(P0 : value → value → Prop),
(∀ (tag : Malfunction.int) (vals vals' : list value),
Forall2 vrel vals vals' →
Forall2 P0 vals vals' →
P0 (Block (tag, vals)) (Block (tag, vals'))) →
(∀ (ty : vector_type) (ptr ptr' : pointer),
R_ptr ptr ptr' → P0 (Vec (ty, ptr)) (Vec (ty, ptr'))) →
(∀ (x : Ident.t) (locals locals' : Ident.t → value) (e : t),
(∀ x0 : Ident.t, vrel (locals x0) (locals' x0)) →
(∀ x0 : Ident.t, P0 (locals x0) (locals' x0)) →
P0 (Func (locals, x, e)) (Func (locals', x, e))) →
(∀ (self : list Ident.t) (mfix mfix' : list rec_value)
(n : nat) (locals locals' : Ident.t → value),
(∀ x : Ident.t, vrel (locals x) (locals' x)) →
(∀ x : Ident.t, P0 (locals x) (locals' x)) →
Forall2
(fun a b : rec_value ⇒
(∀ y e, a = RFunc (y, e) ↔ b = RFunc (y, e)) ∧
(∀ ptr ptr', a = RThunk ptr → b = RThunk ptr' → R_ptr ptr ptr') ∧
(a = Bad_recursive_value ↔ b = Bad_recursive_value)) mfix mfix' →
P0 (RClos (locals, self, mfix, n)) (RClos (locals', self, mfix', n))) →
(∀ (ty : inttype) (i : Z),
P0 (value_Int (ty, i)) (value_Int (ty, i))) →
(∀ f4 : float, P0 (Float f4) (Float f4)) →
(∀ ptr ptr' : pointer,
R_ptr ptr ptr' → P0 (Thunk ptr) (Thunk ptr')) →
(∀ (e : t) (locals locals' : Ident.t → value),
(∀ x : Ident.t, vrel (locals x) (locals' x)) →
(∀ x : Ident.t, P0 (locals x) (locals' x)) →
P0 (Lazy (locals, e)) (Lazy (locals', e))) →
(∀ s : string, P0 (fail s) (fail s)) →
P0 not_evaluated not_evaluated →
∀ v v0 : value, vrel v v0 → P0 v v0.
Proof.
intros.
revert v v0 H10.
fix f 3. intros v V0 [| | | | | | | | | ].
2-10:eauto.
- eapply H0; eauto. induction H10; try econstructor; eauto.
Qed.
Set Elimination Schemes.
Definition CompatiblePtr_sym {P P' : Pointer} `{@CompatiblePtr P P'} : @CompatiblePtr P' P
:= {| R_ptr := fun p' p ⇒ R_ptr p p' |}.
Lemma vrel_sym {P P' : Pointer} `{@CompatiblePtr P P'} v v' :
vrel v v' → @vrel _ _ CompatiblePtr_sym v' v.
Proof.
induction 1; econstructor; eauto.
- induction H1; econstructor; try inversion H0; eauto.
- clear - H2; induction H2; econstructor; eauto. clear -H0.
destruct H0 as [? [? [? ?]]]. repeat split; eauto.
+ eapply H0.
+ eapply H0.
+ intros. eapply H1; eauto.
Qed.
Definition vrel_locals `{CompatiblePtr}
: Ident.Map.t → Ident.Map.t → Prop := fun locals ilocals ⇒ ∀ x, vrel (locals x) (ilocals x).
Class CompatibleHeap {P P' : Pointer} {H : CompatiblePtr P P'}
{HP : @SemanticsSpec.Heap P} {HP' : @Heap P'} :=
{ R_heap : SemanticsSpec.heap → heap → Prop;
fresh_compat : ∀ h ptr h' ih,
R_heap h ih → SemanticsSpec.fresh h ptr h' →
let (iptr,ih') := fresh ih in R_ptr ptr iptr ∧ R_heap h' ih';
update_compat : ∀ default h ih ptr ptr' h' v v',
R_heap h ih → SemanticsSpec.update h ptr v h' →
R_ptr ptr ptr' → Forall2Array vrel v v' default →
let ih' := Interpreter.update ih ptr' v' in R_heap h' ih';
deref_compat : ∀ default h ih ptr ptr' vals,
R_heap h ih → SemanticsSpec.deref h ptr vals →
R_ptr ptr ptr' →
let vals' := Interpreter.deref ih ptr' in
Forall2Array vrel vals vals' default
}.
Lemma cond_correct `{CompatiblePtr}
scr scr' x : vrel scr scr' →
cond scr x = cond scr' x.
Proof.
now destruct x as [ | | [] ]; destruct 1.
Qed.
Lemma existsb_ext {A} (f g : A → bool) l :
(∀ x, f x = g x) →
existsb f l = existsb g l.
Proof.
intros H; induction l; cbn; congruence.
Qed.
Lemma find_match_correct `{CompatibleHeap}
scr scr' cases e h iglobals ilocals :
vrel scr scr' →
SemanticsSpec.find_match scr cases = Some e →
Interpreter.find_match Interpreter.interpret h iglobals ilocals scr' cases = interpret h iglobals ilocals e.
Proof.
induction cases as [ | a cases IHcases ]; cbn [SemanticsSpec.find_match]; intros rel Eq.
- inversion Eq.
- destruct a.
cbn [find_match].
destruct existsb eqn:E.
× inversion Eq. erewrite existsb_ext.
2:{ intros. symmetry. eapply cond_correct. eauto. }
now rewrite E.
× erewrite existsb_ext.
2:{ intros. symmetry. eapply cond_correct. eauto. }
rewrite E. eauto.
Qed.
Lemma vrel_add `{CompatiblePtr} x v iv locals ilocals : vrel v iv → vrel_locals locals ilocals →
vrel_locals (Ident.Map.add x v locals) (Ident.Map.add x iv ilocals).
Proof.
intros Hv Hlocals nm. unfold Ident.Map.add. now destruct Ident.eqb.
Qed.
Lemma isNotEvaluated_vrel `{CompatibleHeap} v v' b :
vrel v v' → isNotEvaluated v = b ↔ is_not_evaluated v' = b.
Proof.
now destruct 1.
Qed.
Ltac fail_case IHeval Hloc Hheap Heq :=
let Hv := fresh "iv1" in cbn; specialize (IHeval _ _ Hloc Hheap); destruct interpret as [? ?];
destruct IHeval as [? Hv]; destruct Hv; inversion Heq; split;eauto; econstructor.
Lemma vrel_locals_add_self `{CompatiblePtr} locals' locals'0 mfix mfix' self :
(∀ x : Ident.t, vrel (locals' x) (locals'0 x)) →
Forall2 (fun a b ⇒
(∀ y e, (a = RFunc (y, e)) ↔ (b = RFunc (y, e))) ∧
(∀ ptr ptr', a = RThunk ptr → b = RThunk ptr' → R_ptr ptr ptr') ∧
(a = Bad_recursive_value ↔ b = Bad_recursive_value)) mfix mfix' →
vrel_locals (SemanticsSpec.add_self self mfix locals') (add_self self mfix' locals'0).
Proof.
intros Hloc ?.
unfold add_self, SemanticsSpec.add_self.
unfold add_recs, SemanticsSpec.add_recs. unfold List.mapi.
generalize 0. generalize self at 1 3.
pose proof (Hcopy := Hloc). revert Hcopy.
generalize locals' at 1 3. generalize locals'0 at 1 3.
revert locals' locals'0 Hloc.
induction self; eauto; cbn; intros.
intro. unfold Ident.Map.add. case_eq (Ident.eqb x a); intro; eauto.
- econstructor; eauto.
- apply IHself; eauto.
Qed.
Lemma as_ty_vrel `{CompatiblePtr} ty v v' :
vrel v v' → as_ty ty v = as_ty ty v'.
Proof.
inversion 1; destruct ty; cbn; try reflexivity.
Defined.
Lemma as_float_vrel `{CompatiblePtr} v v' :
vrel v v' → as_float v = as_float v'.
Proof.
inversion 1; cbn; try reflexivity.
Defined.
Lemma truncate_vrel `{CompatiblePtr} ty z :
vrel (SemanticsSpec.truncate ty z) (truncate ty z).
destruct ty; econstructor.
Qed.
Lemma eval_correct `{CompatibleHeap}
globals locals ilocals iglobals e h h' ih v :
(∀ nm val, In (nm, val) globals → vrel val (iglobals nm)) →
vrel_locals locals ilocals →
R_heap h ih →
eval _ _ globals locals h e h' v →
let (ih',iv) := interpret ih iglobals ilocals e in R_heap h' ih' ∧ vrel v iv.
Proof.
rename H into _CPtr; rename H0 into _CHeap.
intros Hglob Hloc Hheap.
induction 1 as [ locals h x e
| locals h x ids e H
| locals h1 h2 h3 h4 x locals' e e2 v2 e1 v H IHeval1 H0 IHeval2 H1 IHeval3
| locals h1 h2 h3 h4 mfix n y e locals' self e2 v2 e1 v H IHeval1 H0 IHeval2 Hnth H1 IHeval3
| locals h h' e2 e v Heval IHeval Heq
| locals h h' e3 e2 e1 v vals tag IHeval
|
| | | |
|
|
| locals h h' idx b vals tag H IHeval | | | | | |
| | | | | | | | | | | | | | | | | | | ]
in ih, Hheap, ilocals, Hloc |- ×.
- split; eauto. econstructor; eauto.
- split; eauto.
destruct ids as [ | t ids ]; cbn in H. 1:inversion H. clear H.
econstructor; eauto.
- cbn; specialize (IHeval1 _ _ Hloc Hheap). destruct interpret as [ih1 iv1]; destruct IHeval1 as [Hheap1 Hiv1].
specialize (IHeval2 _ _ Hloc Hheap1). destruct interpret as [ih2 iv2]; destruct IHeval2 as [Hheap2 Hiv2].
inversion Hiv1 ; subst.
specialize (IHeval3 (Ident.Map.add x iv2 locals'0) ih2).
destruct interpret as [ih3 iv3]; cbn in ×.
apply IHeval3; eauto. now apply vrel_add.
- cbn; specialize (IHeval1 _ _ Hloc Hheap). destruct interpret as [ih1 iv1]; destruct IHeval1 as [Hheap1 Hiv1].
specialize (IHeval2 _ _ Hloc Hheap1). destruct interpret as [ih2 iv2]; destruct IHeval2 as [Hheap2 Hiv2].
inversion Hiv1 ; subst. clear -H8 Hiv2 H7 Hheap2 Hnth IHeval3.
pose proof (Hmfix := H8).
eapply (All_Forall.Forall2_nth _ _ _ mfix mfix' n Bad_recursive_value Bad_recursive_value) in H8 as [? ?].
edestruct H. specialize (H1 Hnth). rewrite H1.
specialize (IHeval3 (Ident.Map.add y iv2 (add_self self mfix' locals'0)) ih2).
destruct interpret as [ih3 iv3]; cbn in ×.
apply IHeval3; eauto. apply vrel_add; eauto.
apply vrel_locals_add_self; eauto. split; now intros.
- fail_case IHeval Hloc Hheap Heq.
- now apply IHeval.
- cbn; eauto.
- now eapply IHeval.
- cbn; specialize (IHeval1 _ _ Hloc Hheap). destruct interpret as [ih1 iv1]; destruct IHeval1 as [Hheap1 Hiv1].
now eapply IHeval2.
- cbn; specialize (IHeval1 _ _ Hloc Hheap). destruct interpret as [ih1 iv1]; destruct IHeval1 as [Hheap1 Hiv1].
eapply IHeval2; eauto. now apply vrel_add.
- cbn; eapply IHeval; eauto. intros x. clear IHeval. subst.
apply vrel_locals_add_self; eauto.
intros. unfold rfunc. set (l := map snd recs). clearbody self l.
induction l; econstructor; eauto. repeat split.
+ intro H. destruct a; inversion H. destruct p. destruct l0 ; inversion H.
destruct l0 ; now inversion H.
+ intro H; destruct a; inversion H. destruct p. destruct l0 ; inversion H.
destruct l0 ; now inversion H.
+ intros. destruct a; inversion H. destruct p. destruct l0 ; inversion H.
destruct l0 ; now inversion H.
+ destruct a; eauto. destruct p. destruct l0 ; eauto.
destruct l0; inversion 1.
+ destruct a; eauto. destruct p. destruct l0 ; eauto.
destruct l0; inversion 1.
- cbn.
specialize (IHeval1 _ _ Hloc Hheap). destruct interpret as [ih1 iv1]; destruct IHeval1 as [Hheap1 Hiv1].
erewrite find_match_correct; eauto. now apply IHeval2.
- cbn. revert ih Hheap H. induction H0.
+ intros ih Hheap. split ; eauto. econstructor. econstructor.
+ intros ih Hheap. simpl. destruct H as [Heval H].
specialize (H _ _ Hloc Hheap). destruct interpret as [ih1 iv1]; destruct H as [Hheap1 Hiv1].
specialize (IHForall2_acc ih1 Hheap1).
unshelve epose proof (Forall2_acc_map R_heap vrel
(fun (h : Interpreter.heap) (e : t) ⇒ interpret h iglobals ilocals e) _ _ _ _ _ _ H0 _ Hheap1).
{ clear -Hloc. intros. cbn in ×. destruct H0 as [? H0]. specialize (H0 ilocals x'). destruct interpret. apply H0; eauto. }
set (p := map_acc _ ih1 l) in ×. destruct p. destruct H as [Heahp2 Hl0]. split; eauto.
destruct IHForall2_acc as [? IHForall2_acc]. lia. inversion IHForall2_acc; clear IHForall2_acc.
assert (Hl: (int_of_nat (Datatypes.length l) ≤? max_length)%uint63 = true).
{ apply leb_spec. rewrite Int63.of_Z_spec.
rewrite (Forall2_acc_length H0). rewrite Z.mod_small; [lia_max_length |].
unfold max_length in ×. cbn in ×. lia. }
assert (Hl': (int_of_nat (S (Datatypes.length l)) ≤? max_length)%uint63 = true).
{ apply leb_spec. rewrite Int63.of_Z_spec. rewrite (Forall2_acc_length H0).
rewrite Z.mod_small; lia_max_length. }
rewrite Hl in H5. rewrite Hl'. inversion H5; subst. clear H5.
econstructor. econstructor; eauto.
- cbn. specialize (IHeval _ _ Hloc Hheap). destruct interpret as [ih1 iv1]; destruct IHeval as [Hheap1 Hiv1].
split; eauto. inversion Hiv1; subst. clear Hiv1.
eapply All_Forall.Forall2_nth; eauto. econstructor.
- fail_case IHeval Hloc Hheap H0.
- cbn. pose proof (fresh_compat _ _ _ _ Hheap H).
set (Interpreter.fresh ih) in ×. destruct p.
destruct H1; split; [| now econstructor].
eapply update_compat with (default := SemanticsSpec.fail ""); eauto.
split; [reflexivity|].
intros idx Hidx. rewrite <- (int_of_to_nat idx). destruct int_to_nat.
× cbn. econstructor; eauto.
× cbn in Hidx. destruct n; [compute|lia].
econstructor; eauto.
- cbn. specialize (IHeval _ _ Hloc Hheap). destruct interpret as [ih1 iv1]; destruct IHeval as [Hheap1 Hiv1].
inversion Hiv1; subst; clear Hiv1.
pose proof (deref_compat (SemanticsSpec.fail "") _ _ _ _ _ Hheap1 H0 H5).
destruct H2 as [? Hderef]. pose proof (Hderef (int_of_nat 0)).
cbn in H4. rewrite isNotEvaluated_vrel in H3; eauto.
+ eapply H4. lia.
+ destruct is_not_evaluated; inversion H3.
split; eauto. eapply H4. lia.
- cbn; specialize (IHeval1 _ _ Hloc Hheap). destruct interpret as [ih1 iv1]; destruct IHeval1 as [Hheap1 Hiv1].
inversion Hiv1; subst; clear Hiv1.
pose proof (deref_compat (SemanticsSpec.fail "") _ _ _ _ _ Hheap1 H0 H7).
destruct H6 as [? Hderef]. pose proof (Hderef (int_of_nat 0)).
cbn in H8. rewrite isNotEvaluated_vrel in H2; [eapply H8; lia|].
destruct is_not_evaluated; inversion H2. clear H2.
rewrite H1 in Hderef.
specialize (Hderef (int_of_nat 1) (ltac:(eauto))).
rewrite H3 in Hderef. cbn in Hderef. set _.[1] in ×.
inversion Hderef. subst. rewrite <- H11 in Hderef.
specialize (IHeval2 _ _ H9 Hheap1).
destruct interpret as [ih2 iv2]; destruct IHeval2 as [Hheap2 Hiv2].
split; eauto.
eapply update_compat with (default := SemanticsSpec.fail ""); eauto. split; cbn.
× rewrite PArray.length_set. lia.
× intro i. pose proof (int_of_to_nat i). destruct (int_to_nat i); [| destruct n].
+ subst. intros _. rewrite get_set_same; eauto.
rewrite <- (int_of_to_nat (PArray.length _)). rewrite <- H6.
rewrite H1. cbn; lia.
+ subst; intros _. rewrite get_set_other; [now apply eqb_false_spec|]. cbn.
rewrite -/y. rewrite <- H11. econstructor; eauto.
+ lia.
- fail_case IHeval Hloc Hheap H0.
- cbn. split; eauto.
- cbn [interpret]; split; eauto; econstructor.
- cbn [interpret]; split; eauto; econstructor.
- cbn [interpret]; split; eauto; econstructor.
- cbn [interpret]. pose proof (fresh_compat _ _ _ _ Hheap H0).
set (Interpreter.fresh ih) in ×. destruct p.
destruct H2; split; [| now econstructor].
eapply update_compat with (default := SemanticsSpec.fail ""); eauto.
apply Forall2Array_init; eauto.
intros k Hk. pose (int_to_of_nat k).
unfold int_to_nat in e. rewrite e; [lia_max_length| econstructor].
- cbn [interpret]; destruct op; cbn [interpret];
specialize (IHeval _ _ Hloc Hheap); destruct interpret as [ih1 iv1]; destruct IHeval as [Hheap1 Hiv1];
split; eauto; erewrite <- as_ty_vrel; eauto; eapply truncate_vrel.
- cbn [interpret]; destruct op; cbn [interpret];
specialize (IHeval1 _ _ Hloc Hheap); destruct interpret as [ih1 iv1]; destruct IHeval1 as [Hheap1 Hiv1];
specialize (IHeval2 _ _ Hloc Hheap1); destruct interpret as [ih2 iv2]; destruct IHeval2 as [Hheap2 Hiv2];
split; eauto.
1-2: destruct b; repeat erewrite <- (@as_ty_vrel P P'); eauto; eapply truncate_vrel.
destruct b; repeat erewrite <- (@as_ty_vrel P P'); eauto; econstructor.
- cbn [interpret].
specialize (IHeval _ _ Hloc Hheap); destruct interpret as [ih1 iv1]; destruct IHeval as [Hheap1 Hiv1].
split; eauto; erewrite as_float_vrel; eauto; econstructor.
- cbn [interpret]; split; eauto; econstructor.
- cbn [interpret]; split; eauto; econstructor.
- cbn [interpret]; destruct op; cbn [interpret];
specialize (IHeval1 _ _ Hloc Hheap); destruct interpret as [ih1 iv1]; destruct IHeval1 as [Hheap1 Hiv1];
specialize (IHeval2 _ _ Hloc Hheap1); destruct interpret as [ih2 iv2]; destruct IHeval2 as [Hheap2 Hiv2];
split; eauto;cbn; repeat erewrite <- (@as_float_vrel P P'); eauto; econstructor.
- cbn [interpret]; destruct op; cbn [interpret];
specialize (IHeval1 _ _ Hloc Hheap); destruct interpret as [ih1 iv1]; destruct IHeval1 as [Hheap1 Hiv1];
specialize (IHeval2 _ _ Hloc Hheap1); destruct interpret as [ih2 iv2]; destruct IHeval2 as [Hheap2 Hiv2];
split; eauto;cbn; repeat erewrite <- (@as_float_vrel P P'); eauto; econstructor.
- cbn [interpret].
specialize (IHeval _ _ Hloc Hheap); destruct interpret as [ih1 iv1]; destruct IHeval as [Hheap1 Hiv1].
split; eauto. erewrite <- (@as_ty_vrel P P'); eauto; eapply truncate_vrel.
- cbn [interpret].
specialize (IHeval _ _ Hloc Hheap); destruct interpret as [ih1 iv1]; destruct IHeval as [Hheap1 Hiv1].
split; eauto. erewrite <- (@as_ty_vrel P P'); eauto; econstructor.
- cbn [interpret].
specialize (IHeval _ _ Hloc Hheap); destruct interpret as [ih1 iv1]; destruct IHeval as [Hheap1 Hiv1].
split; eauto. erewrite <- (@as_float_vrel P P'); eauto; econstructor.
- cbn [interpret];
specialize (IHeval1 _ _ Hloc Hheap); destruct interpret as [ih1 iv1]; destruct IHeval1 as [Hheap1 Hiv1];
specialize (IHeval2 _ _ Hloc Hheap1); destruct interpret as [ih2 iv2]; destruct IHeval2 as [Hheap2 Hiv2];
inversion Hiv1; subst; clear Hiv1.
pose proof (fresh_compat _ _ _ _ Hheap2 H3).
set (Interpreter.fresh ih2) in ×. destruct p.
destruct H5; split; [| now econstructor].
eapply update_compat with (default := SemanticsSpec.fail ""); eauto.
assert (Hlen' : Int63.of_Z len' = int_of_nat (Z.to_nat len')).
{ unfold int_of_nat. rewrite Z2Nat.id; eauto. }
rewrite Hlen'. apply (Forall2Array_cst _ (Z.to_nat len') _ iv2); eauto.
- cbn [interpret];
specialize (IHeval1 _ _ Hloc Hheap); destruct interpret as [ih1 iv1]; destruct IHeval1 as [Hheap1 Hiv1];
specialize (IHeval2 _ _ Hloc Hheap1); destruct interpret as [ih2 iv2]; destruct IHeval2 as [Hheap2 Hiv2];
inversion Hiv1; subst; clear Hiv1.
inversion Hiv2; subst; clear Hiv2. rewrite H3.
pose proof (fresh_compat _ _ _ _ Hheap2 H4).
set (Interpreter.fresh ih2) in ×. destruct p.
destruct H6; split; [| now econstructor].
eapply update_compat with (default := SemanticsSpec.fail ""); eauto.
unfold List.init. unfold Forall2Array.
assert (Hlen' : Int63.of_Z len' = int_of_nat (Z.to_nat len')).
{ unfold int_of_nat. rewrite Z2Nat.id; eauto. }
rewrite Hlen'. apply Forall2Array_cst; eauto.
econstructor.
- cbn [interpret];
specialize (IHeval1 _ _ Hloc Hheap); destruct interpret as [ih1 iv1]; destruct IHeval1 as [Hheap1 Hiv1];
specialize (IHeval2 _ _ Hloc Hheap1); destruct interpret as [ih2 iv2]; destruct IHeval2 as [Hheap2 Hiv2];
inversion Hiv1; subst; clear Hiv1.
split; eauto.
pose proof (deref_compat (SemanticsSpec.fail "") _ _ _ _ _ Hheap H1 H5).
destruct H2 as [? Hderef].
case (vector_type_eqb ty ty').
2: {
destruct idx'; destruct iv2; try (destruct p as [i0 ?]; destruct i0);
try (destruct p0 as [i1 ?]; destruct i1); try econstructor. }
destruct idx'; destruct iv2;
try (destruct p as [i0 n]; destruct i0);
try (destruct p0 as [i1 n']; destruct i1); try econstructor;
try inversion Hiv2. subst.
pose proof (leb_length _ (deref ih ptr')).
case_eq ((0 <=? n')%Z); intro; simpl; try econstructor.
case_eq (n' <? Z.of_nat (Datatypes.length arr))%Z;
case_eq (n' <? φ (PArray.length (deref ih ptr'))%uint63)%Z; intros.
+ assert (Hn': (0 ≤ n' < Int63.wB)%Z).
{split; [lia|]. clear -H3 H4 H6.
apply leb_spec in H3. apply Z.ltb_lt in H6.
set (PArray.length _) in ×. clearbody i.
clear H4. lia_max_length. }
assert (Heqn' : Z.to_nat n' = int_to_nat (Int63.of_Z n')).
{ unfold int_to_nat. f_equal. rewrite Int63.of_Z_spec.
rewrite Z.mod_small; eauto. }
rewrite Heqn'. apply Hderef. unfold int_to_nat. rewrite Int63.of_Z_spec.
rewrite Z.mod_small; eauto. apply Z.ltb_lt in H7.
lia.
+ rewrite H2 in H7. unfold int_to_nat in H7.
rewrite Z2Nat.id in H7. apply to_Z_bounded.
rewrite H7 in H6. inversion H6.
+ rewrite H2 in H7. unfold int_to_nat in H7.
rewrite Z2Nat.id in H7. apply to_Z_bounded.
rewrite H7 in H6. inversion H6.
+ econstructor.
- cbn [interpret]; specialize (IHeval1 _ _ Hloc Hheap). destruct interpret as [ih1 iv1]; destruct IHeval1 as [Hheap1 Hiv1].
specialize (IHeval2 _ _ Hloc Hheap1).
destruct interpret as [ih2 iv2]; destruct IHeval2 as [Hheap2 Hiv2].
inversion Hiv1 ; subst. inversion Hiv2 ; subst. specialize (IHeval3 _ _ Hloc Hheap2).
destruct interpret as [ih3 iv3]. destruct IHeval3 as [Hheap3 Hiv3].
case_eq (vector_type_eqb ty ty'); [| repeat econstructor; eauto].
pose proof (deref_compat (SemanticsSpec.fail "") _ _ _ _ _ Hheap H2 H7).
destruct H4 as [Hsize Hderef].
rewrite Hsize. unfold int_to_nat. rewrite Z2Nat.id.
pose (to_Z_bounded (PArray.length (deref ih ptr'))); lia.
intro Htyty'.
case_eq (Z.leb 0 i && (Z.ltb i (Int63.to_Z (PArray.length (deref ih ptr')))))%bool;
[| repeat econstructor; eauto].
rename i into z. intro Harr. apply MRProd.andb_and in Harr.
destruct Harr as [Hz0 Harr]. apply Z.leb_le in Hz0.
apply Z.ltb_lt in Harr.
pose proof (Hmax := leb_length _ (deref ih ptr')).
apply leb_spec in Hmax.
destruct ty.
+ split; [| econstructor; eauto].
eapply update_compat with (default := SemanticsSpec.fail ""); eauto.
split. now rewrite List.length_set PArray.length_set.
intros i Hi. set (arr' := deref _ _) in ×. clearbody arr'.
case_eq (i =? Int63.of_Z z)%uint63.
× intro eq; apply eqb_correct in eq. subst.
unfold int_to_nat. rewrite Int63.of_Z_spec Z.mod_small;
[ lia_max_length |].
rewrite get_set_same; eauto.
apply ltb_spec.
rewrite Int63.of_Z_spec Z.mod_small; lia_max_length.
pose (Hnth := List.nth_set_same). rewrite Hnth; eauto.
rewrite Hsize. unfold int_to_nat. apply Z2Nat.inj_lt; cbn in *; lia.
× rewrite eqb_false_spec. intro Hneq. rewrite get_set_other; eauto.
rewrite List.nth_set_other. intro Hneq'; apply Hneq.
assert (int_of_nat (Z.to_nat z) = int_of_nat (int_to_nat i)) by now f_equal.
rewrite int_of_to_nat in H4. unfold int_of_nat in H4.
rewrite Z2Nat.id in H4; [lia | eauto].
eapply Hderef. now rewrite List.length_set in Hi.
+ destruct iv3; inversion Hiv3; try repeat econstructor; eauto.
destruct ty; try repeat econstructor; eauto.
case_eq ((0 <=? i)%Z && (i <? 256)%Z)%bool; try repeat econstructor; eauto.
eapply update_compat with (default := SemanticsSpec.fail ""); eauto.
split. now rewrite List.length_set PArray.length_set. rename i into z'.
intros i Hi. set (arr' := deref _ _) in ×. clearbody arr'.
case_eq (i =? Int63.of_Z z)%uint63.
× intro eq; apply eqb_correct in eq. subst.
unfold int_to_nat. rewrite Int63.of_Z_spec Z.mod_small; [lia_max_length |].
rewrite get_set_same; eauto.
apply ltb_spec. rewrite Int63.of_Z_spec Z.mod_small; lia_max_length.
pose (Hnth := List.nth_set_same). rewrite Hnth; eauto.
rewrite Hsize. unfold int_to_nat. apply Z2Nat.inj_lt; cbn in *; lia.
× rewrite eqb_false_spec. intro Hneq. rewrite get_set_other; eauto.
rewrite List.nth_set_other. intro Hneq'; apply Hneq.
assert (int_of_nat (Z.to_nat z) = int_of_nat (int_to_nat i)) by now f_equal.
rewrite int_of_to_nat in H8. unfold int_of_nat in H8.
rewrite Z2Nat.id in H8; [lia | eauto].
eapply Hderef. now rewrite List.length_set in Hi.
- cbn [interpret].
specialize (IHeval _ _ Hloc Hheap); destruct interpret as [ih1 iv1]; destruct IHeval as [Hheap1 Hiv1].
split; eauto. inversion Hiv1; subst.
destruct (vector_type_eqb ty ty'); try econstructor.
pose proof (deref_compat (SemanticsSpec.fail "") _ _ _ _ _ Hheap H0 H4).
destruct H1 as [Hsize Hderef]. rewrite Hsize.
unfold int_to_nat. rewrite Z2Nat.id.
pose (to_Z_bounded (PArray.length (deref ih ptr'))); lia.
econstructor.
Qed.
Set Guard Checking.