Theory "blast"

Signature

Definitions

bcarry_def

⊢ ∀x y c. bcarry x y c ⇔ x ∧ y ∨ (x ∨ y) ∧ c

BCARRY_def

⊢ (∀x y c. BCARRY 0 x y c ⇔ c) ∧
  ∀i x y c. BCARRY (SUC i) x y c ⇔ bcarry (x i) (y i) (BCARRY i x y c)

bsum_def

⊢ ∀x y c. bsum x y c ⇔ ((x ⇔ ¬y) ⇔ ¬c)

BSUM_def

⊢ ∀i x y c. BSUM i x y c ⇔ bsum (x i) (y i) (BCARRY i x y c)

Theorems

BCARRY_def_compute

⊢ (∀x y c. BCARRY 0 x y c ⇔ c) ∧
  (∀i x y c.
       BCARRY (NUMERAL (BIT1 i)) x y c ⇔
       bcarry (x (NUMERAL (BIT1 i) − 1)) (y (NUMERAL (BIT1 i) − 1))
         (BCARRY (NUMERAL (BIT1 i) − 1) x y c)) ∧
  ∀i x y c.
      BCARRY (NUMERAL (BIT2 i)) x y c ⇔
      bcarry (x (NUMERAL (BIT1 i))) (y (NUMERAL (BIT1 i)))
        (BCARRY (NUMERAL (BIT1 i)) x y c)

BCARRY_LEM

⊢ ∀i x y c.
      0 < i ⇒
      (BCARRY i (λi. BIT i x) (λi. BIT i y) c ⇔
       BIT i (BITS (i − 1) 0 x + BITS (i − 1) 0 y + if c then 1 else 0))

BCARRY_EQ

⊢ ∀n c x1 x2 y1 y2.
      (∀i. i < n ⇒ (x1 i ⇔ x2 i) ∧ (y1 i ⇔ y2 i)) ⇒
      (BCARRY n x1 y1 c ⇔ BCARRY n x2 y2 c)

BSUM_EQ

⊢ ∀n c x1 x2 y1 y2.
      (∀i. i ≤ n ⇒ (x1 i ⇔ x2 i) ∧ (y1 i ⇔ y2 i)) ⇒
      (BSUM n x1 y1 c ⇔ BSUM n x2 y2 c)

BSUM_LEM

⊢ ∀i x y c.
      BSUM i (λi. BIT i x) (λi. BIT i y) c ⇔
      BIT i (x + y + if c then 1 else 0)

BITWISE_ADD

⊢ ∀x y. x + y = FCP i. BSUM i ($' x) ($' y) F

BITWISE_SUB

⊢ ∀x y. x − y = FCP i. BSUM i ($' x) ($~ ∘ $' y) T

BITWISE_LO

⊢ ∀x y. x <₊ y ⇔ ¬BCARRY (dimindex (:α)) ($' x) ($~ ∘ $' y) T

BITWISE_MUL

⊢ ∀w m.
      w * m =
      FOLDL (λa j. a + FCP i. w ' j ∧ j ≤ i ∧ m ' (i − j)) 0w
        (COUNT_LIST (dimindex (:α)))

word_lsl_bv_expand

⊢ ∀w m.
      w <<~ m = if dimindex (:α) = 1 then $FCP (K (¬m ' 0 ∧ w ' 0))
      else
        FCP k.
            FOLDL
              (λa j.
                   a ∨
                   (LOG2 (dimindex (:α) − 1) -- 0) m = n2w j ∧ j ≤ k ∧
                   w ' (k − j)) F (COUNT_LIST (dimindex (:α))) ∧
            (dimindex (:α) − 1 -- LOG2 (dimindex (:α) − 1) + 1) m = 0w

word_lsr_bv_expand

⊢ ∀w m.
      w >>>~ m = if dimindex (:α) = 1 then $FCP (K (¬m ' 0 ∧ w ' 0))
      else
        FCP k.
            FOLDL
              (λa j.
                   a ∨
                   (LOG2 (dimindex (:α) − 1) -- 0) m = n2w j ∧
                   k + j < dimindex (:α) ∧ w ' (k + j)) F
              (COUNT_LIST (dimindex (:α))) ∧
            (dimindex (:α) − 1 -- LOG2 (dimindex (:α) − 1) + 1) m = 0w

word_asr_bv_expand

⊢ ∀w m.
      w >>~ m = if dimindex (:α) = 1 then $FCP (K (w ' 0))
      else
        FCP k.
            FOLDL
              (λa j.
                   a ∨ (LOG2 (dimindex (:α) − 1) -- 0) m = n2w j ∧ (w ≫ j) ' k)
              F (COUNT_LIST (dimindex (:α))) ∧
            (dimindex (:α) − 1 -- LOG2 (dimindex (:α) − 1) + 1) m = 0w ∨
            n2w (dimindex (:α) − 1) <₊ m ∧ w ' (dimindex (:α) − 1)

word_ror_bv_expand

⊢ ∀w m.
      w #>>~ m =
      FCP k.
          FOLDL
            (λa j.
                 a ∨
                 word_mod m (n2w (dimindex (:α))) = n2w j ∧
                 w ' ((j + k) MOD dimindex (:α))) F
            (COUNT_LIST (dimindex (:α)))

word_rol_bv_expand

⊢ ∀w m.
      w #<<~ m =
      FCP k.
          FOLDL
            (λa j.
                 a ∨
                 word_mod m (n2w (dimindex (:α))) = n2w j ∧
                 w '
                 ((k + (dimindex (:α) − j) MOD dimindex (:α)) MOD
                  dimindex (:α))) F (COUNT_LIST (dimindex (:α)))