Theory "alignment"

Parents words

Signature

Constant	Type
align	:num -> α word -> α word
aligned	:num -> α word -> bool
byte_align	:α word -> α word
byte_aligned	:α word -> bool

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

align_add_aligned

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

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