Commit 7e1d0c7c authored by Léon Gondelman's avatar Léon Gondelman

Fixed dbin_op_eval and proved it correctness.

parent 98ced4a7
......@@ -118,9 +118,10 @@ Section vcg.
match dv1,dv2 with
| dValUnknown _, _ | _,dValUnknown _ =>
dUnknown (dValUnknown <$> bin_op_eval op (dval_interp E dv1) (dval_interp E dv2))
| dLitV l1,dLitV l2 =>
| dLitV l1, dLitV l2 =>
if decide (op = EqOp)
then dSome $ dLitV $ dLitBool $ bool_decide (l1 = l2)
then dSome $ dLitV $ dLitBool
$ bool_decide (dbase_lit_interp E l1 = dbase_lit_interp E l2)
else match l1, l2 with
| (dLitInt n1), (dLitInt n2) =>
dSome $ dLitV $ dbin_op_eval_int op n1 n2
......@@ -139,11 +140,26 @@ Section vcg.
destruct dv1 as [dl1 | v1].
- destruct dv2 as [dl2 | v2].
+ unfold bin_op_eval. simpl. case_decide; simplify_eq/=.
{ inversion 1. rewrite /bin_op_eval /=. admit. }
{ admit. }
+ simpl. destruct (bin_op_eval op #(dbase_lit_interp E dl1) v2); try by inversion 1.
- simpl. destruct (bin_op_eval op v1 (dval_interp E dv2)); try by inversion 1.
Admitted.
{ inversion 1. rewrite /bin_op_eval /=. f_equal. simplify_eq /=.
do 2 case_bool_decide; simplify_eq /=; eauto. destruct H1. done. }
{ rewrite /bin_op_eval; intros; destruct dl1, dl2;
rewrite /bin_op_eval_int /bin_op_eval_bool; simplify_eq /=; f_equal;
try (destruct op; done); simpl.
- rewrite /bin_op_eval in H1; case_decide; first done.
destruct b; simplify_eq /=; f_equal.
- destruct op; simplify_eq /=; try done.
- case_decide; first done. destruct b0; simplify_eq /=; f_equal.
destruct op; simplify_eq /=; try done.
- case_decide; first done. destruct b; simplify_eq /=; f_equal.
- case_decide; first done; destruct b; simplify_eq /=; f_equal;
destruct op; simplify_eq /=; try done.
- case_decide; first done; destruct b; simplify_eq /=; f_equal.
- case_decide; first done; destruct b; simplify_eq /=; f_equal.
- case_decide; first done; destruct b,b0; simplify_eq /=; f_equal.
destruct op; simplify_eq /=; try done. }
+ simpl; destruct (bin_op_eval op #(dbase_lit_interp E dl1) v2); try by inversion 1.
- simpl; destruct (bin_op_eval op v1 (dval_interp E dv2)); try by inversion 1.
Qed.
Fixpoint wp_interp (E : list loc) (a : wp_expr) : iProp Σ :=
match a with
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment