Theory "alignment"

Signature

Definitions

byte_aligned_def

⊢ ∀w. byte_aligned w ⇔ aligned (LOG2 (dimindex (:α) DIV 8)) w

byte_align_def

⊢ ∀w. byte_align w = align (LOG2 (dimindex (:α) DIV 8)) w

aligned_def

⊢ ∀p w. aligned p w ⇔ (align p w = w)

align_def

⊢ ∀p w. align p w = (dimindex (:α) − 1 '' p) w

Theorems

word_msb_align

⊢ p < dimindex (:α) ⇒ (word_msb (align p w) ⇔ word_msb w)

pow2_eq_0

⊢ dimindex (:α) ≤ k ⇒ (n2w (2 ** k) = 0w)

MOD_0_aligned

⊢ ∀n p. (n MOD 2 ** p = 0) ⇒ aligned p (n2w n)

lt_align_eq_0

⊢ w2n a < 2 ** p ⇒ (align p a = 0w)

byte_aligned_add

⊢ byte_aligned x ∧ byte_aligned y ⇒ byte_aligned (x + y)

byte_align_aligned

⊢ byte_aligned x ⇔ (byte_align x = x)

aligned_w2n

⊢ aligned k w ⇔ (w2n w MOD 2 ** k = 0)

aligned_pow2

⊢ aligned k (n2w (2 ** k))

aligned_or

⊢ aligned n (w ‖ v) ⇔ aligned n w ∧ aligned n v

aligned_numeric

⊢ (∀x. aligned 3 (n2w (NUMERAL (BIT2 (BIT1 (BIT1 x)))))) ∧
  (∀x. aligned 2 (n2w (NUMERAL (BIT2 (BIT1 x))))) ∧
  (∀x. aligned 1 (n2w (NUMERAL (BIT2 x)))) ∧
  (∀x. aligned 3 (-n2w (NUMERAL (BIT2 (BIT1 (BIT1 x)))))) ∧
  (∀x. aligned 2 (-n2w (NUMERAL (BIT2 (BIT1 x))))) ∧
  (∀x. aligned 1 (-n2w (NUMERAL (BIT2 x)))) ∧
  (∀x y f.
       aligned 3 (y + n2w (NUMERAL (BIT1 (BIT1 (BIT1 (f x)))))) ⇔
       aligned 3 (y + 7w)) ∧
  (∀x y f.
       aligned 3 (y + n2w (NUMERAL (BIT1 (BIT1 (BIT2 x))))) ⇔
       aligned 3 (y + 3w)) ∧
  (∀x y f.
       aligned 3 (y + n2w (NUMERAL (BIT1 (BIT2 (BIT1 x))))) ⇔
       aligned 3 (y + 1w)) ∧
  (∀x y f.
       aligned 3 (y + n2w (NUMERAL (BIT1 (BIT2 (BIT2 x))))) ⇔
       aligned 3 (y + 5w)) ∧
  (∀x y f. aligned 3 (y + n2w (NUMERAL (BIT2 (BIT1 (BIT1 x))))) ⇔ aligned 3 y) ∧
  (∀x y f.
       aligned 3 (y + n2w (NUMERAL (BIT2 (BIT1 (BIT2 x))))) ⇔
       aligned 3 (y + 4w)) ∧
  (∀x y f.
       aligned 3 (y + n2w (NUMERAL (BIT2 (BIT2 (BIT1 x))))) ⇔
       aligned 3 (y + 2w)) ∧
  (∀x y f.
       aligned 3 (y + n2w (NUMERAL (BIT2 (BIT2 (BIT2 x))))) ⇔
       aligned 3 (y + 6w)) ∧
  (∀x y f.
       aligned 3 (y − n2w (NUMERAL (BIT1 (BIT1 (BIT1 (f x)))))) ⇔
       aligned 3 (y − 7w)) ∧
  (∀x y f.
       aligned 3 (y − n2w (NUMERAL (BIT1 (BIT1 (BIT2 x))))) ⇔
       aligned 3 (y − 3w)) ∧
  (∀x y f.
       aligned 3 (y − n2w (NUMERAL (BIT1 (BIT2 (BIT1 x))))) ⇔
       aligned 3 (y − 1w)) ∧
  (∀x y f.
       aligned 3 (y − n2w (NUMERAL (BIT1 (BIT2 (BIT2 x))))) ⇔
       aligned 3 (y − 5w)) ∧
  (∀x y f. aligned 3 (y − n2w (NUMERAL (BIT2 (BIT1 (BIT1 x))))) ⇔ aligned 3 y) ∧
  (∀x y f.
       aligned 3 (y − n2w (NUMERAL (BIT2 (BIT1 (BIT2 x))))) ⇔
       aligned 3 (y − 4w)) ∧
  (∀x y f.
       aligned 3 (y − n2w (NUMERAL (BIT2 (BIT2 (BIT1 x))))) ⇔
       aligned 3 (y − 2w)) ∧
  (∀x y f.
       aligned 3 (y − n2w (NUMERAL (BIT2 (BIT2 (BIT2 x))))) ⇔
       aligned 3 (y − 6w)) ∧
  (∀x y f.
       aligned 2 (y + n2w (NUMERAL (BIT1 (BIT1 (f x))))) ⇔ aligned 2 (y + 3w)) ∧
  (∀x y. aligned 2 (y + n2w (NUMERAL (BIT1 (BIT2 x)))) ⇔ aligned 2 (y + 1w)) ∧
  (∀x y. aligned 2 (y + n2w (NUMERAL (BIT2 (BIT1 x)))) ⇔ aligned 2 y) ∧
  (∀x y. aligned 2 (y + n2w (NUMERAL (BIT2 (BIT2 x)))) ⇔ aligned 2 (y + 2w)) ∧
  (∀x y f.
       aligned 2 (y − n2w (NUMERAL (BIT1 (BIT1 (f x))))) ⇔ aligned 2 (y − 3w)) ∧
  (∀x y. aligned 2 (y − n2w (NUMERAL (BIT1 (BIT2 x)))) ⇔ aligned 2 (y − 1w)) ∧
  (∀x y. aligned 2 (y − n2w (NUMERAL (BIT2 (BIT1 x)))) ⇔ aligned 2 y) ∧
  (∀x y. aligned 2 (y − n2w (NUMERAL (BIT2 (BIT2 x)))) ⇔ aligned 2 (y − 2w)) ∧
  (∀x y f. aligned 1 (y + n2w (NUMERAL (BIT1 (f x)))) ⇔ aligned 1 (y + 1w)) ∧
  (∀x y f. aligned 1 (y − n2w (NUMERAL (BIT1 (f x)))) ⇔ aligned 1 (y − 1w)) ∧
  (∀x y. aligned 1 (y + n2w (NUMERAL (BIT2 x))) ⇔ aligned 1 y) ∧
  ∀x y. aligned 1 (y − n2w (NUMERAL (BIT2 x))) ⇔ aligned 1 y

