Theory "alignment"

Signature

Definitions

align_def

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

aligned_def

|- ∀p w. aligned p w ⇔ (align p w = w)

byte_align_def

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

byte_aligned_def

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

Theorems

align_0

|- ∀w. align 0 w = w

align_align

|- ∀p w. align p (align p w) = align p w

aligned_align

|- ∀p w. aligned p (align p w)

align_aligned

|- ∀p w. aligned p w ⇒ (align p w = w)

align_bitwise_and

|- ∀p w. align p w = w && UINT_MAXw ≪ p

align_shift

|- ∀p w. align p w = w ⋙ p ≪ p

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

aligned_extract

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

aligned_0

|- (∀p. aligned p 0w) ∧ ∀w. aligned 0 w

aligned_1_lsb

|- ∀w. aligned 1 w ⇔ ¬word_lsb w

aligned_ge_dim

|- ∀p w. dimindex (:α) ≤ p ⇒ (aligned p w ⇔ (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_add_sub

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

aligned_add_sub_cor

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

aligned_mul_shift_1

|- ∀p w. aligned p (1w ≪ 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_imp

|- ∀p q w. p < q ∧ aligned q w ⇒ aligned p w

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_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