From d4a1583666ec2f51319c1f8fb5156dd82df8ee2c Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Sun, 6 Nov 2016 00:36:00 -0400 Subject: Prove inversion principles for bounded words --- src/Reflection/Z/Interpretations.v | 160 ++++++++++++++++++++++++++++--------- 1 file changed, 122 insertions(+), 38 deletions(-) (limited to 'src/Reflection') diff --git a/src/Reflection/Z/Interpretations.v b/src/Reflection/Z/Interpretations.v index b5b4cb9d5..8371b3bef 100644 --- a/src/Reflection/Z/Interpretations.v +++ b/src/Reflection/Z/Interpretations.v @@ -257,50 +257,64 @@ Module ZBounds. := if ((0 <=? l) && (Z.log2 u Z -> Z -> Z -> bounds) (x y : t) + Definition t_map2 (f : bounds -> bounds -> bounds) (x y : t) := match x, y with - | Some (Build_bounds lx ux), Some (Build_bounds ly uy) - => match f lx ly ux uy with + | Some x, Some y + => match f x y with | Build_bounds l u => SmartBuildBounds l u end | _, _ => None end%Z. - - Definition add : t -> t -> t - := t_map2 (fun lx ly ux uy => {| lower := lx + ly ; upper := ux + uy |}). - Definition sub : t -> t -> t - := t_map2 (fun lx ly ux uy => {| lower := lx - uy ; upper := ux - ly |}). - Definition mul : t -> t -> t - := t_map2 (fun lx ly ux uy => {| lower := lx * ly ; upper := ux * uy |}). - Definition shl : t -> t -> t - := t_map2 (fun lx ly ux uy => {| lower := lx << ly ; upper := ux << uy |}). - Definition shr : t -> t -> t - := t_map2 (fun lx ly ux uy => {| lower := lx >> uy ; upper := ux >> ly |}). - Definition land : t -> t -> t - := t_map2 (fun lx ly ux uy => {| lower := 0 ; upper := Z.min ux uy |}). - Definition lor : t -> t -> t - := t_map2 (fun lx ly ux uy => {| lower := Z.max lx ly; - upper := 2^(Z.max (Z.log2 (ux+1)) (Z.log2 (uy+1))) - 1 |}). + Definition add' : bounds -> bounds -> bounds + := fun x y => let (lx, ux) := x in let (ly, uy) := y in {| lower := lx + ly ; upper := ux + uy |}. + Definition add : t -> t -> t := t_map2 add'. + Definition sub' : bounds -> bounds -> bounds + := fun x y => let (lx, ux) := x in let (ly, uy) := y in {| lower := lx - uy ; upper := ux - ly |}. + Definition sub : t -> t -> t := t_map2 sub'. + Definition mul' : bounds -> bounds -> bounds + := fun x y => let (lx, ux) := x in let (ly, uy) := y in {| lower := lx * ly ; upper := ux * uy |}. + Definition mul : t -> t -> t := t_map2 mul'. + Definition shl' : bounds -> bounds -> bounds + := fun x y => let (lx, ux) := x in let (ly, uy) := y in {| lower := lx << ly ; upper := ux << uy |}. + Definition shl : t -> t -> t := t_map2 shl'. + Definition shr' : bounds -> bounds -> bounds + := fun x y => let (lx, ux) := x in let (ly, uy) := y in {| lower := lx >> uy ; upper := ux >> ly |}. + Definition shr : t -> t -> t := t_map2 shr'. + Definition land' : bounds -> bounds -> bounds + := fun x y => let (lx, ux) := x in let (ly, uy) := y in {| lower := 0 ; upper := Z.min ux uy |}. + Definition land : t -> t -> t := t_map2 land'. + Definition lor' : bounds -> bounds -> bounds + := fun x y => let (lx, ux) := x in let (ly, uy) := y in + {| lower := Z.max lx ly; + upper := 2^(Z.max (Z.log2 (ux+1)) (Z.log2 (uy+1))) - 1 |}. + Definition lor : t -> t -> t := t_map2 lor'. + Definition neg' : bounds -> bounds -> bounds + := fun int_width v + => let (lint_width, uint_width) := int_width in + let (lb, ub) := v in + let might_be_one := ((lb <=? 1) && (1 <=? ub))%Z%bool in + let must_be_one := ((lb =? 1) && (ub =? 1))%Z%bool in + if must_be_one + then {| lower := Z.ones lint_width ; upper := Z.ones uint_width |} + else if might_be_one + then {| lower := 0 ; upper := Z.ones uint_width |} + else {| lower := 0 ; upper := 0 |}. Definition neg : t -> t -> t := fun int_width v => match int_width, v with - | Some (Build_bounds lint_width uint_width), Some (Build_bounds lb ub) + | Some (Build_bounds lint_width uint_width as int_width), Some (Build_bounds lb ub as v) => if ((0 <=? lint_width) && (uint_width <=? Word64.bit_width))%Z%bool - then Some (let might_be_one := ((lb <=? 1) && (1 <=? ub))%Z%bool in - let must_be_one := ((lb =? 1) && (ub =? 1))%Z%bool in - if must_be_one - then {| lower := Z.ones lint_width ; upper := Z.ones uint_width |} - else if might_be_one - then {| lower := 0 ; upper := Z.ones uint_width |} - else {| lower := 0 ; upper := 0 |}) + then Some (neg' int_width v) else None | _, _ => None end. - Definition cmovne (x y r1 r2 : t) : t - := t_map2 (fun lr1 lr2 ur1 ur2 => {| lower := Z.min lr1 lr2 ; upper := Z.max ur1 ur2 |}) r1 r2. - Definition cmovle (x y r1 r2 : t) : t - := t_map2 (fun lr1 lr2 ur1 ur2 => {| lower := Z.min lr1 lr2 ; upper := Z.max ur1 ur2 |}) r1 r2. + Definition cmovne' (r1 r2 : bounds) : bounds + := let (lr1, ur1) := r1 in let (lr2, ur2) := r2 in {| lower := Z.min lr1 lr2 ; upper := Z.max ur1 ur2 |}. + Definition cmovne (x y r1 r2 : t) : t := t_map2 cmovne' r1 r2. + Definition cmovle' (r1 r2 : bounds) : bounds + := let (lr1, ur1) := r1 in let (lr2, ur2) := r2 in {| lower := Z.min lr1 lr2 ; upper := Z.max ur1 ur2 |}. + Definition cmovle (x y r1 r2 : t) : t := t_map2 cmovle' r1 r2. Module Export Notations. Delimit Scope bounds_scope with bounds. @@ -355,6 +369,16 @@ Module BoundedWord64. Bind Scope bounded_word_scope with t. Local Coercion Z.of_nat : nat >-> Z. + Ltac inversion_BoundedWord := + repeat match goal with + | _ => progress subst + | [ H : _ = _ :> BoundedWord |- _ ] + => pose proof (f_equal lower H); + pose proof (f_equal upper H); + pose proof (f_equal value H); + clear H + end. + Definition interp_base_type (ty : base_type) := LiftOption.interp_base_type' BoundedWord ty. @@ -425,7 +449,11 @@ Module BoundedWord64. | _, _ => None end); try unfold bounds_op; try unfold word_op; - cbv [ZBounds.t_map2 BoundedWordToBounds ZBounds.SmartBuildBounds ModularBaseSystemListZOperations.neg]. + repeat match goal with + | [ |- appcontext[ZBounds.t_map2 ?op] ] => unfold op + | [ |- appcontext[?op (ZBounds.Build_bounds _ _) (ZBounds.Build_bounds _ _)] ] => unfold op + | _ => progress cbv [ZBounds.t_map2 BoundedWordToBounds ZBounds.SmartBuildBounds ModularBaseSystemListZOperations.neg] + end. Local Ltac build_4op word_op bounds_op := refine (fun x y z w : t @@ -446,7 +474,11 @@ Module BoundedWord64. | _, _, _, _ => None end); try unfold bounds_op; try unfold word_op; - cbv [ZBounds.t_map2 BoundedWordToBounds ZBounds.SmartBuildBounds cmovne cmovl]. + repeat match goal with + | [ |- appcontext[ZBounds.t_map2 ?op] ] => unfold op + | [ |- appcontext[?op (ZBounds.Build_bounds _ _) (ZBounds.Build_bounds _ _)] ] => unfold op + | _ => progress cbv [ZBounds.t_map2 BoundedWordToBounds ZBounds.SmartBuildBounds cmovne cmovl] + end. Axiom proof_admitted : False. Local Opaque Word64.bit_width. @@ -527,13 +559,65 @@ Module BoundedWord64. Definition cmovle : t -> t -> t -> t -> t. Proof. build_4op Word64.cmovle ZBounds.cmovle; abstract t_start. Defined. - Local Notation value_binop_correct op opW := - (forall x y v, op (Some x) (Some y) = Some v -> value v = opW (value x) (value y)) + Local Notation binop_correct op opW opB := + (forall x y v, op (Some x) (Some y) = Some v -> value v = opW (value x) (value y) + /\ BoundedWordToBounds v = opB (BoundedWordToBounds x) (BoundedWordToBounds y)) (only parsing). - Definition value_add : value_binop_correct add Word64.add. - Proof. - Admitted. + Local Notation op4_correct op opW opB := + (forall x y z w v, op (Some x) (Some y) (Some z) (Some w) = Some v + -> value v = opW (value x) (value y) (value z) (value w) + /\ BoundedWordToBounds v = opB (BoundedWordToBounds x) (BoundedWordToBounds y) (BoundedWordToBounds z) (BoundedWordToBounds w)) + (only parsing). + + Local Ltac convoy_destruct_in H := + match type of H with + | context G[match ?e with Some x => @?S x | None => ?N end eq_refl] + => let e' := fresh in + let H' := fresh in + pose e as e'; + pose (eq_refl : e = e') as H'; + let G' := context G[match e' with Some x => S x | None => N end H'] in + change G' in H; + clearbody H' e'; destruct e' + end. + Local Arguments ZBounds.SmartBuildBounds _ _ / . + Local Arguments BoundedWordToBounds _ / . + Local Ltac invert_t_step := + match goal with + | _ => progress intros + | [ |- ?x = ?x ] => reflexivity + | [ H : context[match _ with _ => _ end eq_refl] |- _ ] => convoy_destruct_in H + | _ => progress destruct_head' BoundedWord + | _ => progress destruct_head' ZBounds.bounds + | _ => progress inversion_option + | _ => progress ZBounds.inversion_bounds + | _ => progress inversion_BoundedWord + | _ => progress simpl in * + | _ => progress break_match_hyps + | [ |- _ /\ _ ] => split + end. + Local Ltac invert_t := repeat invert_t_step. + Definition invert_add : binop_correct add Word64.add ZBounds.add'. + Proof. invert_t. Qed. + Definition invert_sub : binop_correct sub Word64.sub ZBounds.sub'. + Proof. invert_t. Qed. + Definition invert_mul : binop_correct mul Word64.mul ZBounds.mul'. + Proof. invert_t. Qed. + Definition invert_shl : binop_correct shl Word64.shl ZBounds.shl'. + Proof. invert_t. Qed. + Definition invert_shr : binop_correct shr Word64.shr ZBounds.shr'. + Proof. invert_t. Qed. + Definition invert_land : binop_correct land Word64.land ZBounds.land'. + Proof. invert_t. Qed. + Definition invert_lor : binop_correct lor Word64.lor ZBounds.lor'. + Proof. invert_t. Qed. + Definition invert_neg : binop_correct neg Word64.neg ZBounds.neg'. + Proof. invert_t. Qed. + Definition invert_cmovne : op4_correct cmovne Word64.cmovne (fun _ _ => ZBounds.cmovne'). + Proof. invert_t. Qed. + Definition invert_cmovle : op4_correct cmovle Word64.cmovle (fun _ _ => ZBounds.cmovle'). + Proof. invert_t. Qed. Module Export Notations. Delimit Scope bounded_word_scope with bounded_word. -- cgit v1.2.3