aligned_mul_shift_1

⊢ ∀p w. aligned p (1w ≪ p * w)

aligned_lsl_leq

⊢ k ≤ l ⇒ aligned k (w ≪ l)

aligned_lsl

⊢ aligned k (w ≪ k)

aligned_imp

⊢ ∀p q w. p < q ∧ aligned q w ⇒ aligned p w

aligned_ge_dim

⊢ ∀p w. dimindex (:α) ≤ p ⇒ (aligned p w ⇔ (w = 0w))

aligned_extract

⊢ ∀p w. aligned p w ⇔ (p = 0) ∨ ((p − 1 >< 0) w = 0w)

aligned_bitwise_and

⊢ ∀p w. aligned p w ⇔ (w && n2w (2 ** p − 1) = 0w)

aligned_bit_count_upto

⊢ ∀p w. aligned p w ⇔ (bit_count_upto (MIN (dimindex (:α)) p) w = 0)

aligned_between

⊢ ¬aligned p n ∧ aligned p m ∧ align p n <₊ m ⇒ n <₊ m

aligned_align

⊢ ∀p w. aligned p (align p w)

aligned_add_sub_prod

⊢ ∀p w x.
      (aligned p (w + 1w ≪ p * x) ⇔ aligned p w) ∧
      (aligned p (w − 1w ≪ p * x) ⇔ aligned p w)

aligned_add_sub_cor

⊢ ∀p a b. aligned p a ∧ aligned p b ⇒ aligned p (a + b) ∧ aligned p (a − b)

aligned_add_sub_123

⊢ (∀w x.
       (aligned 1 (w + 2w * x) ⇔ aligned 1 w) ∧
       (aligned 1 (w − 2w * x) ⇔ aligned 1 w)) ∧
  (∀x. aligned 1 (2w * x) ∧ aligned 1 (-2w * x)) ∧
  (∀w x.
       (aligned 2 (w + 4w * x) ⇔ aligned 2 w) ∧
       (aligned 2 (w − 4w * x) ⇔ aligned 2 w)) ∧
  (∀x. aligned 2 (4w * x) ∧ aligned 2 (-4w * x)) ∧
  (∀w x.
       (aligned 3 (w + 8w * x) ⇔ aligned 3 w) ∧
       (aligned 3 (w − 8w * x) ⇔ aligned 3 w)) ∧
  ∀x. aligned 3 (8w * x) ∧ aligned 3 (-8w * x)

aligned_add_sub

⊢ ∀p a b.
      aligned p b ⇒
      (aligned p (a + b) ⇔ aligned p a) ∧ (aligned p (a − b) ⇔ aligned p a)

aligned_add_pow

⊢ (∀w k. aligned k (w + n2w (2 ** k)) ⇔ aligned k w) ∧
  ∀k n w. aligned k (w + n2w (n * 2 ** k)) ⇔ aligned k w

aligned_1_lsb

⊢ ∀w. aligned 1 w ⇔ ¬word_lsb w

aligned_0

⊢ (∀p. aligned p 0w) ∧ ∀w. aligned 0 w

align_w2n

⊢ ∀p w. align p w = n2w (w2n w DIV 2 ** p * 2 ** p)

align_sub

⊢ ∀p w. align p w = if p = 0 then w else w − (p − 1 >< 0) w

align_shift

⊢ ∀p w. align p w = w ⋙ p ≪ p

align_ls

⊢ align p n ≤₊ n

align_lo

⊢ ¬aligned p n ⇒ align p n <₊ n

align_bitwise_and

⊢ ∀p w. align p w = w && UINT_MAXw ≪ p

align_aligned

⊢ ∀p w. aligned p w ⇒ (align p w = w)

align_align_MAX

⊢ ∀k l w. align k (align l w) = align (MAX k l) w

align_align

⊢ ∀p w. align p (align p w) = align p w

align_add_aligned_gen

⊢ ∀a. aligned p a ⇒ (align p (a + b) = a + align p b)

align_add_aligned

⊢ ∀p a b. aligned p a ∧ w2n b < 2 ** p ⇒ (align p (a + b) = a)

align_0

⊢ ∀w. align 0 w = w