Require Import VST.floyd.proofauto.
Require Import VST.progs.cast_test.

Instance CompSpecs : compspecs.
(* Goal: compspecs *)
Proof. make_compspecs prog. Defined.

Local Open Scope logic.

Definition test_spec :=
 DECLARE _test
  WITH n: Z
  PRE [ _n OF tlong ]
        PROP  (0 <= n < Int.max_signed)
        LOCAL (temp _n (Vlong (Int64.repr n)))
        SEP   ()
  POST [ tuchar ]
        PROP ()
        LOCAL(temp ret_temp (Vint (Int.repr 0)))
        SEP ().

Definition Vprog : varspecs := nil.

Definition Gprog : funspecs := ltac:(with_library prog [test_spec]).

Lemma body_test:  semax_body Vprog Gprog f_test test_spec.
Proof.
(* Goal: semax_body Vprog Gprog CompSpecs f_test test_spec *)
start_function.
(* i64 n, b, c;  u8 d *)
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _d (Vint (Int.zero_ext (Zpos (xO (xO (xO xH)))) (Int.repr (Int64.unsigned (Int64.and (Int64.repr (Int.unsigned (Int.zero_ext (Zpos (xO (xO (xO xH)))) (Int.repr (Int64.unsigned (Int64.and (Int64.shl (Int64.sub (Int64.repr (Int.signed (Int.repr (Zpos (xO (xO xH)))))) (Int64.sub (Int64.mul (Int64.repr (Int.signed (Int.repr (Zpos (xO xH))))) (Int64.repr n)) (Int64.repr (Int.signed (Int.repr (Zpos (xO (xO xH)))))))) (Int64.repr (Int.unsigned (Int.repr (Zpos (xO (xO (xO xH)))))))) (Int64.repr (Int.signed (Int.repr (Zpos (xI (xI (xI (xI (xI (xI (xI xH))))))))))))))))) (Int64.shr (Int64.add (Int64.repr (Int.signed (Int.neg (Int.repr (Zpos (xO (xO xH))))))) (Int64.add (Int64.mul (Int64.repr n) (Int64.repr (Int.signed (Int.repr (Zpos (xO xH)))))) (Int64.repr (Int.signed (Int.repr (Zpos (xO (xO xH)))))))) (Int64.repr (Int.unsigned (Int.repr (Zpos (xO (xO (xO xH)))))))))))))) (@cons localdef (temp _c (Vlong (Int64.shl (Int64.sub (Int64.repr (Int.signed (Int.repr (Zpos (xO (xO xH)))))) (Int64.sub (Int64.mul (Int64.repr (Int.signed (Int.repr (Zpos (xO xH))))) (Int64.repr n)) (Int64.repr (Int.signed (Int.repr (Zpos (xO (xO xH)))))))) (Int64.repr (Int.unsigned (Int.repr (Zpos (xO (xO (xO xH)))))))))) (@cons localdef (temp _b (Vlong (Int64.shr (Int64.add (Int64.repr (Int.signed (Int.neg (Int.repr (Zpos (xO (xO xH))))))) (Int64.add (Int64.mul (Int64.repr n) (Int64.repr (Int.signed (Int.repr (Zpos (xO xH)))))) (Int64.repr (Int.signed (Int.repr (Zpos (xO (xO xH)))))))) (Int64.repr (Int.unsigned (Int.repr (Zpos (xO (xO (xO xH)))))))))) (@cons localdef (temp _n (Vlong (Int64.repr n))) (@nil localdef))))) (SEPx (@nil mpred)))) (Sreturn (@Some expr (Etempvar _d tuchar))) POSTCONDITION *)
forward.  (* b = n * 2; *)
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _d (Vint (Int.zero_ext (Zpos (xO (xO (xO xH)))) (Int.repr (Int64.unsigned (Int64.and (Int64.repr (Int.unsigned (Int.zero_ext (Zpos (xO (xO (xO xH)))) (Int.repr (Int64.unsigned (Int64.and (Int64.shl (Int64.sub (Int64.repr (Int.signed (Int.repr (Zpos (xO (xO xH)))))) (Int64.sub (Int64.mul (Int64.repr (Int.signed (Int.repr (Zpos (xO xH))))) (Int64.repr n)) (Int64.repr (Int.signed (Int.repr (Zpos (xO (xO xH)))))))) (Int64.repr (Int.unsigned (Int.repr (Zpos (xO (xO (xO xH)))))))) (Int64.repr (Int.signed (Int.repr (Zpos (xI (xI (xI (xI (xI (xI (xI xH))))))))))))))))) (Int64.shr (Int64.add (Int64.repr (Int.signed (Int.neg (Int.repr (Zpos (xO (xO xH))))))) (Int64.add (Int64.mul (Int64.repr n) (Int64.repr (Int.signed (Int.repr (Zpos (xO xH)))))) (Int64.repr (Int.signed (Int.repr (Zpos (xO (xO xH)))))))) (Int64.repr (Int.unsigned (Int.repr (Zpos (xO (xO (xO xH)))))))))))))) (@cons localdef (temp _c (Vlong (Int64.shl (Int64.sub (Int64.repr (Int.signed (Int.repr (Zpos (xO (xO xH)))))) (Int64.sub (Int64.mul (Int64.repr (Int.signed (Int.repr (Zpos (xO xH))))) (Int64.repr n)) (Int64.repr (Int.signed (Int.repr (Zpos (xO (xO xH)))))))) (Int64.repr (Int.unsigned (Int.repr (Zpos (xO (xO (xO xH)))))))))) (@cons localdef (temp _b (Vlong (Int64.shr (Int64.add (Int64.repr (Int.signed (Int.neg (Int.repr (Zpos (xO (xO xH))))))) (Int64.add (Int64.mul (Int64.repr n) (Int64.repr (Int.signed (Int.repr (Zpos (xO xH)))))) (Int64.repr (Int.signed (Int.repr (Zpos (xO (xO xH)))))))) (Int64.repr (Int.unsigned (Int.repr (Zpos (xO (xO (xO xH)))))))))) (@cons localdef (temp _n (Vlong (Int64.repr n))) (@nil localdef))))) (SEPx (@nil mpred)))) (Sreturn (@Some expr (Etempvar _d tuchar))) POSTCONDITION *)
forward.  (*  c = 2 * n; *)
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _d (Vint (Int.zero_ext (Zpos (xO (xO (xO xH)))) (Int.repr (Int64.unsigned (Int64.and (Int64.repr (Int.unsigned (Int.zero_ext (Zpos (xO (xO (xO xH)))) (Int.repr (Int64.unsigned (Int64.and (Int64.shl (Int64.sub (Int64.repr (Int.signed (Int.repr (Zpos (xO (xO xH)))))) (Int64.sub (Int64.mul (Int64.repr (Int.signed (Int.repr (Zpos (xO xH))))) (Int64.repr n)) (Int64.repr (Int.signed (Int.repr (Zpos (xO (xO xH)))))))) (Int64.repr (Int.unsigned (Int.repr (Zpos (xO (xO (xO xH)))))))) (Int64.repr (Int.signed (Int.repr (Zpos (xI (xI (xI (xI (xI (xI (xI xH))))))))))))))))) (Int64.shr (Int64.add (Int64.repr (Int.signed (Int.neg (Int.repr (Zpos (xO (xO xH))))))) (Int64.add (Int64.mul (Int64.repr n) (Int64.repr (Int.signed (Int.repr (Zpos (xO xH)))))) (Int64.repr (Int.signed (Int.repr (Zpos (xO (xO xH)))))))) (Int64.repr (Int.unsigned (Int.repr (Zpos (xO (xO (xO xH)))))))))))))) (@cons localdef (temp _c (Vlong (Int64.shl (Int64.sub (Int64.repr (Int.signed (Int.repr (Zpos (xO (xO xH)))))) (Int64.sub (Int64.mul (Int64.repr (Int.signed (Int.repr (Zpos (xO xH))))) (Int64.repr n)) (Int64.repr (Int.signed (Int.repr (Zpos (xO (xO xH)))))))) (Int64.repr (Int.unsigned (Int.repr (Zpos (xO (xO (xO xH)))))))))) (@cons localdef (temp _b (Vlong (Int64.shr (Int64.add (Int64.repr (Int.signed (Int.neg (Int.repr (Zpos (xO (xO xH))))))) (Int64.add (Int64.mul (Int64.repr n) (Int64.repr (Int.signed (Int.repr (Zpos (xO xH)))))) (Int64.repr (Int.signed (Int.repr (Zpos (xO (xO xH)))))))) (Int64.repr (Int.unsigned (Int.repr (Zpos (xO (xO (xO xH)))))))))) (@cons localdef (temp _n (Vlong (Int64.repr n))) (@nil localdef))))) (SEPx (@nil mpred)))) (Sreturn (@Some expr (Etempvar _d tuchar))) POSTCONDITION *)
forward.  (*  b = b + 4; *)
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _d (Vint (Int.zero_ext (Zpos (xO (xO (xO xH)))) (Int.repr (Int64.unsigned (Int64.and (Int64.repr (Int.unsigned (Int.zero_ext (Zpos (xO (xO (xO xH)))) (Int.repr (Int64.unsigned (Int64.and (Int64.shl (Int64.sub (Int64.repr (Int.signed (Int.repr (Zpos (xO (xO xH)))))) (Int64.sub (Int64.mul (Int64.repr (Int.signed (Int.repr (Zpos (xO xH))))) (Int64.repr n)) (Int64.repr (Int.signed (Int.repr (Zpos (xO (xO xH)))))))) (Int64.repr (Int.unsigned (Int.repr (Zpos (xO (xO (xO xH)))))))) (Int64.repr (Int.signed (Int.repr (Zpos (xI (xI (xI (xI (xI (xI (xI xH))))))))))))))))) (Int64.shr (Int64.add (Int64.repr (Int.signed (Int.neg (Int.repr (Zpos (xO (xO xH))))))) (Int64.add (Int64.mul (Int64.repr n) (Int64.repr (Int.signed (Int.repr (Zpos (xO xH)))))) (Int64.repr (Int.signed (Int.repr (Zpos (xO (xO xH)))))))) (Int64.repr (Int.unsigned (Int.repr (Zpos (xO (xO (xO xH)))))))))))))) (@cons localdef (temp _c (Vlong (Int64.shl (Int64.sub (Int64.repr (Int.signed (Int.repr (Zpos (xO (xO xH)))))) (Int64.sub (Int64.mul (Int64.repr (Int.signed (Int.repr (Zpos (xO xH))))) (Int64.repr n)) (Int64.repr (Int.signed (Int.repr (Zpos (xO (xO xH)))))))) (Int64.repr (Int.unsigned (Int.repr (Zpos (xO (xO (xO xH)))))))))) (@cons localdef (temp _b (Vlong (Int64.shr (Int64.add (Int64.repr (Int.signed (Int.neg (Int.repr (Zpos (xO (xO xH))))))) (Int64.add (Int64.mul (Int64.repr n) (Int64.repr (Int.signed (Int.repr (Zpos (xO xH)))))) (Int64.repr (Int.signed (Int.repr (Zpos (xO (xO xH)))))))) (Int64.repr (Int.unsigned (Int.repr (Zpos (xO (xO (xO xH)))))))))) (@cons localdef (temp _n (Vlong (Int64.repr n))) (@nil localdef))))) (SEPx (@nil mpred)))) (Sreturn (@Some expr (Etempvar _d tuchar))) POSTCONDITION *)
forward.  (*  b = (-4) + b; *)
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _d (Vint (Int.zero_ext (Zpos (xO (xO (xO xH)))) (Int.repr (Int64.unsigned (Int64.and (Int64.repr (Int.unsigned (Int.zero_ext (Zpos (xO (xO (xO xH)))) (Int.repr (Int64.unsigned (Int64.and (Int64.shl (Int64.sub (Int64.repr (Int.signed (Int.repr (Zpos (xO (xO xH)))))) (Int64.sub (Int64.mul (Int64.repr (Int.signed (Int.repr (Zpos (xO xH))))) (Int64.repr n)) (Int64.repr (Int.signed (Int.repr (Zpos (xO (xO xH)))))))) (Int64.repr (Int.unsigned (Int.repr (Zpos (xO (xO (xO xH)))))))) (Int64.repr (Int.signed (Int.repr (Zpos (xI (xI (xI (xI (xI (xI (xI xH))))))))))))))))) (Int64.shr (Int64.add (Int64.repr (Int.signed (Int.neg (Int.repr (Zpos (xO (xO xH))))))) (Int64.add (Int64.mul (Int64.repr n) (Int64.repr (Int.signed (Int.repr (Zpos (xO xH)))))) (Int64.repr (Int.signed (Int.repr (Zpos (xO (xO xH)))))))) (Int64.repr (Int.unsigned (Int.repr (Zpos (xO (xO (xO xH)))))))))))))) (@cons localdef (temp _c (Vlong (Int64.shl (Int64.sub (Int64.repr (Int.signed (Int.repr (Zpos (xO (xO xH)))))) (Int64.sub (Int64.mul (Int64.repr (Int.signed (Int.repr (Zpos (xO xH))))) (Int64.repr n)) (Int64.repr (Int.signed (Int.repr (Zpos (xO (xO xH)))))))) (Int64.repr (Int.unsigned (Int.repr (Zpos (xO (xO (xO xH)))))))))) (@cons localdef (temp _b (Vlong (Int64.shr (Int64.add (Int64.repr (Int.signed (Int.neg (Int.repr (Zpos (xO (xO xH))))))) (Int64.add (Int64.mul (Int64.repr n) (Int64.repr (Int.signed (Int.repr (Zpos (xO xH)))))) (Int64.repr (Int.signed (Int.repr (Zpos (xO (xO xH)))))))) (Int64.repr (Int.unsigned (Int.repr (Zpos (xO (xO (xO xH)))))))))) (@cons localdef (temp _n (Vlong (Int64.repr n))) (@nil localdef))))) (SEPx (@nil mpred)))) (Sreturn (@Some expr (Etempvar _d tuchar))) POSTCONDITION *)
forward.  (*  c = c - 4; *)
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _d (Vint (Int.zero_ext (Zpos (xO (xO (xO xH)))) (Int.repr (Int64.unsigned (Int64.and (Int64.repr (Int.unsigned (Int.zero_ext (Zpos (xO (xO (xO xH)))) (Int.repr (Int64.unsigned (Int64.and (Int64.shl (Int64.sub (Int64.repr (Int.signed (Int.repr (Zpos (xO (xO xH)))))) (Int64.sub (Int64.mul (Int64.repr (Int.signed (Int.repr (Zpos (xO xH))))) (Int64.repr n)) (Int64.repr (Int.signed (Int.repr (Zpos (xO (xO xH)))))))) (Int64.repr (Int.unsigned (Int.repr (Zpos (xO (xO (xO xH)))))))) (Int64.repr (Int.signed (Int.repr (Zpos (xI (xI (xI (xI (xI (xI (xI xH))))))))))))))))) (Int64.shr (Int64.add (Int64.repr (Int.signed (Int.neg (Int.repr (Zpos (xO (xO xH))))))) (Int64.add (Int64.mul (Int64.repr n) (Int64.repr (Int.signed (Int.repr (Zpos (xO xH)))))) (Int64.repr (Int.signed (Int.repr (Zpos (xO (xO xH)))))))) (Int64.repr (Int.unsigned (Int.repr (Zpos (xO (xO (xO xH)))))))))))))) (@cons localdef (temp _c (Vlong (Int64.shl (Int64.sub (Int64.repr (Int.signed (Int.repr (Zpos (xO (xO xH)))))) (Int64.sub (Int64.mul (Int64.repr (Int.signed (Int.repr (Zpos (xO xH))))) (Int64.repr n)) (Int64.repr (Int.signed (Int.repr (Zpos (xO (xO xH)))))))) (Int64.repr (Int.unsigned (Int.repr (Zpos (xO (xO (xO xH)))))))))) (@cons localdef (temp _b (Vlong (Int64.shr (Int64.add (Int64.repr (Int.signed (Int.neg (Int.repr (Zpos (xO (xO xH))))))) (Int64.add (Int64.mul (Int64.repr n) (Int64.repr (Int.signed (Int.repr (Zpos (xO xH)))))) (Int64.repr (Int.signed (Int.repr (Zpos (xO (xO xH)))))))) (Int64.repr (Int.unsigned (Int.repr (Zpos (xO (xO (xO xH)))))))))) (@cons localdef (temp _n (Vlong (Int64.repr n))) (@nil localdef))))) (SEPx (@nil mpred)))) (Sreturn (@Some expr (Etempvar _d tuchar))) POSTCONDITION *)
forward.  (*  c = 4 - c; *)
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _d (Vint (Int.zero_ext (Zpos (xO (xO (xO xH)))) (Int.repr (Int64.unsigned (Int64.and (Int64.repr (Int.unsigned (Int.zero_ext (Zpos (xO (xO (xO xH)))) (Int.repr (Int64.unsigned (Int64.and (Int64.shl (Int64.sub (Int64.repr (Int.signed (Int.repr (Zpos (xO (xO xH)))))) (Int64.sub (Int64.mul (Int64.repr (Int.signed (Int.repr (Zpos (xO xH))))) (Int64.repr n)) (Int64.repr (Int.signed (Int.repr (Zpos (xO (xO xH)))))))) (Int64.repr (Int.unsigned (Int.repr (Zpos (xO (xO (xO xH)))))))) (Int64.repr (Int.signed (Int.repr (Zpos (xI (xI (xI (xI (xI (xI (xI xH))))))))))))))))) (Int64.shr (Int64.add (Int64.repr (Int.signed (Int.neg (Int.repr (Zpos (xO (xO xH))))))) (Int64.add (Int64.mul (Int64.repr n) (Int64.repr (Int.signed (Int.repr (Zpos (xO xH)))))) (Int64.repr (Int.signed (Int.repr (Zpos (xO (xO xH)))))))) (Int64.repr (Int.unsigned (Int.repr (Zpos (xO (xO (xO xH)))))))))))))) (@cons localdef (temp _c (Vlong (Int64.shl (Int64.sub (Int64.repr (Int.signed (Int.repr (Zpos (xO (xO xH)))))) (Int64.sub (Int64.mul (Int64.repr (Int.signed (Int.repr (Zpos (xO xH))))) (Int64.repr n)) (Int64.repr (Int.signed (Int.repr (Zpos (xO (xO xH)))))))) (Int64.repr (Int.unsigned (Int.repr (Zpos (xO (xO (xO xH)))))))))) (@cons localdef (temp _b (Vlong (Int64.shr (Int64.add (Int64.repr (Int.signed (Int.neg (Int.repr (Zpos (xO (xO xH))))))) (Int64.add (Int64.mul (Int64.repr n) (Int64.repr (Int.signed (Int.repr (Zpos (xO xH)))))) (Int64.repr (Int.signed (Int.repr (Zpos (xO (xO xH)))))))) (Int64.repr (Int.unsigned (Int.repr (Zpos (xO (xO (xO xH)))))))))) (@cons localdef (temp _n (Vlong (Int64.repr n))) (@nil localdef))))) (SEPx (@nil mpred)))) (Sreturn (@Some expr (Etempvar _d tuchar))) POSTCONDITION *)
forward.  (*  b = b >> 8; *)
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _d (Vint (Int.zero_ext (Zpos (xO (xO (xO xH)))) (Int.repr (Int64.unsigned (Int64.and (Int64.repr (Int.unsigned (Int.zero_ext (Zpos (xO (xO (xO xH)))) (Int.repr (Int64.unsigned (Int64.and (Int64.shl (Int64.sub (Int64.repr (Int.signed (Int.repr (Zpos (xO (xO xH)))))) (Int64.sub (Int64.mul (Int64.repr (Int.signed (Int.repr (Zpos (xO xH))))) (Int64.repr n)) (Int64.repr (Int.signed (Int.repr (Zpos (xO (xO xH)))))))) (Int64.repr (Int.unsigned (Int.repr (Zpos (xO (xO (xO xH)))))))) (Int64.repr (Int.signed (Int.repr (Zpos (xI (xI (xI (xI (xI (xI (xI xH))))))))))))))))) (Int64.shr (Int64.add (Int64.repr (Int.signed (Int.neg (Int.repr (Zpos (xO (xO xH))))))) (Int64.add (Int64.mul (Int64.repr n) (Int64.repr (Int.signed (Int.repr (Zpos (xO xH)))))) (Int64.repr (Int.signed (Int.repr (Zpos (xO (xO xH)))))))) (Int64.repr (Int.unsigned (Int.repr (Zpos (xO (xO (xO xH)))))))))))))) (@cons localdef (temp _c (Vlong (Int64.shl (Int64.sub (Int64.repr (Int.signed (Int.repr (Zpos (xO (xO xH)))))) (Int64.sub (Int64.mul (Int64.repr (Int.signed (Int.repr (Zpos (xO xH))))) (Int64.repr n)) (Int64.repr (Int.signed (Int.repr (Zpos (xO (xO xH)))))))) (Int64.repr (Int.unsigned (Int.repr (Zpos (xO (xO (xO xH)))))))))) (@cons localdef (temp _b (Vlong (Int64.shr (Int64.add (Int64.repr (Int.signed (Int.neg (Int.repr (Zpos (xO (xO xH))))))) (Int64.add (Int64.mul (Int64.repr n) (Int64.repr (Int.signed (Int.repr (Zpos (xO xH)))))) (Int64.repr (Int.signed (Int.repr (Zpos (xO (xO xH)))))))) (Int64.repr (Int.unsigned (Int.repr (Zpos (xO (xO (xO xH)))))))))) (@cons localdef (temp _n (Vlong (Int64.repr n))) (@nil localdef))))) (SEPx (@nil mpred)))) (Sreturn (@Some expr (Etempvar _d tuchar))) POSTCONDITION *)
forward.  (*  c = c << 8; *)
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _d (Vint (Int.zero_ext (Zpos (xO (xO (xO xH)))) (Int.repr (Int64.unsigned (Int64.and (Int64.repr (Int.unsigned (Int.zero_ext (Zpos (xO (xO (xO xH)))) (Int.repr (Int64.unsigned (Int64.and (Int64.shl (Int64.sub (Int64.repr (Int.signed (Int.repr (Zpos (xO (xO xH)))))) (Int64.sub (Int64.mul (Int64.repr (Int.signed (Int.repr (Zpos (xO xH))))) (Int64.repr n)) (Int64.repr (Int.signed (Int.repr (Zpos (xO (xO xH)))))))) (Int64.repr (Int.unsigned (Int.repr (Zpos (xO (xO (xO xH)))))))) (Int64.repr (Int.signed (Int.repr (Zpos (xI (xI (xI (xI (xI (xI (xI xH))))))))))))))))) (Int64.shr (Int64.add (Int64.repr (Int.signed (Int.neg (Int.repr (Zpos (xO (xO xH))))))) (Int64.add (Int64.mul (Int64.repr n) (Int64.repr (Int.signed (Int.repr (Zpos (xO xH)))))) (Int64.repr (Int.signed (Int.repr (Zpos (xO (xO xH)))))))) (Int64.repr (Int.unsigned (Int.repr (Zpos (xO (xO (xO xH)))))))))))))) (@cons localdef (temp _c (Vlong (Int64.shl (Int64.sub (Int64.repr (Int.signed (Int.repr (Zpos (xO (xO xH)))))) (Int64.sub (Int64.mul (Int64.repr (Int.signed (Int.repr (Zpos (xO xH))))) (Int64.repr n)) (Int64.repr (Int.signed (Int.repr (Zpos (xO (xO xH)))))))) (Int64.repr (Int.unsigned (Int.repr (Zpos (xO (xO (xO xH)))))))))) (@cons localdef (temp _b (Vlong (Int64.shr (Int64.add (Int64.repr (Int.signed (Int.neg (Int.repr (Zpos (xO (xO xH))))))) (Int64.add (Int64.mul (Int64.repr n) (Int64.repr (Int.signed (Int.repr (Zpos (xO xH)))))) (Int64.repr (Int.signed (Int.repr (Zpos (xO (xO xH)))))))) (Int64.repr (Int.unsigned (Int.repr (Zpos (xO (xO (xO xH)))))))))) (@cons localdef (temp _n (Vlong (Int64.repr n))) (@nil localdef))))) (SEPx (@nil mpred)))) (Sreturn (@Some expr (Etempvar _d tuchar))) POSTCONDITION *)
forward.  (*  d = c & 0xff; *)
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _d (Vint (Int.zero_ext (Zpos (xO (xO (xO xH)))) (Int.repr (Int64.unsigned (Int64.and (Int64.repr (Int.unsigned (Int.zero_ext (Zpos (xO (xO (xO xH)))) (Int.repr (Int64.unsigned (Int64.and (Int64.shl (Int64.sub (Int64.repr (Int.signed (Int.repr (Zpos (xO (xO xH)))))) (Int64.sub (Int64.mul (Int64.repr (Int.signed (Int.repr (Zpos (xO xH))))) (Int64.repr n)) (Int64.repr (Int.signed (Int.repr (Zpos (xO (xO xH)))))))) (Int64.repr (Int.unsigned (Int.repr (Zpos (xO (xO (xO xH)))))))) (Int64.repr (Int.signed (Int.repr (Zpos (xI (xI (xI (xI (xI (xI (xI xH))))))))))))))))) (Int64.shr (Int64.add (Int64.repr (Int.signed (Int.neg (Int.repr (Zpos (xO (xO xH))))))) (Int64.add (Int64.mul (Int64.repr n) (Int64.repr (Int.signed (Int.repr (Zpos (xO xH)))))) (Int64.repr (Int.signed (Int.repr (Zpos (xO (xO xH)))))))) (Int64.repr (Int.unsigned (Int.repr (Zpos (xO (xO (xO xH)))))))))))))) (@cons localdef (temp _c (Vlong (Int64.shl (Int64.sub (Int64.repr (Int.signed (Int.repr (Zpos (xO (xO xH)))))) (Int64.sub (Int64.mul (Int64.repr (Int.signed (Int.repr (Zpos (xO xH))))) (Int64.repr n)) (Int64.repr (Int.signed (Int.repr (Zpos (xO (xO xH)))))))) (Int64.repr (Int.unsigned (Int.repr (Zpos (xO (xO (xO xH)))))))))) (@cons localdef (temp _b (Vlong (Int64.shr (Int64.add (Int64.repr (Int.signed (Int.neg (Int.repr (Zpos (xO (xO xH))))))) (Int64.add (Int64.mul (Int64.repr n) (Int64.repr (Int.signed (Int.repr (Zpos (xO xH)))))) (Int64.repr (Int.signed (Int.repr (Zpos (xO (xO xH)))))))) (Int64.repr (Int.unsigned (Int.repr (Zpos (xO (xO (xO xH)))))))))) (@cons localdef (temp _n (Vlong (Int64.repr n))) (@nil localdef))))) (SEPx (@nil mpred)))) (Sreturn (@Some expr (Etempvar _d tuchar))) POSTCONDITION *)
forward.  (*  d = d & b; *)
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _d (Vint (Int.zero_ext (Zpos (xO (xO (xO xH)))) (Int.repr (Int64.unsigned (Int64.and (Int64.repr (Int.unsigned (Int.zero_ext (Zpos (xO (xO (xO xH)))) (Int.repr (Int64.unsigned (Int64.and (Int64.shl (Int64.sub (Int64.repr (Int.signed (Int.repr (Zpos (xO (xO xH)))))) (Int64.sub (Int64.mul (Int64.repr (Int.signed (Int.repr (Zpos (xO xH))))) (Int64.repr n)) (Int64.repr (Int.signed (Int.repr (Zpos (xO (xO xH)))))))) (Int64.repr (Int.unsigned (Int.repr (Zpos (xO (xO (xO xH)))))))) (Int64.repr (Int.signed (Int.repr (Zpos (xI (xI (xI (xI (xI (xI (xI xH))))))))))))))))) (Int64.shr (Int64.add (Int64.repr (Int.signed (Int.neg (Int.repr (Zpos (xO (xO xH))))))) (Int64.add (Int64.mul (Int64.repr n) (Int64.repr (Int.signed (Int.repr (Zpos (xO xH)))))) (Int64.repr (Int.signed (Int.repr (Zpos (xO (xO xH)))))))) (Int64.repr (Int.unsigned (Int.repr (Zpos (xO (xO (xO xH)))))))))))))) (@cons localdef (temp _c (Vlong (Int64.shl (Int64.sub (Int64.repr (Int.signed (Int.repr (Zpos (xO (xO xH)))))) (Int64.sub (Int64.mul (Int64.repr (Int.signed (Int.repr (Zpos (xO xH))))) (Int64.repr n)) (Int64.repr (Int.signed (Int.repr (Zpos (xO (xO xH)))))))) (Int64.repr (Int.unsigned (Int.repr (Zpos (xO (xO (xO xH)))))))))) (@cons localdef (temp _b (Vlong (Int64.shr (Int64.add (Int64.repr (Int.signed (Int.neg (Int.repr (Zpos (xO (xO xH))))))) (Int64.add (Int64.mul (Int64.repr n) (Int64.repr (Int.signed (Int.repr (Zpos (xO xH)))))) (Int64.repr (Int.signed (Int.repr (Zpos (xO (xO xH)))))))) (Int64.repr (Int.unsigned (Int.repr (Zpos (xO (xO (xO xH)))))))))) (@cons localdef (temp _n (Vlong (Int64.repr n))) (@nil localdef))))) (SEPx (@nil mpred)))) (Sreturn (@Some expr (Etempvar _d tuchar))) POSTCONDITION *)
forward.  (* return d *)
(* Goal: @derives mpred Nveric (@emp mpred Nveric Sveric) (@prop mpred Nveric (@eq val (Vint (cast_int_int I8 Unsigned (Int.zero_ext (Zpos (xO (xO (xO xH)))) (Int.repr (Int64.unsigned (Int64.and (Int64.repr (Int.unsigned (Int.zero_ext (Zpos (xO (xO (xO xH)))) (Int.repr (Int64.unsigned (Int64.and (Int64.shl (Int64.repr (Z.sub (Zpos (xO (xO xH))) (Z.sub (Z.mul (Zpos (xO xH)) n) (Zpos (xO (xO xH)))))) (Int64.repr (Zpos (xO (xO (xO xH)))))) (Int64.repr (Zpos (xI (xI (xI (xI (xI (xI (xI xH))))))))))))))) (Int64.shr (Int64.repr (Z.add (Z.opp (Zpos (xO (xO xH)))) (Z.add (Z.mul n (Zpos (xO xH))) (Zpos (xO (xO xH)))))) (Int64.repr (Zpos (xO (xO (xO xH)))))))))))) (Vint (Int.repr Z0)))) *)
entailer!. clear.
(* Goal: @eq val (Vint (cast_int_int I8 Unsigned (Int.zero_ext (Zpos (xO (xO (xO xH)))) (Int.repr (Int64.unsigned (Int64.and (Int64.repr (Int.unsigned (Int.zero_ext (Zpos (xO (xO (xO xH)))) (Int.repr (Int64.unsigned (Int64.and (Int64.shl (Int64.repr (Z.sub (Zpos (xO (xO xH))) (Z.sub (Z.mul (Zpos (xO xH)) n) (Zpos (xO (xO xH)))))) (Int64.repr (Zpos (xO (xO (xO xH)))))) (Int64.repr (Zpos (xI (xI (xI (xI (xI (xI (xI xH))))))))))))))) (Int64.shr (Int64.repr (Z.add (Z.opp (Zpos (xO (xO xH)))) (Z.add (Z.mul n (Zpos (xO xH))) (Zpos (xO (xO xH)))))) (Int64.repr (Zpos (xO (xO (xO xH)))))))))))) (Vint (Int.repr Z0)) *)
rewrite <- Int64.mul_pow2 with (n:= Int64.repr 256) by reflexivity.
(* Goal: @eq val (Vint (cast_int_int I8 Unsigned (Int.zero_ext (Zpos (xO (xO (xO xH)))) (Int.repr (Int64.unsigned (Int64.and (Int64.repr (Int.unsigned (Int.zero_ext (Zpos (xO (xO (xO xH)))) (Int.repr (Int64.unsigned (Int64.and (Int64.mul (Int64.repr (Z.sub (Zpos (xO (xO xH))) (Z.sub (Z.mul (Zpos (xO xH)) n) (Zpos (xO (xO xH)))))) (Int64.repr (Zpos (xO (xO (xO (xO (xO (xO (xO (xO xH))))))))))) (Int64.repr (Zpos (xI (xI (xI (xI (xI (xI (xI xH))))))))))))))) (Int64.shr (Int64.repr (Z.add (Z.opp (Zpos (xO (xO xH)))) (Z.add (Z.mul n (Zpos (xO xH))) (Zpos (xO (xO xH)))))) (Int64.repr (Zpos (xO (xO (xO xH)))))))))))) (Vint (Int.repr Z0)) *)
normalize.
(* Goal: @eq val (Vint (cast_int_int I8 Unsigned (Int.zero_ext (Zpos (xO (xO (xO xH)))) (Int.repr (Int64.unsigned (Int64.and (Int64.repr (Int.unsigned (Int.zero_ext (Zpos (xO (xO (xO xH)))) (Int.repr (Int64.unsigned (Int64.repr (Z.land (Z.mul (Z.sub (Zpos (xO (xO xH))) (Z.sub (Z.mul (Zpos (xO xH)) n) (Zpos (xO (xO xH))))) (Zpos (xO (xO (xO (xO (xO (xO (xO (xO xH)))))))))) (Zpos (xI (xI (xI (xI (xI (xI (xI xH))))))))))))))) (Int64.shr (Int64.repr (Z.add (Z.opp (Zpos (xO (xO xH)))) (Z.add (Z.mul n (Zpos (xO xH))) (Zpos (xO (xO xH)))))) (Int64.repr (Zpos (xO (xO (xO xH)))))))))))) (Vint (Int.repr Z0)) *)
rewrite (Z.land_ones _ 8) by computable.
(* Goal: @eq val (Vint (cast_int_int I8 Unsigned (Int.zero_ext (Zpos (xO (xO (xO xH)))) (Int.repr (Int64.unsigned (Int64.and (Int64.repr (Int.unsigned (Int.zero_ext (Zpos (xO (xO (xO xH)))) (Int.repr (Int64.unsigned (Int64.repr (Z.modulo (Z.mul (Z.sub (Zpos (xO (xO xH))) (Z.sub (Z.mul (Zpos (xO xH)) n) (Zpos (xO (xO xH))))) (Zpos (xO (xO (xO (xO (xO (xO (xO (xO xH)))))))))) (Z.pow (Zpos (xO xH)) (Zpos (xO (xO (xO xH)))))))))))) (Int64.shr (Int64.repr (Z.add (Z.opp (Zpos (xO (xO xH)))) (Z.add (Z.mul n (Zpos (xO xH))) (Zpos (xO (xO xH)))))) (Int64.repr (Zpos (xO (xO (xO xH)))))))))))) (Vint (Int.repr Z0)) *)
rewrite Z_mod_mult.
(* Goal: @eq val (Vint (cast_int_int I8 Unsigned (Int.zero_ext (Zpos (xO (xO (xO xH)))) (Int.repr (Int64.unsigned (Int64.and (Int64.repr (Int.unsigned (Int.zero_ext (Zpos (xO (xO (xO xH)))) (Int.repr (Int64.unsigned (Int64.repr Z0)))))) (Int64.shr (Int64.repr (Z.add (Z.opp (Zpos (xO (xO xH)))) (Z.add (Z.mul n (Zpos (xO xH))) (Zpos (xO (xO xH)))))) (Int64.repr (Zpos (xO (xO (xO xH)))))))))))) (Vint (Int.repr Z0)) *)
reflexivity.
Qed.


