(* This file is generated by Why3's Coq driver *) (* Beware! Only edit allowed sections below *) Require Import ZArith. Require Import Rbase. Parameter bv : Type. Parameter nth: bv -> Z -> bool. Parameter bvzero: bv. Axiom Nth_zero : forall (n:Z), ((0%Z <= n)%Z /\ (n < 32%Z)%Z) -> ((nth bvzero n) = false). Parameter bvone: bv. Axiom Nth_one : forall (n:Z), ((0%Z <= n)%Z /\ (n < 32%Z)%Z) -> ((nth bvone n) = true). Definition eq(v1:bv) (v2:bv): Prop := forall (n:Z), ((0%Z <= n)%Z /\ (n < 32%Z)%Z) -> ((nth v1 n) = (nth v2 n)). Axiom extensionality : forall (v1:bv) (v2:bv), (eq v1 v2) -> (v1 = v2). Parameter bw_and: bv -> bv -> bv. Axiom Nth_bw_and : forall (v1:bv) (v2:bv) (n:Z), ((0%Z <= n)%Z /\ (n < 32%Z)%Z) -> ((nth (bw_and v1 v2) n) = (andb (nth v1 n) (nth v2 n))). Parameter bw_or: bv -> bv -> bv. Axiom Nth_bw_or : forall (v1:bv) (v2:bv) (n:Z), ((0%Z <= n)%Z /\ (n < 32%Z)%Z) -> ((nth (bw_or v1 v2) n) = (orb (nth v1 n) (nth v2 n))). Parameter bw_xor: bv -> bv -> bv. Axiom Nth_bw_xor : forall (v1:bv) (v2:bv) (n:Z), ((0%Z <= n)%Z /\ (n < 32%Z)%Z) -> ((nth (bw_xor v1 v2) n) = (xorb (nth v1 n) (nth v2 n))). Parameter bw_not: bv -> bv. Axiom Nth_bw_not : forall (v:bv) (n:Z), ((0%Z <= n)%Z /\ (n < 32%Z)%Z) -> ((nth (bw_not v) n) = (negb (nth v n))). Parameter lsr: bv -> Z -> bv. Axiom lsr_nth_low : forall (b:bv) (n:Z) (s:Z), ((0%Z <= n)%Z /\ (n < 32%Z)%Z) -> ((0%Z <= s)%Z -> (((n + s)%Z < 32%Z)%Z -> ((nth (lsr b s) n) = (nth b (n + s)%Z)))). Axiom lsr_nth_high : forall (b:bv) (n:Z) (s:Z), ((0%Z <= n)%Z /\ (n < 32%Z)%Z) -> ((0%Z <= s)%Z -> ((32%Z <= (n + s)%Z)%Z -> ((nth (lsr b s) n) = false))). Parameter asr: bv -> Z -> bv. Axiom asr_nth_low : forall (b:bv) (n:Z) (s:Z), ((0%Z <= n)%Z /\ (n < 32%Z)%Z) -> ((0%Z <= s)%Z -> (((n + s)%Z < 32%Z)%Z -> ((nth (asr b s) n) = (nth b (n + s)%Z)))). Axiom asr_nth_high : forall (b:bv) (n:Z) (s:Z), ((0%Z <= n)%Z /\ (n < 32%Z)%Z) -> ((0%Z <= s)%Z -> ((32%Z <= (n + s)%Z)%Z -> ((nth (asr b s) n) = (nth b (32%Z - 1%Z)%Z)))). Parameter lsl: bv -> Z -> bv. Axiom lsl_nth_high : forall (b:bv) (n:Z) (s:Z), ((0%Z <= n)%Z /\ (n < 32%Z)%Z) -> ((0%Z <= s)%Z -> ((0%Z <= (n - s)%Z)%Z -> ((nth (lsl b s) n) = (nth b (n - s)%Z)))). Axiom lsl_nth_low : forall (b:bv) (n:Z) (s:Z), ((0%Z <= n)%Z /\ (n < 32%Z)%Z) -> ((0%Z <= s)%Z -> (((n - s)%Z < 0%Z)%Z -> ((nth (lsl b s) n) = false))). Parameter to_nat_aux: bv -> Z -> Z. Axiom to_nat_aux_zero : forall (b:bv) (i:Z), ((0%Z <= i)%Z /\ (i < 32%Z)%Z) -> (((nth b i) = false) -> ((to_nat_aux b i) = (2%Z * (to_nat_aux b (i + 1%Z)%Z))%Z)). Axiom to_nat_aux_one : forall (b:bv) (i:Z), ((0%Z <= i)%Z /\ (i < 32%Z)%Z) -> (((nth b i) = true) -> ((to_nat_aux b i) = (1%Z + (2%Z * (to_nat_aux b (i + 1%Z)%Z))%Z)%Z)). Axiom to_nat_aux_high : forall (b:bv) (i:Z), (32%Z <= i)%Z -> ((to_nat_aux b i) = 0%Z). Parameter to_int_aux: bv -> Z -> Z. Axiom to_int_aux_zero : forall (b:bv) (i:Z), ((0%Z <= i)%Z /\ (i < (32%Z - 1%Z)%Z)%Z) -> (((nth b i) = false) -> ((to_int_aux b i) = (2%Z * (to_int_aux b (i + 1%Z)%Z))%Z)). Axiom to_int_aux_one : forall (b:bv) (i:Z), ((0%Z <= i)%Z /\ (i < (32%Z - 1%Z)%Z)%Z) -> (((nth b i) = true) -> ((to_int_aux b i) = (1%Z + (2%Z * (to_int_aux b (i + 1%Z)%Z))%Z)%Z)). Axiom to_int_aux_pos : forall (b:bv), ((nth b (32%Z - 1%Z)%Z) = false) -> ((to_int_aux b (32%Z - 1%Z)%Z) = 0%Z). Axiom to_int_aux_neg : forall (b:bv), ((nth b (32%Z - 1%Z)%Z) = true) -> ((to_int_aux b (32%Z - 1%Z)%Z) = (-1%Z)%Z). (* YOU MAY EDIT THE CONTEXT BELOW *) (* DO NOT EDIT BELOW *) Theorem to_int_0x80000000 : ((to_int_aux (lsl bvone 31%Z) 0%Z) = (-2147483648%Z)%Z). (* YOU MAY EDIT THE PROOF BELOW *) rewrite to_int_aux_zero; auto with zarith. 2: rewrite lsl_nth_low; auto with zarith. rewrite to_int_aux_zero; auto with zarith. 2: rewrite lsl_nth_low; auto with zarith. rewrite to_int_aux_zero; auto with zarith. 2: rewrite lsl_nth_low; auto with zarith. rewrite to_int_aux_zero; auto with zarith. 2: rewrite lsl_nth_low; auto with zarith. rewrite to_int_aux_zero; auto with zarith. 2: rewrite lsl_nth_low; auto with zarith. rewrite to_int_aux_zero; auto with zarith. 2: rewrite lsl_nth_low; auto with zarith. rewrite to_int_aux_zero; auto with zarith. 2: rewrite lsl_nth_low; auto with zarith. rewrite to_int_aux_zero; auto with zarith. 2: rewrite lsl_nth_low; auto with zarith. rewrite to_int_aux_zero; auto with zarith. 2: rewrite lsl_nth_low; auto with zarith. rewrite to_int_aux_zero; auto with zarith. 2: rewrite lsl_nth_low; auto with zarith. rewrite to_int_aux_zero; auto with zarith. 2: rewrite lsl_nth_low; auto with zarith. rewrite to_int_aux_zero; auto with zarith. 2: rewrite lsl_nth_low; auto with zarith. rewrite to_int_aux_zero; auto with zarith. 2: rewrite lsl_nth_low; auto with zarith. rewrite to_int_aux_zero; auto with zarith. 2: rewrite lsl_nth_low; auto with zarith. rewrite to_int_aux_zero; auto with zarith. 2: rewrite lsl_nth_low; auto with zarith. rewrite to_int_aux_zero; auto with zarith. 2: rewrite lsl_nth_low; auto with zarith. rewrite to_int_aux_zero; auto with zarith. 2: rewrite lsl_nth_low; auto with zarith. rewrite to_int_aux_zero; auto with zarith. 2: rewrite lsl_nth_low; auto with zarith. rewrite to_int_aux_zero; auto with zarith. 2: rewrite lsl_nth_low; auto with zarith. rewrite to_int_aux_zero; auto with zarith. 2: rewrite lsl_nth_low; auto with zarith. rewrite to_int_aux_zero; auto with zarith. 2: rewrite lsl_nth_low; auto with zarith. rewrite to_int_aux_zero; auto with zarith. 2: rewrite lsl_nth_low; auto with zarith. rewrite to_int_aux_zero; auto with zarith. 2: rewrite lsl_nth_low; auto with zarith. rewrite to_int_aux_zero; auto with zarith. 2: rewrite lsl_nth_low; auto with zarith. rewrite to_int_aux_zero; auto with zarith. 2: rewrite lsl_nth_low; auto with zarith. rewrite to_int_aux_zero; auto with zarith. 2: rewrite lsl_nth_low; auto with zarith. rewrite to_int_aux_zero; auto with zarith. 2: rewrite lsl_nth_low; auto with zarith. rewrite to_int_aux_zero; auto with zarith. 2: rewrite lsl_nth_low; auto with zarith. rewrite to_int_aux_zero; auto with zarith. 2: rewrite lsl_nth_low; auto with zarith. rewrite to_int_aux_zero; auto with zarith. 2: rewrite lsl_nth_low; auto with zarith. rewrite to_int_aux_zero; auto with zarith. 2: rewrite lsl_nth_low; auto with zarith. rewrite to_int_aux_neg; auto with zarith. rewrite lsl_nth_high; auto with zarith. rewrite Nth_one; auto with zarith. Qed. (* DO NOT EDIT BELOW *)