Finish initial definition of bitvectors.

3 files changed, 109 insertions, 522 deletions

diff --git a/src/Helium/Data/BitVec.agda b/src/Helium/Data/BitVec.agda
deleted file mode 100644
index 3d409ca..0000000
--- a/src/Helium/Data/BitVec.agda
+++ /dev/null
@@ -1,104 +0,0 @@
-{-# OPTIONS --safe --without-K #-}
-
-module Helium.Data.BitVec where
-
-open import Algebra.Core
-open import Data.Bool as B using () renaming (Bool to Bit; false to 0#; true to 1#)
-open import Data.Fin hiding (_+_; _-_)
-open import Data.Fin.Properties using (toℕ-fromℕ)
-open import Data.Nat as N hiding (_+_)
-open import Data.Product
-open import Data.Vec hiding (map; replicate)
-open import Relation.Binary.PropositionalEquality using (cong)
-
-private
-  variable
-    l m n : ℕ
-
-infixr 6 _∧_ _+_ _-_
-infixr 5 _∨_ _xor_
-
-
--- Type
-
-BitVec : ℕ → Set
-BitVec = Vec Bit
-
-
--- Constants
-
-replicate : Bit → BitVec n
-replicate {zero}  b = []
-replicate {suc n} b = b ∷ replicate b
-
-zeroes : BitVec n
-zeroes = replicate 0#
-
-ones : BitVec n
-ones = replicate 1#
-
-one : BitVec (suc n)
-one {zero}  = 1# ∷ []
-one {suc n} = 0# ∷ one
-
-
--- Bitwise operations
-
-bitwise : Op₁ Bit → Op₁ (BitVec n)
-bitwise f [] = []
-bitwise f (x ∷ xs) = f x ∷ bitwise f xs
-
-bitwise₂ : Op₂ Bit → Op₂ (BitVec n)
-bitwise₂ _∙_ []       []       = []
-bitwise₂ _∙_ (x ∷ xs) (y ∷ ys) = x ∙ y ∷ bitwise₂ _∙_ xs ys
-
-not : BitVec n → BitVec n
-not = bitwise B.not
-
-_∧_ : BitVec n → BitVec n → BitVec n
-_∧_ = bitwise₂ B._∧_
-
-_∨_ : BitVec n → BitVec n → BitVec n
-_∨_ = bitwise₂ B._∨_
-
-_xor_ : BitVec n → BitVec n → BitVec n
-_xor_ = bitwise₂ B._xor_
-
-
--- Arithmetic operations
-
-add-carry : Bit → BitVec n → BitVec n → Bit
-add-carry c  []       []      = c
-add-carry c (x ∷ xs) (y ∷ ys) = add-carry c xs ys B.∧ (x B.xor y) B.xor (x B.∧ y)
-
-add-rem : Bit → BitVec n → BitVec n → BitVec n
-add-rem c []       []       = []
-add-rem c (x ∷ xs) (y ∷ ys) = (add-carry c xs ys B.xor x B.xor y) ∷ add-rem c xs ys
-
-add : Bit → BitVec n → BitVec n → BitVec (suc n)
-add c xs ys = add-carry c xs ys ∷ add-rem c xs ys
-
-_+_ : BitVec n → BitVec n → BitVec n
-xs + ys = add-rem 0# xs ys
-
-_-_ : BitVec n → BitVec n → BitVec n
-xs - ys = add-rem 1# xs (not ys)
-
-
--- Conversions
-
-bitToFin : Bit → Fin 2
-bitToFin 0# = zero
-bitToFin 1# = suc zero
-
-finToBit : Fin 2 → Bit
-finToBit zero       = 0#
-finToBit (suc zero) = 1#
-
-toFin : BitVec n → Fin (2 ^ n)
-toFin         []       = zero
-toFin         (b ∷ bs) = combine (bitToFin b) (toFin bs)
-
-fromFin : Fin (2 ^ n) → BitVec n
-fromFin {zero}  x = []
-fromFin {suc n} x = uncurry (_∷_) (map finToBit fromFin (remQuot (2 ^ n) x))
diff --git a/src/Helium/Data/BitVec/Properties.agda b/src/Helium/Data/BitVec/Properties.agda
deleted file mode 100644
index 8094f97..0000000
--- a/src/Helium/Data/BitVec/Properties.agda
+++ /dev/null
@@ -1,418 +0,0 @@
-{-# OPTIONS --safe --without-K #-}
-
-module Helium.Data.BitVec.Properties where
-
-import Algebra.Definitions as Algebra
-open import Data.Bool as B using () renaming (Bool to Bit; false to 0#; true to 1#)
-open import Data.Empty
-open import Data.Fin as F hiding (_+_; _<_; _≥_)
-open import Data.Fin.Properties as FP
-import Data.Bool.Properties as B
-open import Data.Nat as N hiding (_+_; _*_)
-import Data.Nat.Properties as NP
-open import Data.Product
-open import Data.Vec using ([]; _∷_)
-open import Data.Vec.Properties using (∷-injective; ∷-injectiveʳ)
-open import Function
-open import Helium.Data.BitVec
-open import Relation.Binary.PropositionalEquality as ≡
-
-private
-  variable
-    l m n : ℕ
-
-module A n = Algebra (_≡_ {A = BitVec n})
-  renaming ( _DistributesOverʳ_ to ₍_₎_DistributesOverʳ_
-           ; _DistributesOverˡ_ to ₍_₎_DistributesOverˡ_
-           ; _DistributesOver_ to ₍_₎_DistributesOver_
-           ; _IdempotentOn_ to ₍_₎_IdempotentOn_
-           ; _Absorbs_ to ₍_₎_Absorbs_
-           )
-
-
---- Bitwise operations
-
--- bitwise
-
-bitwise-injective : ∀ f → Injective _≡_ _≡_ f → Injective _≡_ _≡_ (bitwise {n} f)
-bitwise-injective f inj {[]}     {[]}     eq = refl
-bitwise-injective f inj {x ∷ xs} {y ∷ ys} eq = uncurry (cong₂ _∷_) (dmap inj (bitwise-injective f inj) (∷-injective eq))
-
-bitwise-idem : ∀ f → Algebra.IdempotentFun _≡_ f → A.IdempotentFun n (bitwise f)
-bitwise-idem f idem []       = refl
-bitwise-idem f idem (x ∷ xs) = cong₂ _∷_ (idem x) (bitwise-idem f idem xs)
-
-bitwise-involutive : ∀ f → Algebra.Involutive _≡_ f → A.Involutive n (bitwise f)
-bitwise-involutive f inv []       = refl
-bitwise-involutive f inv (x ∷ xs) = cong₂ _∷_ (inv x) (bitwise-involutive f inv xs)
-
--- bitwise₂
-
-bitwise₂-assoc : ∀ ∙ → Algebra.Associative _≡_ ∙ → A.Associative n (bitwise₂ ∙)
-bitwise₂-assoc ∙ assoc [] [] [] = refl
-bitwise₂-assoc ∙ assoc (x ∷ xs) (y ∷ ys) (z ∷ zs) = cong₂ _∷_ (assoc x y z) (bitwise₂-assoc ∙ assoc xs ys zs)
-
-bitwise₂-comm : ∀ ∙ → Algebra.Commutative _≡_ ∙ → A.Commutative n (bitwise₂ ∙)
-bitwise₂-comm ∙ comm [] [] = refl
-bitwise₂-comm ∙ comm (x ∷ xs) (y ∷ ys) = cong₂ _∷_ (comm x y) (bitwise₂-comm ∙ comm xs ys)
-
-bitwise₂-identityˡ : ∀ b ∙ → Algebra.LeftIdentity _≡_ b ∙ → A.LeftIdentity n (replicate b) (bitwise₂ ∙)
-bitwise₂-identityˡ b ∙ id [] = refl
-bitwise₂-identityˡ b ∙ id (x ∷ xs) = cong₂ _∷_ (id x) (bitwise₂-identityˡ b ∙ id xs)
-
-bitwise₂-identityʳ : ∀ b ∙ → Algebra.RightIdentity _≡_ b ∙ → A.RightIdentity n (replicate b) (bitwise₂ ∙)
-bitwise₂-identityʳ b ∙ id [] = refl
-bitwise₂-identityʳ b ∙ id (x ∷ xs) = cong₂ _∷_ (id x) (bitwise₂-identityʳ b ∙ id xs)
-
-bitwise₂-identity : ∀ b ∙ → Algebra.Identity _≡_ b ∙ → A.Identity n (replicate b) (bitwise₂ ∙)
-bitwise₂-identity b ∙ = dmap (bitwise₂-identityˡ b ∙) (bitwise₂-identityʳ b ∙)
-
-bitwise₂-zeroˡ : ∀ b ∙ → Algebra.LeftZero _≡_ b ∙ → A.LeftZero n (replicate b) (bitwise₂ ∙)
-bitwise₂-zeroˡ b ∙ z [] = refl
-bitwise₂-zeroˡ b ∙ z (x ∷ xs) = cong₂ _∷_ (z x) (bitwise₂-zeroˡ b ∙ z xs)
-
-bitwise₂-zeroʳ : ∀ b ∙ → Algebra.RightZero _≡_ b ∙ → A.RightZero n (replicate b) (bitwise₂ ∙)
-bitwise₂-zeroʳ b ∙ z [] = refl
-bitwise₂-zeroʳ b ∙ z (x ∷ xs) = cong₂ _∷_ (z x) (bitwise₂-zeroʳ b ∙ z xs)
-
-bitwise₂-zero : ∀ b ∙ → Algebra.Zero _≡_ b ∙ → A.Zero n (replicate b) (bitwise₂ ∙)
-bitwise₂-zero b ∙ = dmap (bitwise₂-zeroˡ b ∙) (bitwise₂-zeroʳ b ∙)
-
-bitwise₂-inverseˡ : ∀ b f ∙ → Algebra.LeftInverse _≡_ b f ∙ → A.LeftInverse n (replicate b) (bitwise f) (bitwise₂ ∙)
-bitwise₂-inverseˡ b f ∙ id [] = refl
-bitwise₂-inverseˡ b f ∙ id (x ∷ xs) = cong₂ _∷_ (id x) (bitwise₂-inverseˡ b f ∙ id xs)
-
-bitwise₂-inverseʳ : ∀ b f ∙ → Algebra.RightInverse _≡_ b f ∙ → A.RightInverse n (replicate b) (bitwise f) (bitwise₂ ∙)
-bitwise₂-inverseʳ b f ∙ id [] = refl
-bitwise₂-inverseʳ b f ∙ id (x ∷ xs) = cong₂ _∷_ (id x) (bitwise₂-inverseʳ b f ∙ id xs)
-
-bitwise₂-inverse : ∀ b f ∙ → Algebra.Inverse _≡_ b f ∙ → A.Inverse n (replicate b) (bitwise f) (bitwise₂ ∙)
-bitwise₂-inverse b f ∙ = dmap (bitwise₂-inverseˡ b f ∙) (bitwise₂-inverseʳ b f ∙)
-
-bitwise₂-conicalˡ : ∀ b ∙ → Algebra.LeftConical _≡_ b ∙ → A.LeftConical n (replicate b) (bitwise₂ ∙)
-bitwise₂-conicalˡ b ∙ conical [] [] eq = refl
-bitwise₂-conicalˡ b ∙ conical (x ∷ xs) (y ∷ ys) eq = uncurry (cong₂ _∷_) (dmap (conical x y) (bitwise₂-conicalˡ b ∙ conical xs ys) (∷-injective eq))
-
-bitwise₂-conicalʳ : ∀ b ∙ → Algebra.RightConical _≡_ b ∙ → A.RightConical n (replicate b) (bitwise₂ ∙)
-bitwise₂-conicalʳ b ∙ conical [] [] eq = refl
-bitwise₂-conicalʳ b ∙ conical (x ∷ xs) (y ∷ ys) eq = uncurry (cong₂ _∷_) (dmap (conical x y) (bitwise₂-conicalʳ b ∙ conical xs ys) (∷-injective eq))
-
-bitwise₂-conical : ∀ b ∙ → Algebra.Conical _≡_ b ∙ → A.Conical n (replicate b) (bitwise₂ ∙)
-bitwise₂-conical b ∙ = dmap (bitwise₂-conicalˡ b ∙) (bitwise₂-conicalʳ b ∙)
-
-bitwise₂-distribˡ : ∀ * ∙ → Algebra._DistributesOverˡ_ _≡_ * ∙ → A.₍ n ₎ (bitwise₂ *) DistributesOverˡ (bitwise₂ ∙)
-bitwise₂-distribˡ * ∙ distrib [] [] [] = refl
-bitwise₂-distribˡ * ∙ distrib (x ∷ xs) (y ∷ ys) (z ∷ zs) = cong₂ _∷_ (distrib x y z) (bitwise₂-distribˡ * ∙ distrib xs ys zs)
-
-bitwise₂-distribʳ : ∀ * ∙ → Algebra._DistributesOverʳ_ _≡_ * ∙ → A.₍ n ₎ (bitwise₂ *) DistributesOverʳ (bitwise₂ ∙)
-bitwise₂-distribʳ * ∙ distrib [] [] [] = refl
-bitwise₂-distribʳ * ∙ distrib (x ∷ xs) (y ∷ ys) (z ∷ zs) = cong₂ _∷_ (distrib x y z) (bitwise₂-distribʳ * ∙ distrib xs ys zs)
-
-bitwise₂-distrib : ∀ * ∙ → Algebra._DistributesOver_ _≡_ * ∙ → A.₍ n ₎ (bitwise₂ *) DistributesOver (bitwise₂ ∙)
-bitwise₂-distrib * ∙ = dmap (bitwise₂-distribˡ * ∙) (bitwise₂-distribʳ * ∙)
-
-bitwise₂-idemOn : ∀ ∙ b → Algebra._IdempotentOn_ _≡_ ∙ b → A.₍ n ₎ (bitwise₂ ∙) IdempotentOn (replicate b)
-bitwise₂-idemOn {zero}  ∙ b idem = refl
-bitwise₂-idemOn {suc n} ∙ b idem = cong₂ _∷_ idem (bitwise₂-idemOn ∙ b idem)
-
-bitwise₂-idem : ∀ ∙ → Algebra.Idempotent _≡_ ∙ → A.Idempotent n (bitwise₂ ∙)
-bitwise₂-idem ∙ idem [] = refl
-bitwise₂-idem ∙ idem (x ∷ xs) = cong₂ _∷_ (idem x) (bitwise₂-idem ∙ idem xs)
-
-bitwise₂-absorbs : ∀ * ∙ → Algebra._Absorbs_ _≡_ * ∙ → A.₍ n ₎ (bitwise₂ *) Absorbs (bitwise₂ ∙)
-bitwise₂-absorbs * ∙ absorbs [] [] = refl
-bitwise₂-absorbs * ∙ absorbs (x ∷ xs) (y ∷ ys) = cong₂ _∷_ (absorbs x y) (bitwise₂-absorbs * ∙ absorbs xs ys)
-
-bitwise₂-absorptive : ∀ * ∙ → Algebra.Absorptive _≡_ * ∙ → A.Absorptive n (bitwise₂ *) (bitwise₂ ∙)
-bitwise₂-absorptive * ∙ = dmap (bitwise₂-absorbs * ∙) (bitwise₂-absorbs ∙ *)
-
-bitwise₂-cancelˡ : ∀ ∙ → Algebra.LeftCancellative _≡_ ∙ → A.LeftCancellative n (bitwise₂ ∙)
-bitwise₂-cancelˡ ∙ cancel [] {[]} {[]} eq = refl
-bitwise₂-cancelˡ ∙ cancel (x ∷ xs) {y ∷ ys} {z ∷ zs} eq = uncurry (cong₂ _∷_) (dmap (cancel x) (bitwise₂-cancelˡ ∙ cancel xs) (∷-injective eq))
-
-bitwise₂-cancelʳ : ∀ ∙ → Algebra.RightCancellative _≡_ ∙ → A.RightCancellative n (bitwise₂ ∙)
-bitwise₂-cancelʳ ∙ cancel [] [] eq = refl
-bitwise₂-cancelʳ ∙ cancel {x ∷ xs} (y ∷ ys) (z ∷ zs) eq = uncurry (cong₂ _∷_) (dmap (cancel y z) (bitwise₂-cancelʳ ∙ cancel ys zs) (∷-injective eq))
-
-bitwise₂-cancel : ∀ ∙ → Algebra.Cancellative _≡_ ∙ → A.Cancellative n (bitwise₂ ∙)
-bitwise₂-cancel ∙ = dmap (bitwise₂-cancelˡ ∙) (bitwise₂-cancelʳ ∙)
-
-bitwise₂-interchangable : ∀ * ∙ → Algebra.Interchangable _≡_ * ∙ → A.Interchangable n (bitwise₂ *) (bitwise₂ ∙)
-bitwise₂-interchangable * ∙ inter [] [] [] [] = refl
-bitwise₂-interchangable * ∙ inter (x ∷ xs) (y ∷ ys) (z ∷ zs) (w ∷ ws) = cong₂ _∷_ (inter x y z w) (bitwise₂-interchangable * ∙ inter xs ys zs ws)
-
--- not
-
-not-involutive : A.Involutive n not
-not-involutive = bitwise-involutive B.not B.not-involutive
-
-not-injective : Injective _≡_ _≡_ (not {n})
-not-injective = bitwise-injective B.not B.not-injective
-
-not-0 : not {n} zeroes ≡ ones
-not-0 {zero}  = refl
-not-0 {suc n} = cong (1# ∷_) not-0
-
-not-1 : not {n} ones ≡ zeroes
-not-1 {zero}  = refl
-not-1 {suc n} = cong (0# ∷_) not-1
-
--- ∧
-
-∧-assoc : A.Associative n _∧_
-∧-assoc = bitwise₂-assoc B._∧_ B.∧-assoc
-
-∧-comm : A.Commutative n _∧_
-∧-comm = bitwise₂-comm B._∧_ B.∧-comm
-
-∧-identityˡ : A.LeftIdentity n ones _∧_
-∧-identityˡ = bitwise₂-identityˡ 1# B._∧_ B.∧-identityˡ
-
-∧-identityʳ : A.RightIdentity n ones _∧_
-∧-identityʳ = bitwise₂-identityʳ 1# B._∧_ B.∧-identityʳ
-
-∧-identity : A.Identity n ones _∧_
-∧-identity = ∧-identityˡ , ∧-identityʳ
-
-∧-zeroˡ : A.LeftZero n zeroes _∧_
-∧-zeroˡ = bitwise₂-zeroˡ 0# B._∧_ B.∧-zeroˡ
-
-∧-zeroʳ : A.RightZero n zeroes _∧_
-∧-zeroʳ = bitwise₂-zeroʳ 0# B._∧_ B.∧-zeroʳ
-
-∧-zero : A.Zero n zeroes _∧_
-∧-zero = ∧-zeroˡ , ∧-zeroʳ
-
-∧-inverseˡ : A.LeftInverse n zeroes not _∧_
-∧-inverseˡ = bitwise₂-inverseˡ 0# B.not B._∧_ B.∧-inverseˡ
-
-∧-inverseʳ : A.RightInverse n zeroes not _∧_
-∧-inverseʳ = bitwise₂-inverseʳ 0# B.not B._∧_ B.∧-inverseʳ
-
-∧-inverse : A.Inverse n zeroes not _∧_
-∧-inverse = ∧-inverseˡ , ∧-inverseʳ
-
-∧-conicalˡ : A.LeftConical n ones _∧_
-∧-conicalˡ = bitwise₂-conicalˡ 1# B._∧_ λ { 1# 1# eq → refl }
-
-∧-conicalʳ : A.RightConical n ones _∧_
-∧-conicalʳ = bitwise₂-conicalʳ 1# B._∧_ λ { 1# 1# eq → refl }
-
-∧-conical : A.Conical n ones _∧_
-∧-conical = ∧-conicalˡ , ∧-conicalʳ
-
-∧-idem : A.Idempotent n _∧_
-∧-idem = bitwise₂-idem B._∧_ B.∧-idem
-
--- ∨
-
-∨-assoc : A.Associative n _∨_
-∨-assoc = bitwise₂-assoc B._∨_ B.∨-assoc
-
-∨-comm : A.Commutative n _∨_
-∨-comm = bitwise₂-comm B._∨_ B.∨-comm
-
-∨-identityˡ : A.LeftIdentity n zeroes _∨_
-∨-identityˡ = bitwise₂-identityˡ 0# B._∨_ B.∨-identityˡ
-
-∨-identityʳ : A.RightIdentity n zeroes _∨_
-∨-identityʳ = bitwise₂-identityʳ 0# B._∨_ B.∨-identityʳ
-
-∨-identity : A.Identity n zeroes _∨_
-∨-identity = ∨-identityˡ , ∨-identityʳ
-
-∨-zeroˡ : A.LeftZero n ones _∨_
-∨-zeroˡ = bitwise₂-zeroˡ 1# B._∨_ B.∨-zeroˡ
-
-∨-zeroʳ : A.RightZero n ones _∨_
-∨-zeroʳ = bitwise₂-zeroʳ 1# B._∨_ B.∨-zeroʳ
-
-∨-zero : A.Zero n ones _∨_
-∨-zero = ∨-zeroˡ , ∨-zeroʳ
-
-∨-inverseˡ : A.LeftInverse n ones not _∨_
-∨-inverseˡ = bitwise₂-inverseˡ 1# B.not B._∨_ B.∨-inverseˡ
-
-∨-inverseʳ : A.RightInverse n ones not _∨_
-∨-inverseʳ = bitwise₂-inverseʳ 1# B.not B._∨_ B.∨-inverseʳ
-
-∨-inverse : A.Inverse n ones not _∨_
-∨-inverse = ∨-inverseˡ , ∨-inverseʳ
-
-∨-conicalˡ : A.LeftConical n zeroes _∨_
-∨-conicalˡ = bitwise₂-conicalˡ 0# B._∨_ λ { 0# 0# eq → refl }
-
-∨-conicalʳ : A.RightConical n zeroes _∨_
-∨-conicalʳ = bitwise₂-conicalʳ 0# B._∨_ λ { 0# 0# eq → refl }
-
-∨-conical : A.Conical n zeroes _∨_
-∨-conical = ∨-conicalˡ , ∨-conicalʳ
-
-∨-idem : A.Idempotent n _∨_
-∨-idem = bitwise₂-idem B._∨_ B.∨-idem
-
--- ∧ and ∨
-
-∧-distribˡ-∨ : A.₍ n ₎ _∧_ DistributesOverˡ _∨_
-∧-distribˡ-∨ = bitwise₂-distribˡ B._∧_ B._∨_ B.∧-distribˡ-∨
-
-∧-distribʳ-∨ : A.₍ n ₎ _∧_ DistributesOverʳ _∨_
-∧-distribʳ-∨ = bitwise₂-distribʳ B._∧_ B._∨_ B.∧-distribʳ-∨
-
-∧-distrib-∨ : A.₍ n ₎ _∧_ DistributesOver _∨_
-∧-distrib-∨ = ∧-distribˡ-∨ , ∧-distribʳ-∨
-
-∨-distribˡ-∧ : A.₍ n ₎ _∨_ DistributesOverˡ _∧_
-∨-distribˡ-∧ = bitwise₂-distribˡ B._∨_ B._∧_ B.∨-distribˡ-∧
-
-∨-distribʳ-∧ : A.₍ n ₎ _∨_ DistributesOverʳ _∧_
-∨-distribʳ-∧ = bitwise₂-distribʳ B._∨_ B._∧_ B.∨-distribʳ-∧
-
-∨-distrib-∧ : A.₍ n ₎ _∨_ DistributesOver _∧_
-∨-distrib-∧ = ∨-distribˡ-∧ , ∨-distribʳ-∧
-
-∧-abs-∨ : A.₍ n ₎ _∧_ Absorbs _∨_
-∧-abs-∨ = bitwise₂-absorbs B._∧_ B._∨_ B.∧-abs-∨
-
-∨-abs-∧ : A.₍ n ₎ _∨_ Absorbs _∧_
-∨-abs-∧ = bitwise₂-absorbs B._∨_ B._∧_ B.∨-abs-∧
-
-∧-∨-absorptive : A.Absorptive n _∧_ _∨_
-∧-∨-absorptive = ∧-abs-∨ , ∨-abs-∧
-
--- xor
-
-private
-  bxor-comm : ∀ x y → x B.xor y ≡ y B.xor x
-  bxor-comm 0# 0# = refl
-  bxor-comm 0# 1# = refl
-  bxor-comm 1# 0# = refl
-  bxor-comm 1# 1# = refl
-
-  bxor-identityʳ : ∀ x → x B.xor 0# ≡ x
-  bxor-identityʳ 0# = refl
-  bxor-identityʳ 1# = refl
-
-  bxor-annihilate : ∀ x → x B.xor x ≡ 0#
-  bxor-annihilate 0# = refl
-  bxor-annihilate 1# = refl
-
-  bxor-distribˡ-not : ∀ x y → B.not (x B.xor y) ≡ B.not x B.xor y
-  bxor-distribˡ-not 0# y = refl
-  bxor-distribˡ-not 1# y = B.not-involutive y
-
-  bxor-distribʳ-not : ∀ x y → B.not (x B.xor y) ≡ x B.xor B.not y
-  bxor-distribʳ-not 0# y = refl
-  bxor-distribʳ-not 1# y = refl
-
-xor-assoc : A.Associative n _xor_
-xor-assoc = bitwise₂-assoc B._xor_ (λ
-  { 0# y z → refl
-  ; 1# y z → sym (bxor-distribˡ-not y z)
-  })
-
-xor-comm : A.Commutative n _xor_
-xor-comm = bitwise₂-comm B._xor_ bxor-comm
-
-xor-identityˡ : A.LeftIdentity n zeroes _xor_
-xor-identityˡ = bitwise₂-identityˡ 0# B._xor_ λ _ → refl
-
-xor-identityʳ : A.RightIdentity n zeroes _xor_
-xor-identityʳ = bitwise₂-identityʳ 0# B._xor_ bxor-identityʳ
-
-xor-identity : A.Identity n zeroes _xor_
-xor-identity = xor-identityˡ , xor-identityʳ
-
-xor-inverseˡ : A.LeftInverse n ones not _xor_
-xor-inverseˡ = bitwise₂-inverseˡ 1# B.not B._xor_ (λ { 0# → refl ; 1# → refl })
-
-xor-inverseʳ : A.RightInverse n ones not _xor_
-xor-inverseʳ = bitwise₂-inverseʳ 1# B.not B._xor_ (λ { 0# → refl ; 1# → refl })
-
-xor-inverse : A.Inverse n ones not _xor_
-xor-inverse = xor-inverseˡ , xor-inverseʳ
-
-xor-annihilate : ∀ (xs : BitVec n) → xs xor xs ≡ zeroes
-xor-annihilate [] = refl
-xor-annihilate (x ∷ xs) = cong₂ _∷_ (bxor-annihilate x) (xor-annihilate xs)
-
-xor-cancelˡ : A.LeftCancellative n _xor_
-xor-cancelˡ = bitwise₂-cancelˡ B._xor_ (λ { 0# eq → eq ; 1# eq → B.not-injective eq })
-
-xor-cancelʳ : A.RightCancellative n _xor_
-xor-cancelʳ = bitwise₂-cancelʳ B._xor_ (λ
-  { 0# 0# eq → refl
-  ; 0# 1# eq → ⊥-elim (B.not-¬ refl eq)
-  ; 1# 0# eq → ⊥-elim (B.not-¬ refl (sym eq))
-  ; 1# 1# eq → refl
-  })
-
-xor-cancel : A.Cancellative n _xor_
-xor-cancel = xor-cancelˡ , xor-cancelʳ
-
--- not and xor
-
-xor-distribˡ-not : ∀ (xs ys : BitVec n) → not (xs xor ys) ≡ not xs xor ys
-xor-distribˡ-not [] [] = refl
-xor-distribˡ-not (x ∷ xs) (y ∷ ys) = cong₂ _∷_ (bxor-distribˡ-not x y) (xor-distribˡ-not xs ys)
-
-xor-distribʳ-not : ∀ (xs ys : BitVec n) → not (xs xor ys) ≡ xs xor not ys
-xor-distribʳ-not [] [] = refl
-xor-distribʳ-not (x ∷ xs) (y ∷ ys) = cong₂ _∷_ (bxor-distribʳ-not x y) (xor-distribʳ-not xs ys)
-
--- ∧ and xor
-
-∧-distribˡ-xor : A.₍ n ₎ _∧_ DistributesOverˡ _xor_
-∧-distribˡ-xor = bitwise₂-distribˡ B._∧_ B._xor_ (λ { 0# y z → refl ; 1# y z → refl })
-
-∧-distribʳ-xor : A.₍ n ₎ _∧_ DistributesOverʳ _xor_
-∧-distribʳ-xor = bitwise₂-distribʳ B._∧_ B._xor_ (λ
-  { x 0# z  → refl
-  ; x 1# 0# → sym (bxor-identityʳ x)
-  ; x 1# 1# → sym (bxor-annihilate x)
-  })
-
-∧-distrib-xor : A.₍ n ₎ _∧_ DistributesOver _xor_
-∧-distrib-xor = ∧-distribˡ-xor , ∧-distribʳ-xor
-
--- ∨ and xor
-
-∨-squash-xor : ∀ (xs ys : BitVec n) → xs ∨ (xs xor ys) ≡ xs ∨ ys
-∨-squash-xor [] [] = refl
-∨-squash-xor (x ∷ xs) (y ∷ ys) =
-  flip (cong₂ _∷_) (∨-squash-xor xs ys) (case x return (λ x → x B.∨ x B.xor y ≡ x B.∨ y) of λ
-    { 0# → refl
-    ; 1# → refl
-    })
-
-
--- Conversions
-
--- bitToFin and finToBit
-
-bitToFin-finToBit : ∀ x → bitToFin (finToBit x) ≡ x
-bitToFin-finToBit zero       = refl
-bitToFin-finToBit (suc zero) = refl
-
-finToBit-bitToFin : ∀ x → finToBit (bitToFin x) ≡ x
-finToBit-bitToFin 0# = refl
-finToBit-bitToFin 1# = refl
-
--- toFin and fromFin
-
-fromFin-toFin : ∀ xs → fromFin {n} (toFin {n} xs) ≡ xs
-fromFin-toFin         []       = refl
-fromFin-toFin {suc n} (x ∷ xs) with quotRem {2} (2 ^ n) (combine (bitToFin x) (toFin xs)) | remQuot-combine (bitToFin x) (toFin xs)
-... | .(toFin xs) , .(bitToFin x) | refl = cong₂ _∷_ (finToBit-bitToFin x) (fromFin-toFin xs)
-
-toFin-fromFin : ∀ x → toFin {n} (fromFin x) ≡ x
-toFin-fromFin {zero}  zero = refl
-toFin-fromFin {suc n} x = begin
-  combine (bitToFin (finToBit (proj₁ rq))) (toFin (fromFin {n} (proj₂ rq))) ≡⟨ eq₁ ⟩
-  combine (proj₁ rq) (proj₂ rq) ≡⟨ combine-remQuot (2 ^ n) x ⟩
-  x ∎
-  where
-  open ≡-Reasoning
-  rq = remQuot {2} (2 ^ n) x
-  eq₁ = cong₂ combine (bitToFin-finToBit (proj₁ rq)) (toFin-fromFin {n} (proj₂ rq))
-
diff --git a/src/Helium/Data/Bits.agda b/src/Helium/Data/Bits.agda
new file mode 100644
index 0000000..255bd9d
--- /dev/null
+++ b/src/Helium/Data/Bits.agda
@@ -0,0 +1,109 @@
+{-# OPTIONS --safe --without-K #-}
+
+module Helium.Data.Bits where
+
+open import Algebra
+open import Algebra.Morphism.Definitions
+open import Data.Fin as Fin hiding (_+_; _≟_)
+import Data.Fin.Properties as Finₚ
+open import Data.Nat as ℕ using (ℕ; suc; _+_)
+import Data.Nat.Properties as ℕₚ
+open import Function
+open import Level using (_⊔_) renaming (suc to ℓsuc)
+open import Relation.Binary
+import Relation.Binary.PropositionalEquality as P
+
+private
+  variable
+    k l m n : ℕ
+
+
+module _
+  {a ℓ} {A : ℕ → Set a}
+  (_≈_ : ∀ {m n} → REL (A m) (A n) ℓ)
+  where
+
+  private
+    variable
+      u v x y z : A n
+
+    infix 4 _≗_
+
+    _≗_ : ∀ {b} {B : Set b} → REL (B → A m) (B → A n) (b ⊔ ℓ)
+    f ≗ g = ∀ {x} → f x ≈ g x
+
+  record IsBits (_∨_ _∧_ : ∀ {n} → Op₂ (A n))
+                (¬_ : ∀ {n} → Op₁ (A n))
+                (0# 1# : ∀ {n} → A n)
+                (_∶_ : ∀ {m n} → A m → A n → A (m + n))
+                (slice : ∀ {n} (i : Fin (suc n)) j → A n → A (toℕ (i - j)))
+                (update : ∀ {n} (i : Fin (suc n)) j → Op₁ (A (toℕ (i - j))) → Op₁ (A n))
+                : Set (a ⊔ ℓ) where
+    infix 4 _≟_
+    field
+      -- boolean algebraic properties
+      isBooleanAlgebra : IsBooleanAlgebra (_≈_ {n}) _∨_ _∧_ ¬_ 0# 1#
+      _≟_ : Decidable (_≈_ {m} {n})
+
+      -- _∶_ properties
+      ∶-cong      : x ≈ y → u ≈ v → (x ∶ u) ≈ (y ∶ v)
+      ∶-assoc     : ((x ∶ y) ∶ z) ≈ (x ∶ (y ∶ z))
+      ∶-identityˡ : ∀ {ε : A 0} → (ε ∶ x) ≈ x
+      ∶-identityʳ : ∀ {ε : A 0} → (x ∶ ε) ≈ x
+      ∶-swap-∨ : ((x ∨ y) ∶ (u ∨ v)) ≈ ((x ∶ u) ∨ (y ∶ v))
+      ∶-swap-∧ : ((x ∧ y) ∶ (u ∧ v)) ≈ ((x ∶ u) ∧ (y ∶ v))
+      ∶-homo-¬ : ((¬ x) ∶ (¬ y)) ≈ (¬ (x ∶ y))
+      1#∶1# : (1# {m} ∶ 1# {n}) ≈ 1# {m + n}
+      0#∶0# : (0# {m} ∶ 0# {n}) ≈ 0# {m + n}
+
+      -- slice properties
+      slice-cong : ∀ {i j} → x ≈ y → slice i j x ≈ slice i j y
+      slice-fromℕ-zero : ∀ {x : A n} → slice (fromℕ n) zero x ≈ x
+      slice-inject : ∀ {x : A m} {y : A n} {i i′ j j′} →
+        .(i≡i′ : toℕ i P.≡ toℕ i′) .(j≡j′ : toℕ j P.≡ toℕ j′) →
+        slice i′ j′ (x ∶ y) ≈ slice i j y
+      slice-raise : ∀ {x : A m} {y : A n} {i i′ j j′} →
+        .(n+i≡i′ : n + toℕ i P.≡ toℕ i′) .(n+j≡j′ : n + toℕ j P.≡ toℕ j′) →
+        slice i′ j′ (x ∶ y) ≈ slice i j x
+
+      -- update properties
+      update-cong : ∀ {i j f} → (∀ {x y} → x ≈ y → f x ≈ f y) → x ≈ y → update i j f x ≈ update i j f y
+      update² : ∀ {i j f g} → update i j f ∘ update {n} i j g ≗ update {n} i j (f ∘ g)
+      slice-update : ∀ {i j f} → slice {n} i j ∘ update {n} i j f ≗ f ∘ slice i j
+
+record RawBits a ℓ : Set (ℓsuc a ⊔ ℓsuc ℓ) where
+  infix 8 ¬_
+  infixr 7 _∧_
+  infixr 6 _∨_
+  infixr 5 _∶_
+  infix 4 _≈_
+  field
+    BitVec : ℕ → Set a
+    _≈_    : REL (BitVec m) (BitVec n) ℓ
+    _∨_    : Op₂ (BitVec n)
+    _∧_    : Op₂ (BitVec n)
+    ¬_     : Op₁ (BitVec n)
+    0#     : BitVec n
+    1#     : BitVec n
+    _∶_    : BitVec m → BitVec n → BitVec (m + n)
+    slice  : ∀ (i : Fin (suc n)) j → BitVec n → BitVec (toℕ (i - j))
+    update : ∀ (i : Fin (suc n)) j → Op₁ (BitVec (toℕ (i - j))) → Op₁ (BitVec n)
+
+record Bits a ℓ : Set (ℓsuc a ⊔ ℓsuc ℓ) where
+  infix 8 ¬_
+  infixr 7 _∧_
+  infixr 6 _∨_
+  infixr 5 _∶_
+  infix 4 _≈_
+  field
+    BitVec : ℕ → Set a
+    _≈_    : REL (BitVec m) (BitVec n) ℓ
+    _∨_    : Op₂ (BitVec n)
+    _∧_    : Op₂ (BitVec n)
+    ¬_     : Op₁ (BitVec n)
+    0#     : BitVec n
+    1#     : BitVec n
+    _∶_    : BitVec m → BitVec n → BitVec (m + n)
+    slice  : ∀ (i : Fin (suc n)) j → BitVec n → BitVec (toℕ (i - j))
+    update : ∀ (i : Fin (suc n)) j → Op₁ (BitVec (toℕ (i - j))) → Op₁ (BitVec n)
+    isBits : IsBits _≈_ _∨_ _∧_ ¬_ 0# 1# _∶_ slice update