1 files changed, 412 insertions, 0 deletions
diff --git a/src/Helium/Data/Pseudocode/Types.agda b/src/Helium/Data/Pseudocode/Types.agda
new file mode 100644
index 0000000..a545ddc
--- /dev/null
+++ b/src/Helium/Data/Pseudocode/Types.agda
@@ -0,0 +1,412 @@
+------------------------------------------------------------------------
+-- Agda Helium
+--
+-- Definition of types and operations used by the Armv8-M pseudocode.
+------------------------------------------------------------------------
+
+{-# OPTIONS --safe --without-K #-}
+
+module Helium.Data.Pseudocode.Types where
+
+open import Algebra.Core
+import Algebra.Definitions.RawSemiring as RS
+open import Data.Bool.Base using (Bool; if_then_else_)
+open import Data.Empty using (⊥-elim)
+open import Data.Fin.Base as Fin hiding (cast)
+import Data.Fin.Properties as Fₚ
+import Data.Fin.Induction as Induction
+open import Data.Nat.Base using (ℕ; zero; suc)
+open import Data.Sum using (_⊎_; inj₁; inj₂; [_,_]′)
+open import Data.Vec.Functional
+open import Data.Vec.Functional.Relation.Binary.Pointwise using (Pointwise)
+import Data.Vec.Functional.Relation.Binary.Pointwise.Properties as Pwₚ
+open import Function using (_$_; _∘′_; id)
+open import Helium.Algebra.Ordered.StrictTotal.Bundles
+open import Helium.Algebra.Decidable.Bundles
+  using (BooleanAlgebra; RawBooleanAlgebra)
+import Helium.Algebra.Decidable.Construct.Pointwise as Pw
+open import Helium.Algebra.Morphism.Structures
+open import Level using (_⊔_) renaming (suc to ℓsuc)
+open import Relation.Binary.Core using (Rel)
+open import Relation.Binary.Definitions
+open import Relation.Binary.PropositionalEquality as P using (_≡_)
+import Relation.Binary.Reasoning.StrictPartialOrder as Reasoning
+open import Relation.Binary.Structures using (IsStrictTotalOrder)
+open import Relation.Nullary using (does; yes; no)
+open import Relation.Nullary.Decidable.Core
+  using (False; toWitnessFalse; fromWitnessFalse)
+
+record RawPseudocode b₁ b₂ i₁ i₂ i₃ r₁ r₂ r₃ : Set (ℓsuc (b₁ ⊔ b₂ ⊔ i₁ ⊔ i₂ ⊔ i₃ ⊔ r₁ ⊔ r₂ ⊔ r₃)) where
+  field
+    bitRawBooleanAlgebra : RawBooleanAlgebra b₁ b₂
+    integerRawRing : RawRing i₁ i₂ i₃
+    realRawField : RawField r₁ r₂ r₃
+
+  bitsRawBooleanAlgebra : ℕ → RawBooleanAlgebra b₁ b₂
+  bitsRawBooleanAlgebra =  Pw.rawBooleanAlgebra  bitRawBooleanAlgebra
+
+  module 𝔹 = RawBooleanAlgebra bitRawBooleanAlgebra
+    renaming (Carrier to Bit; ⊤ to 1𝔹; ⊥ to 0𝔹)
+  module Bits {n} = RawBooleanAlgebra (bitsRawBooleanAlgebra n)
+    renaming (⊤ to ones; ⊥ to zeros)
+  module ℤ = RawRing integerRawRing renaming (Carrier to ℤ; 1# to 1ℤ; 0# to 0ℤ)
+  module ℝ = RawField realRawField renaming (Carrier to ℝ; 1# to 1ℝ; 0# to 0ℝ)
+  module ℤ′ = RS ℤ.Unordered.rawSemiring
+  module ℝ′ = RS ℝ.Unordered.rawSemiring
+
+  Bits : ℕ → Set b₁
+  Bits n = Bits.Carrier {n}
+
+  open 𝔹 public using (Bit; 1𝔹; 0𝔹)
+  open Bits public using (ones; zeros)
+  open ℤ public using (ℤ; 1ℤ; 0ℤ)
+  open ℝ public using (ℝ; 1ℝ; 0ℝ)
+
+  infix 4 _≟ᶻ_ _<ᶻ?_ _≟ʳ_ _<ʳ?_ _≟ᵇ₁_ _≟ᵇ_
+  field
+    _≟ᶻ_  : Decidable ℤ._≈_
+    _<ᶻ?_ : Decidable ℤ._<_
+    _≟ʳ_  : Decidable ℝ._≈_
+    _<ʳ?_ : Decidable ℝ._<_
+    _≟ᵇ₁_ : Decidable 𝔹._≈_
+
+  _≟ᵇ_ : ∀ {n} → Decidable (Bits._≈_ {n})
+  _≟ᵇ_ = Pwₚ.decidable _≟ᵇ₁_
+
+  field
+    _/1 : ℤ → ℝ
+    ⌊_⌋ : ℝ → ℤ
+
+  cast : ∀ {m n} → .(eq : m ≡ n) → Bits m → Bits n
+  cast eq x i = x $ Fin.cast (P.sym eq) i
+
+  2ℤ : ℤ
+  2ℤ = 2 ℤ′.×′ 1ℤ
+
+  getᵇ : ∀ {n} → Fin n → Bits n → Bit
+  getᵇ i x = x (opposite i)
+
+  setᵇ : ∀ {n} → Fin n → Bit → Op₁ (Bits n)
+  setᵇ i b = updateAt (opposite i) λ _ → b
+
+  sliceᵇ : ∀ {n} (i : Fin (suc n)) j → Bits n → Bits (toℕ (i - j))
+  sliceᵇ         zero    zero    x = []
+  sliceᵇ {suc n} (suc i) zero    x = getᵇ i x ∷ sliceᵇ i zero (tail x)
+  sliceᵇ {suc n} (suc i) (suc j) x = sliceᵇ i j (tail x)
+
+  updateᵇ : ∀ {n} (i : Fin (suc n)) j → Bits (toℕ (i - j)) → Op₁ (Bits n)
+  updateᵇ {n} = Induction.<-weakInduction P (λ _ _ → id) helper
+    where
+    P : Fin (suc n) → Set b₁
+    P i = ∀ j → Bits (toℕ (i - j)) → Op₁ (Bits n)
+
+    eq : ∀ {n} {i : Fin n} → toℕ i ≡ toℕ (inject₁ i)
+    eq = P.sym $ Fₚ.toℕ-inject₁ _
+
+    eq′ : ∀ {n} {i : Fin n} j → toℕ (i - j) ≡ toℕ (inject₁ i - Fin.cast eq j)
+    eq′             zero    = eq
+    eq′ {i = suc _} (suc j) = eq′ j
+
+    helper : ∀ i → P (inject₁ i) → P (suc i)
+    helper i rec zero    y = rec zero (cast eq (tail y)) ∘′ setᵇ i (y zero)
+    helper i rec (suc j) y = rec (Fin.cast eq j) (cast (eq′ j) y)
+
+  hasBit : ∀ {n} → Fin n → Bits n → Bool
+  hasBit i x = does (getᵇ i x ≟ᵇ₁ 1𝔹)
+
+  infixl 7 _div_ _mod_
+
+  _div_ : ∀ (x y : ℤ) → {y≉0 : False (y /1 ≟ʳ 0ℝ)} → ℤ
+  (x div y) {y≉0} = ⌊ x /1 ℝ.* toWitnessFalse y≉0 ℝ.⁻¹ ⌋
+
+  _mod_ : ∀ (x y : ℤ) → {y≉0 : False (y /1 ≟ʳ 0ℝ)} → ℤ
+  (x mod y) {y≉0} = x ℤ.+ ℤ.- y ℤ.* (x div y) {y≉0}
+
+  infixl 5 _<<_
+  _<<_ : ℤ → ℕ → ℤ
+  x << n = 2ℤ ℤ′.^′ n ℤ.* x
+
+  module ShiftNotZero
+    (1<<n≉0 : ∀ n → False ((1ℤ << n) /1 ≟ʳ 0ℝ))
+    where
+
+    infixl 5 _>>_
+    _>>_ : ℤ → ℕ → ℤ
+    x >> zero  = x
+    x >> suc n = (x div (1ℤ << suc n)) {1<<n≉0 (suc n)}
+
+    getᶻ : ℕ → ℤ → Bit
+    getᶻ n x =
+      if does ((x mod (1ℤ << suc n)) {1<<n≉0 (suc n)} <ᶻ? 1ℤ << n)
+      then 1𝔹
+      else 0𝔹
+
+    sliceᶻ : ∀ n i → ℤ → Bits (n ℕ-ℕ i)
+    sliceᶻ zero    zero    x = []
+    sliceᶻ (suc n) zero    x = getᶻ n x ∷ sliceᶻ n zero x
+    sliceᶻ (suc n) (suc i) x = sliceᶻ n i (x >> 1)
+
+  uint : ∀ {n} → Bits n → ℤ
+  uint x = ℤ′.sum λ i → if hasBit i x then 1ℤ << toℕ i else 0ℤ
+
+  sint : ∀ {n} → Bits n → ℤ
+  sint {zero}  x = 0ℤ
+  sint {suc n} x = uint x ℤ.+ ℤ.- (if hasBit (fromℕ n) x then 1ℤ << suc n else 0ℤ)
+
+record Pseudocode b₁ b₂ i₁ i₂ i₃ r₁ r₂ r₃ :
+                  Set (ℓsuc (b₁ ⊔ b₂ ⊔ i₁ ⊔ i₂ ⊔ i₃ ⊔ r₁ ⊔ r₂ ⊔ r₃)) where
+  field
+    bitBooleanAlgebra : BooleanAlgebra b₁ b₂
+    integerRing       : CommutativeRing i₁ i₂ i₃
+    realField         : Field r₁ r₂ r₃
+
+  bitsBooleanAlgebra : ℕ → BooleanAlgebra b₁ b₂
+  bitsBooleanAlgebra = Pw.booleanAlgebra bitBooleanAlgebra
+
+  module 𝔹 = BooleanAlgebra bitBooleanAlgebra
+    renaming (Carrier to Bit; ⊤ to 1𝔹; ⊥ to 0𝔹)
+  module Bits {n} = BooleanAlgebra (bitsBooleanAlgebra n)
+    renaming (⊤ to ones; ⊥ to zeros)
+  module ℤ = CommutativeRing integerRing
+    renaming (Carrier to ℤ; 1# to 1ℤ; 0# to 0ℤ)
+  module ℝ = Field realField
+    renaming (Carrier to ℝ; 1# to 1ℝ; 0# to 0ℝ)
+
+  Bits : ℕ → Set b₁
+  Bits n = Bits.Carrier {n}
+
+  open 𝔹 public using (Bit; 1𝔹; 0𝔹)
+  open Bits public using (ones; zeros)
+  open ℤ public using (ℤ; 1ℤ; 0ℤ)
+  open ℝ public using (ℝ; 1ℝ; 0ℝ)
+
+  module ℤ-Reasoning = Reasoning ℤ.strictPartialOrder
+  module ℝ-Reasoning = Reasoning ℝ.strictPartialOrder
+
+  field
+    integerDiscrete : ∀ x y → y ℤ.≤ x ⊎ x ℤ.+ 1ℤ ℤ.≤ y
+    1≉0 : 1ℤ ℤ.≉ 0ℤ
+
+    _/1 : ℤ → ℝ
+    ⌊_⌋ : ℝ → ℤ
+    /1-isHomo : IsRingHomomorphism ℤ.Unordered.rawRing ℝ.Unordered.rawRing _/1
+    ⌊⌋-isHomo : IsRingHomomorphism ℝ.Unordered.rawRing ℤ.Unordered.rawRing ⌊_⌋
+    /1-mono : ∀ x y → x ℤ.< y → x /1 ℝ.< y /1
+    ⌊⌋-floor : ∀ x y → x ℤ.≤ ⌊ y ⌋ → ⌊ y ⌋ ℤ.< x ℤ.+ 1ℤ
+    ⌊⌋∘/1≗id : ∀ x → ⌊ x /1 ⌋ ℤ.≈ x
+
+  module /1 = IsRingHomomorphism /1-isHomo renaming (⟦⟧-cong to cong)
+  module ⌊⌋ = IsRingHomomorphism ⌊⌋-isHomo renaming (⟦⟧-cong to cong)
+
+  bitRawBooleanAlgebra : RawBooleanAlgebra b₁ b₂
+  bitRawBooleanAlgebra = record
+    { _≈_ = _≈_
+    ; _∨_ = _∨_
+    ; _∧_ = _∧_
+    ; ¬_  = ¬_
+    ; ⊤   = ⊤
+    ; ⊥   = ⊥
+    }
+    where open BooleanAlgebra bitBooleanAlgebra
+
+  rawPseudocode : RawPseudocode b₁ b₂ i₁ i₂ i₃ r₁ r₂ r₃
+  rawPseudocode = record
+    { bitRawBooleanAlgebra = bitRawBooleanAlgebra
+    ; integerRawRing = ℤ.rawRing
+    ; realRawField = ℝ.rawField
+    ; _≟ᶻ_ = ℤ._≟_
+    ; _<ᶻ?_ = ℤ._<?_
+    ; _≟ʳ_ = ℝ._≟_
+    ; _<ʳ?_ = ℝ._<?_
+    ; _≟ᵇ₁_ = 𝔹._≟_
+    ; _/1 = _/1
+    ; ⌊_⌋ = ⌊_⌋
+    }
+
+  open RawPseudocode rawPseudocode public
+    using
+    ( 2ℤ; cast; getᵇ; setᵇ; sliceᵇ; updateᵇ; hasBit
+    ; _div_; _mod_; _<<_; uint; sint
+    )
+
+  private
+    -- FIXME: move almost all of these proofs into a separate module
+    a<b⇒ca<cb : ∀ {a b c} → 0ℤ ℤ.< c → a ℤ.< b → c ℤ.* a ℤ.< c ℤ.* b
+    a<b⇒ca<cb {a} {b} {c} 0<c a<b = begin-strict
+      c ℤ.* a                     ≈˘⟨ ℤ.+-identityʳ _ ⟩
+      c ℤ.* a ℤ.+ 0ℤ              <⟨  ℤ.+-invariantˡ _ $ ℤ.0<a+0<b⇒0<ab 0<c 0<b-a ⟩
+      c ℤ.* a ℤ.+ c ℤ.* (b ℤ.- a) ≈˘⟨ ℤ.distribˡ c a (b ℤ.- a) ⟩
+      c ℤ.* (a ℤ.+ (b ℤ.- a))     ≈⟨  ℤ.*-congˡ $ ℤ.+-congˡ $ ℤ.+-comm b (ℤ.- a) ⟩
+      c ℤ.* (a ℤ.+ (ℤ.- a ℤ.+ b)) ≈˘⟨ ℤ.*-congˡ $ ℤ.+-assoc a (ℤ.- a) b ⟩
+      c ℤ.* ((a ℤ.+ ℤ.- a) ℤ.+ b) ≈⟨  ℤ.*-congˡ $ ℤ.+-congʳ $ ℤ.-‿inverseʳ a ⟩
+      c ℤ.* (0ℤ ℤ.+ b)            ≈⟨  (ℤ.*-congˡ $ ℤ.+-identityˡ b) ⟩
+      c ℤ.* b                     ∎
+      where
+      open ℤ-Reasoning
+
+      0<b-a : 0ℤ ℤ.< b ℤ.- a
+      0<b-a = begin-strict
+        0ℤ      ≈˘⟨ ℤ.-‿inverseʳ a ⟩
+        a ℤ.- a <⟨  ℤ.+-invariantʳ (ℤ.- a) a<b ⟩
+        b ℤ.- a ∎
+
+    -‿idem : ∀ x → ℤ.- (ℤ.- x) ℤ.≈ x
+    -‿idem x = begin-equality
+      ℤ.- (ℤ.- x)             ≈˘⟨ ℤ.+-identityˡ _ ⟩
+      0ℤ ℤ.- ℤ.- x            ≈˘⟨ ℤ.+-congʳ $ ℤ.-‿inverseʳ x ⟩
+      x ℤ.- x ℤ.- ℤ.- x       ≈⟨  ℤ.+-assoc x (ℤ.- x) _ ⟩
+      x ℤ.+ (ℤ.- x ℤ.- ℤ.- x) ≈⟨  ℤ.+-congˡ $ ℤ.-‿inverseʳ (ℤ.- x) ⟩
+      x ℤ.+ 0ℤ                ≈⟨  ℤ.+-identityʳ x ⟩
+      x                       ∎
+      where open ℤ-Reasoning
+
+    -a*b≈-ab : ∀ a b → ℤ.- a ℤ.* b ℤ.≈ ℤ.- (a ℤ.* b)
+    -a*b≈-ab a b = begin-equality
+      ℤ.- a ℤ.* b                           ≈˘⟨ ℤ.+-identityʳ _ ⟩
+      ℤ.- a ℤ.* b ℤ.+ 0ℤ                    ≈˘⟨ ℤ.+-congˡ $ ℤ.-‿inverseʳ _ ⟩
+      ℤ.- a ℤ.* b ℤ.+ (a ℤ.* b ℤ.- a ℤ.* b) ≈˘⟨ ℤ.+-assoc _ _ _ ⟩
+      ℤ.- a ℤ.* b ℤ.+ a ℤ.* b ℤ.- a ℤ.* b   ≈˘⟨ ℤ.+-congʳ $ ℤ.distribʳ b _ a ⟩
+      (ℤ.- a ℤ.+ a) ℤ.* b ℤ.- a ℤ.* b       ≈⟨  ℤ.+-congʳ $ ℤ.*-congʳ $ ℤ.-‿inverseˡ a ⟩
+      0ℤ ℤ.* b ℤ.- a ℤ.* b                  ≈⟨  ℤ.+-congʳ $ ℤ.zeroˡ b ⟩
+      0ℤ ℤ.- a ℤ.* b                        ≈⟨  ℤ.+-identityˡ _ ⟩
+      ℤ.- (a ℤ.* b)                         ∎
+      where open ℤ-Reasoning
+
+    a*-b≈-ab : ∀ a b → a ℤ.* ℤ.- b ℤ.≈ ℤ.- (a ℤ.* b)
+    a*-b≈-ab a b = begin-equality
+      a ℤ.* ℤ.- b   ≈⟨ ℤ.*-comm a (ℤ.- b) ⟩
+      ℤ.- b ℤ.* a   ≈⟨ -a*b≈-ab b a ⟩
+      ℤ.- (b ℤ.* a) ≈⟨ ℤ.-‿cong $ ℤ.*-comm b a ⟩
+      ℤ.- (a ℤ.* b) ∎
+      where open ℤ-Reasoning
+
+    0<a⇒0>-a : ∀ {a} → 0ℤ ℤ.< a → 0ℤ ℤ.> ℤ.- a
+    0<a⇒0>-a {a} 0<a = begin-strict
+      ℤ.- a    ≈˘⟨ ℤ.+-identityˡ _ ⟩
+      0ℤ ℤ.- a <⟨  ℤ.+-invariantʳ _ 0<a ⟩
+      a ℤ.- a  ≈⟨  ℤ.-‿inverseʳ a ⟩
+      0ℤ       ∎
+      where open ℤ-Reasoning
+
+    0>a⇒0<-a : ∀ {a} → 0ℤ ℤ.> a → 0ℤ ℤ.< ℤ.- a
+    0>a⇒0<-a {a} 0>a = begin-strict
+      0ℤ       ≈˘⟨ ℤ.-‿inverseʳ a ⟩
+      a ℤ.- a  <⟨  ℤ.+-invariantʳ _ 0>a ⟩
+      0ℤ ℤ.- a ≈⟨  ℤ.+-identityˡ _ ⟩
+      ℤ.- a    ∎
+      where open ℤ-Reasoning
+
+    0<-a⇒0>a : ∀ {a} → 0ℤ ℤ.< ℤ.- a → 0ℤ ℤ.> a
+    0<-a⇒0>a {a} 0<-a = begin-strict
+      a        ≈˘⟨ ℤ.+-identityʳ a ⟩
+      a ℤ.+ 0ℤ <⟨  ℤ.+-invariantˡ a 0<-a ⟩
+      a ℤ.- a  ≈⟨  ℤ.-‿inverseʳ a ⟩
+      0ℤ       ∎
+      where open ℤ-Reasoning
+
+    0>-a⇒0<a : ∀ {a} → 0ℤ ℤ.> ℤ.- a → 0ℤ ℤ.< a
+    0>-a⇒0<a {a} 0>-a = begin-strict
+      0ℤ       ≈˘⟨ ℤ.-‿inverseʳ a ⟩
+      a ℤ.- a  <⟨  ℤ.+-invariantˡ a 0>-a ⟩
+      a ℤ.+ 0ℤ ≈⟨  ℤ.+-identityʳ a ⟩
+      a        ∎
+      where open ℤ-Reasoning
+
+    0>a+0<b⇒0>ab : ∀ {a b} → 0ℤ ℤ.> a → 0ℤ ℤ.< b → 0ℤ ℤ.> a ℤ.* b
+    0>a+0<b⇒0>ab {a} {b} 0>a 0<b = 0<-a⇒0>a $ begin-strict
+      0ℤ              <⟨ ℤ.0<a+0<b⇒0<ab (0>a⇒0<-a 0>a) 0<b ⟩
+      ℤ.- a ℤ.* b     ≈⟨ -a*b≈-ab a b ⟩
+      ℤ.- (a ℤ.* b)   ∎
+      where open ℤ-Reasoning
+
+    0<a+0>b⇒0>ab : ∀ {a b} → 0ℤ ℤ.< a → 0ℤ ℤ.> b → 0ℤ ℤ.> a ℤ.* b
+    0<a+0>b⇒0>ab {a} {b} 0<a 0>b = 0<-a⇒0>a $ begin-strict
+      0ℤ              <⟨ ℤ.0<a+0<b⇒0<ab 0<a (0>a⇒0<-a 0>b) ⟩
+      a ℤ.* ℤ.- b     ≈⟨ a*-b≈-ab a b ⟩
+      ℤ.- (a ℤ.* b)   ∎
+      where open ℤ-Reasoning
+
+    0>a+0>b⇒0<ab : ∀ {a b} → 0ℤ ℤ.> a → 0ℤ ℤ.> b → 0ℤ ℤ.< a ℤ.* b
+    0>a+0>b⇒0<ab {a} {b} 0>a 0>b = begin-strict
+      0ℤ                  <⟨ ℤ.0<a+0<b⇒0<ab (0>a⇒0<-a 0>a) (0>a⇒0<-a 0>b) ⟩
+      ℤ.- a ℤ.* ℤ.- b     ≈⟨ -a*b≈-ab a (ℤ.- b) ⟩
+      ℤ.- (a ℤ.* ℤ.- b)   ≈⟨ ℤ.-‿cong $ a*-b≈-ab a b ⟩
+      ℤ.- (ℤ.- (a ℤ.* b)) ≈⟨ -‿idem (a ℤ.* b) ⟩
+      a ℤ.* b             ∎
+      where open ℤ-Reasoning
+
+    a≉0+b≉0⇒ab≉0 : ∀ {a b} → a ℤ.≉ 0ℤ → b ℤ.≉ 0ℤ → a ℤ.* b ℤ.≉ 0ℤ
+    a≉0+b≉0⇒ab≉0 {a} {b} a≉0 b≉0 ab≈0 with ℤ.compare a 0ℤ | ℤ.compare b 0ℤ
+    ... | tri< a<0 _ _ | tri< b<0 _ _ = ℤ.irrefl (ℤ.Eq.sym ab≈0) $ 0>a+0>b⇒0<ab a<0 b<0
+    ... | tri< a<0 _ _ | tri≈ _ b≈0 _ = b≉0 b≈0
+    ... | tri< a<0 _ _ | tri> _ _ b>0 = ℤ.irrefl ab≈0 $ 0>a+0<b⇒0>ab a<0 b>0
+    ... | tri≈ _ a≈0 _ | _            = a≉0 a≈0
+    ... | tri> _ _ a>0 | tri< b<0 _ _ = ℤ.irrefl ab≈0 $ 0<a+0>b⇒0>ab a>0 b<0
+    ... | tri> _ _ a>0 | tri≈ _ b≈0 _ = b≉0 b≈0
+    ... | tri> _ _ a>0 | tri> _ _ b>0 = ℤ.irrefl (ℤ.Eq.sym ab≈0) $ ℤ.0<a+0<b⇒0<ab a>0 b>0
+
+    ab≈0⇒a≈0⊎b≈0 : ∀ {a b} → a ℤ.* b ℤ.≈ 0ℤ → a ℤ.≈ 0ℤ ⊎ b ℤ.≈ 0ℤ
+    ab≈0⇒a≈0⊎b≈0 {a} {b} ab≈0 with a ℤ.≟ 0ℤ | b ℤ.≟ 0ℤ
+    ... | yes a≈0 | _       = inj₁ a≈0
+    ... | no a≉0  | yes b≈0 = inj₂ b≈0
+    ... | no a≉0  | no b≉0  = ⊥-elim (a≉0+b≉0⇒ab≉0 a≉0 b≉0 ab≈0)
+
+    2a<<n≈a<<1+n : ∀ a n → 2ℤ ℤ.* (a << n) ℤ.≈ a << suc n
+    2a<<n≈a<<1+n a zero    = ℤ.*-congˡ $ ℤ.*-identityˡ a
+    2a<<n≈a<<1+n a (suc n) = begin-equality
+      2ℤ ℤ.* (a << suc n) ≈˘⟨ ℤ.*-assoc 2ℤ _ a ⟩
+      (2ℤ ℤ.* _) ℤ.* a    ≈⟨  ℤ.*-congʳ $ ℤ.*-comm 2ℤ _ ⟩
+      a << suc (suc n)    ∎
+      where open ℤ-Reasoning
+
+    0<1 : 0ℤ ℤ.< 1ℤ
+    0<1 with ℤ.compare 0ℤ 1ℤ
+    ... | tri< 0<1 _ _ = 0<1
+    ... | tri≈ _ 0≈1 _ = ⊥-elim (1≉0 (ℤ.Eq.sym 0≈1))
+    ... | tri> _ _ 0>1 = begin-strict
+        0ℤ                  ≈˘⟨ ℤ.zeroʳ (ℤ.- 1ℤ) ⟩
+        ℤ.- 1ℤ ℤ.* 0ℤ       <⟨  a<b⇒ca<cb (0>a⇒0<-a 0>1) (0>a⇒0<-a 0>1) ⟩
+        ℤ.- 1ℤ ℤ.* ℤ.- 1ℤ   ≈⟨  -a*b≈-ab 1ℤ (ℤ.- 1ℤ) ⟩
+        ℤ.- (1ℤ ℤ.* ℤ.- 1ℤ) ≈⟨  ℤ.-‿cong $ ℤ.*-identityˡ (ℤ.- 1ℤ) ⟩
+        ℤ.- (ℤ.- 1ℤ)        ≈⟨  -‿idem 1ℤ ⟩
+        1ℤ                  ∎
+      where open ℤ-Reasoning
+
+    0<2 : 0ℤ ℤ.< 2ℤ
+    0<2 = begin-strict
+      0ℤ        ≈˘⟨ ℤ.+-identity² ⟩
+      0ℤ ℤ.+ 0ℤ <⟨  ℤ.+-invariantˡ 0ℤ 0<1 ⟩
+      0ℤ ℤ.+ 1ℤ <⟨  ℤ.+-invariantʳ 1ℤ 0<1 ⟩
+      2ℤ        ∎
+      where open ℤ-Reasoning
+
+    1<<n≉0 : ∀ n → 1ℤ << n ℤ.≉ 0ℤ
+    1<<n≉0 zero          eq = 1≉0 1≈0
+      where
+      open ℤ-Reasoning
+      1≈0 = begin-equality
+        1ℤ        ≈˘⟨ ℤ.*-identity² ⟩
+        1ℤ ℤ.* 1ℤ ≈⟨  eq ⟩
+        0ℤ        ∎
+    1<<n≉0 (suc zero)    eq = ℤ.irrefl 0≈2 0<2
+      where
+      open ℤ-Reasoning
+      0≈2 = begin-equality
+        0ℤ        ≈˘⟨ eq ⟩
+        2ℤ ℤ.* 1ℤ ≈⟨  ℤ.*-identityʳ 2ℤ ⟩
+        2ℤ        ∎
+    1<<n≉0 (suc (suc n)) eq =
+      [ (λ 2≈0 → ℤ.irrefl (ℤ.Eq.sym 2≈0) 0<2) , 1<<n≉0 (suc n) ]′
+      $ ab≈0⇒a≈0⊎b≈0 $ ℤ.Eq.trans (2a<<n≈a<<1+n 1ℤ (suc n)) eq
+
+    1<<n≉0ℝ : ∀ n → (1ℤ << n) /1 ℝ.≉ 0ℝ
+    1<<n≉0ℝ n eq = 1<<n≉0 n $ (begin-equality
+      1ℤ << n          ≈˘⟨ ⌊⌋∘/1≗id (1ℤ << n) ⟩
+      ⌊ (1ℤ << n) /1 ⌋ ≈⟨  ⌊⌋.cong $ eq ⟩
+      ⌊ 0ℝ ⌋           ≈⟨  ⌊⌋.0#-homo ⟩
+      0ℤ               ∎)
+      where open ℤ-Reasoning
+
+    open RawPseudocode rawPseudocode using (module ShiftNotZero)
+
+  open ShiftNotZero (λ n → fromWitnessFalse (1<<n≉0ℝ n)) public