[Simplicity] Simplicity Video from Scale by the Bay 2018
Russell O'Connor
roconnor at blockstream.io
Sun Dec 23 08:21:05 AEDT 2018
Chris has brought to my attention that my presentation of Simplicity at
this year's Scale by the Bay has been available for a few weeks at
https://www.youtube.com/watch?v=M4XnDrRIKx8. In that video I give a worked
example of a shallow embedding of Simplicity into Agda and proving the
correctness of a multi-bit adder.
Simplicity isn't officially being developed in Agda, however Agda has some
features that make it a nice language to use for presentation purposes. I
am attaching the Agda source files (before and after) that I used for the
presentation so that you can follow along.
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.ozlabs.org/pipermail/simplicity/attachments/20181222/c23052ed/attachment-0001.html>
-------------- next part --------------
--
--
--
--
--
--
--
-- Simplicity for Programable Money
--
-- Russell O'Connor (Blockstream)
--
-- November 17th, 2018
--
-- Scale by the Bay
--
--
--
--
--
--
--
--
--
--
-- Background
--
-- * In Bitcoin funds are guarded by small programs written in Bitcoin Script.
--
-- * A typical program in Bitcoin script validates a digital signature to authorize a transaction.
--
-- * Other, more complex, programs allow one to create "smart contracts":
--
-- + Cross-chain atomic transactions
--
-- + Hash Time-lock Contracts
--
-- + Bi-directional payment channels
--
-- + Lightning Network
--
-- + and more.
--
-- * Bitcoin is programable money.
--
--
--
-- Bitcoin Script
--
-- * Stack machine without looping instructions
--
-- * Enables static analysis
--
-- + You can bound the maximum number of each operation that will be evaluated.
--
-- + Bitcoin rejects programs that have too many, expensive, signature verification
-- operations.
--
-- * Allows caching of results
--
-- + Evaluation depends only on the transaction data.
--
-- + If the Bitcoin Script is successful, that result holds no matter where the
-- transaction is added to the blockchain.
--
--
--
--
--
-- Problem
--
-- Many operations in Bitcoin Script were disabled by Satoshi Nakamoto in 2010.
--
-- For example, integer multiplication.
--
-- This limits what smart contracts we can develop for Bitcoin.
--
--
--
--
--
--
--
--
--
--
--
--
--
--
--
-- Motivation
--
-- If I were designing a programming langauge for Bitcoin, what would it be like?
--
-- * Create an expressive language that lets users build novel programs and smart
-- contracts.
--
-- * Enable useful static analysis to bound computational resource usage of programs.
--
-- * Provide formal semantics for reasoning using off-the-shelf proof-assistant
-- software.
--
-- I call my new langauge, Simplicity.
--
--
--
--
--
--
--
--
module Simplicity where
-- Simplicity is a combinator based, typed, functional programming langauge
--
-- Simplicity has 3 kinds of type
-- * The unit type: 𝟙
-- * Product types: A × B
-- * Sum types: A ⊎ B
--
-- Simplicity has no function types.
data 𝟙 : Set where
⟨⟩ : 𝟙
infix 40 _×_
data _×_ (A B : Set) : Set where
⟨_,_⟩ : A → B → A × B
infix 30 _⊎_
data _⊎_ (A B : Set) : Set where
σᴸ : A → A ⊎ B
σᴿ : B → A ⊎ B
-- Every Simplicity expression, t, denotes a function from a Simplicity type to a Simplicity type.
--
-- We write t : A ⊢ B
--
_⊢_ : Set → Set → Set
A ⊢ B = A → B
-- Simplicity expressions always denotes functions and cannot express values.
-- The core Simplicity language consists of nine combinators.
-- The iden expression denotes the identity function
iden : ∀ {A}
-----
→ A ⊢ A
iden = λ z → z
-- The comp combinator composes Simplicity expressions
comp : ∀ {A B C}
→ A ⊢ B
→ B ⊢ C
-----
→ A ⊢ C
comp s t = λ x → t ( s x)
-- The unit expression returns the value of the unit type.
unit : ∀ {A}
-----
→ A ⊢ 𝟙
unit = λ _ → ⟨⟩
-- The pair combinator combines the results of two function on the same input.
pair : ∀ {A B C}
→ A ⊢ B
→ A ⊢ C
---------
→ A ⊢ B × C
pair s t = λ z → ⟨ s z , t z ⟩
-- The take combinator evalutes a function on the first component of a pair.
take : ∀ {A B C}
→ A ⊢ C
---------
→ A × B ⊢ C
take t = λ { ⟨ x , y ⟩ → t x }
-- The drop combinator evaluates a function on the second component of a pair.
drop : ∀ {A B C}
→ B ⊢ C
---------
→ A × B ⊢ C
drop t = λ { ⟨ x , y ⟩ → t y }
-- The injl combinator tags the result of a function with a σᴸ tag.
injl : ∀ {A B C}
→ A ⊢ B
---------
→ A ⊢ B ⊎ C
injl t = λ z → σᴸ (t z)
-- The injr combinator tags the result of a function with a σᴿ tag.
injr : ∀ {A B C}
→ A ⊢ C
---------
→ A ⊢ B ⊎ C
injr t = λ z → σᴿ (t z)
-- The case combinator evalutes of of two functions depending on the tag of
-- the first component of the input.
case : ∀ {A B C D}
→ A × C ⊢ D
→ B × C ⊢ D
---------------
→ (A ⊎ B) × C ⊢ D
case s t = λ { ⟨ σᴸ a , c ⟩ → s ⟨ a , c ⟩
; ⟨ σᴿ b , c ⟩ → t ⟨ b , c ⟩
}
--
-- Simplicity isn't meant to be directly programmed in,
-- but we are going to do that anyways.
--
𝟚 = 𝟙 ⊎ 𝟙
true : ∀ {A}
-----
→ A ⊢ 𝟚
true = injr unit
false : ∀ {A}
-----
→ A ⊢ 𝟚
false = injl unit
infix 30 _▵_
_▵_ = pair
infixr 20 _⨾_
_⨾_ = comp
not : 𝟚 ⊢ 𝟚
not = iden ▵ unit
⨾ case true false
or : 𝟚 × 𝟚 ⊢ 𝟚
or = case (drop iden) true
import Data.Nat
open Data.Nat
word-2^ : ℕ → Set
word-2^ zero = 𝟚
word-2^ (suc n) = word-2^ n × word-2^ n
adder : 𝟚 × 𝟚 ⊢ word-2^ 1
adder = case (drop (false ▵ iden)) (drop (iden ▵ not))
fulladder : (𝟚 × 𝟚) × 𝟚 ⊢ word-2^ 1
fulladder = take adder ▵ drop iden
⨾ take (take iden) ▵ (take (drop iden) ▵ drop iden ⨾ adder)
⨾ (take iden ▵ drop (take iden) ⨾ or) ▵ drop (drop iden)
import Relation.Binary.PropositionalEquality
open Relation.Binary.PropositionalEquality
⌈_⌉ : ∀ {n} → word-2^ n → ℕ
⌈_⌉ {zero} (σᴸ x) = 0
⌈_⌉ {zero} (σᴿ x) = 1
⌈_⌉ {suc n} ⟨ xhi , xlo ⟩ = ⌈ xhi ⌉ * 2 ^ (2 ^ n) + ⌈ xlo ⌉
fulladder-correct : ∀ a b c → ⌈ a ⌉ + ⌈ b ⌉ + ⌈ c ⌉ ≡ ⌈ fulladder ⟨ ⟨ a , b ⟩ , c ⟩ ⌉
fulladder-correct (σᴸ x) (σᴸ x₁) c = refl
fulladder-correct (σᴸ x) (σᴿ x₁) (σᴸ x₂) = refl
fulladder-correct (σᴸ x) (σᴿ x₁) (σᴿ x₂) = refl
fulladder-correct (σᴿ x) (σᴸ x₁) (σᴸ x₂) = refl
fulladder-correct (σᴿ x) (σᴸ x₁) (σᴿ x₂) = refl
fulladder-correct (σᴿ x) (σᴿ x₁) c = refl
fulladder-word : ∀ {n}
-------------------------------------------
→ (word-2^ n × word-2^ n) × 𝟚 ⊢ 𝟚 × word-2^ n
fulladder-word {zero} = fulladder
fulladder-word {suc n} = take (take (take iden) ▵ drop (take iden))
▵ (take (take (drop iden) ▵ drop (drop iden)) ▵ drop iden
⨾ fulladder-word)
⨾ (take iden ▵ drop (take iden) ⨾ fulladder-word)
▵ drop (drop iden)
⨾ take (take iden) ▵ (take (drop iden) ▵ drop iden)
open ≡-Reasoning
import Data.Nat.Properties
open Data.Nat.Properties
open SemiringSolver
⌈_⌉₁ : ∀ {n} → 𝟚 × word-2^ n → ℕ
⌈_⌉₁ {n} ⟨ c , y ⟩ = ⌈ c ⌉ * 2 ^ (2 ^ n) + ⌈ y ⌉
fulladder-word-correct : ∀ {n} → (a b : word-2^ n) → (c : 𝟚)
→ ⌈ a ⌉ + ⌈ b ⌉ + ⌈ c ⌉ ≡ ⌈ fulladder-word (⟨ ⟨ a , b ⟩ , c ⟩) ⌉₁
fulladder-word-correct {zero} a b c = fulladder-correct a b c
fulladder-word-correct {suc n} ⟨ ahi , alo ⟩ ⟨ bhi , blo ⟩ c
with fulladder-word ⟨ ⟨ alo , blo ⟩ , c ⟩
| inspect fulladder-word ⟨ ⟨ alo , blo ⟩ , c ⟩
fulladder-word-correct {suc n} ⟨ ahi , alo ⟩ ⟨ bhi , blo ⟩ c | ⟨ c₁ , rlo ⟩ | [ eq₁ ]
with fulladder-word ⟨ ⟨ ahi , bhi ⟩ , c₁ ⟩
| inspect fulladder-word ⟨ ⟨ ahi , bhi ⟩ , c₁ ⟩
fulladder-word-correct {suc n} ⟨ ahi , alo ⟩ ⟨ bhi , blo ⟩ c | ⟨ c₁ , rlo ⟩ | [ eq₁ ]
| ⟨ c₂ , rhi ⟩ | [ eq₂ ] =
begin
⌈ ahi ⌉ * (2 ^ (2 ^ n)) + ⌈ alo ⌉ +
(⌈ bhi ⌉ * (2 ^ (2 ^ n)) + ⌈ blo ⌉)
+ ⌈ c ⌉
≡⟨ solve 6
(λ ah al bh bl c₃ z →
ah :* z :+ al :+ (bh :* z :+ bl) :+ c₃ :=
(ah :+ bh) :* z :+ (al :+ bl :+ c₃))
refl ⌈ ahi ⌉ ⌈ alo ⌉ ⌈ bhi ⌉ ⌈ blo ⌉ ⌈ c ⌉ (2 ^ (2 ^ n)) ⟩
(⌈ ahi ⌉ + ⌈ bhi ⌉) * (2 ^ (2 ^ n)) +
( ⌈ alo ⌉ + ⌈ blo ⌉ + ⌈ c ⌉)
≡⟨ cong (λ x → (⌈ ahi ⌉ + ⌈ bhi ⌉) * (2 ^ (2 ^ n)) + x) (fulladder-word-correct alo blo c) ⟩
(⌈ ahi ⌉ + ⌈ bhi ⌉) * (2 ^ (2 ^ n)) +
( ⌈ fulladder-word ⟨ ⟨ alo , blo ⟩ , c ⟩ ⌉₁)
≡⟨ cong (λ x → (⌈ ahi ⌉ + ⌈ bhi ⌉) * (2 ^ (2 ^ n)) + ⌈ x ⌉₁) eq₁ ⟩
(⌈ ahi ⌉ + ⌈ bhi ⌉) * (2 ^ (2 ^ n)) +
( ⌈ ⟨ c₁ , rlo ⟩ ⌉₁)
≡⟨⟩
(⌈ ahi ⌉ + ⌈ bhi ⌉) * (2 ^ (2 ^ n)) +
( ⌈ c₁ ⌉ * 2 ^ (2 ^ n) + ⌈ rlo ⌉)
≡⟨ solve 5
(λ ah bh rl c₃ z →
(ah :+ bh) :* z :+ (c₃ :* z :+ rl) := (ah :+ bh :+ c₃) :* z :+ rl)
refl ⌈ ahi ⌉ ⌈ bhi ⌉ ⌈ rlo ⌉ ⌈ c₁ ⌉ (2 ^ (2 ^ n)) ⟩
(⌈ ahi ⌉ + ⌈ bhi ⌉ + ⌈ c₁ ⌉) * (2 ^ (2 ^ n)) + ⌈ rlo ⌉
≡⟨ cong (λ x → x * (2 ^ (2 ^ n)) + ⌈ rlo ⌉) (fulladder-word-correct ahi bhi c₁) ⟩
(⌈ fulladder-word ⟨ ⟨ ahi , bhi ⟩ , c₁ ⟩ ⌉₁) * (2 ^ (2 ^ n)) + ⌈ rlo ⌉
≡⟨ cong (λ x → ⌈ x ⌉₁ * (2 ^ (2 ^ n)) + ⌈ rlo ⌉) eq₂ ⟩
(⌈ c₂ ⌉ * 2 ^ (2 ^ n) + ⌈ rhi ⌉) * (2 ^ (2 ^ n)) + ⌈ rlo ⌉
≡⟨ reasons ⟩
⌈ c₂ ⌉ * (2 ^ ((2 ^ n) + ((2 ^ n) + zero))) +
(⌈ rhi ⌉ * (2 ^ (2 ^ n)) + ⌈ rlo ⌉)
∎
where
reasons = trans (solve 4
(λ rh rl c₃ z →
(c₃ :* z :+ rh) :* z :+ rl := c₃ :* (z :* z) :+ (rh :* z :+ rl))
refl ⌈ rhi ⌉ ⌈ rlo ⌉ ⌈ c₂ ⌉ (2 ^ (2 ^ n))) (cong (λ x → ⌈ c₂ ⌉ * x + (⌈ rhi ⌉ * (2 ^ (2 ^ n)) + ⌈ rlo ⌉))
(trans
(sym (^-distribˡ-+-* 2 (2 ^ n) (2 ^ n)))
(cong (λ x → 2 ^ ((2 ^ n) + x)) (sym (+-identityʳ (2 ^ n))))))
--
--
-- Thank You!
--
-- A Coq implementation and Haskell implementation can be found at
--
-- ⟨ https://github.com/ElementsProject/simplicity ⟩
--
--
-------------- next part --------------
--
--
--
--
--
--
--
-- Simplicity for Programable Money
--
-- Russell O'Connor (Blockstream)
--
-- November 17th, 2018
--
-- Scale by the Bay
--
--
--
--
--
--
--
--
--
--
-- Background
--
-- * In Bitcoin funds are guarded by small programs written in Bitcoin Script.
--
-- * A typical program in Bitcoin script validates a digital signature to authorize a transaction.
--
-- * Other, more complex, programs allow one to create "smart contracts":
--
-- + Cross-chain atomic transactions
--
-- + Hash Time-lock Contracts
--
-- + Bi-directional payment channels
--
-- + Lightning Network
--
-- + and more.
--
-- * Bitcoin is programable money.
--
--
--
-- Bitcoin Script
--
-- * Stack machine without looping instructions
--
-- * Enables static analysis
--
-- + You can bound the maximum number of each operation that will be evaluated.
--
-- + Bitcoin rejects programs that have too many, expensive, signature verification
-- operations.
--
-- * Allows caching of results
--
-- + Evaluation depends only on the transaction data.
--
-- + If the Bitcoin Script is successful, that result holds no matter where the
-- transaction is added to the blockchain.
--
--
--
--
--
-- Problem
--
-- Many operations in Bitcoin Script were disabled by Satoshi Nakamoto in 2010.
--
-- For example, integer multiplication.
--
-- This limits what smart contracts we can develop for Bitcoin.
--
--
--
--
--
--
--
--
--
--
--
--
--
--
--
-- Motivation
--
-- If I were designing a programming langauge for Bitcoin, what would it be like?
--
-- * Create an expressive language that lets users build novel programs and smart
-- contracts.
--
-- * Enable useful static analysis to bound computational resource usage of programs.
--
-- * Provide formal semantics for reasoning using off-the-shelf proof-assistant
-- software.
--
-- I call my new langauge, Simplicity.
--
--
--
--
--
--
--
--
module Simplicity where
-- Simplicity is a combinator based, typed, functional programming langauge
--
-- Simplicity has 3 kinds of type
-- * The unit type: 𝟙
-- * Product types: A × B
-- * Sum types: A ⊎ B
--
-- Simplicity has no function types.
data 𝟙 : Set where
⟨⟩ : 𝟙
infix 40 _×_
data _×_ (A B : Set) : Set where
⟨_,_⟩ : A → B → A × B
infix 30 _⊎_
data _⊎_ (A B : Set) : Set where
σᴸ : A → A ⊎ B
σᴿ : B → A ⊎ B
-- Every Simplicity expression, t, denotes a function from a Simplicity type to a Simplicity type.
--
-- We write t : A ⊢ B
--
_⊢_ : Set → Set → Set
A ⊢ B = A → B
-- Simplicity expressions always denotes functions and cannot express values.
-- The core Simplicity language consists of nine combinators.
-- The iden expression denotes the identity function
iden : ∀ {A}
-----
→ A ⊢ A
iden = {!!}
-- The comp combinator composes Simplicity expressions
comp : ∀ {A B C}
→ A ⊢ B
→ B ⊢ C
-----
→ A ⊢ C
comp s t = {!!}
-- The unit expression returns the value of the unit type.
unit : ∀ {A}
-----
→ A ⊢ 𝟙
unit = {!!}
-- The pair combinator combines the results of two function on the same input.
pair : ∀ {A B C}
→ A ⊢ B
→ A ⊢ C
---------
→ A ⊢ B × C
pair s t = {!!}
-- The take combinator evalutes a function on the first component of a pair.
take : ∀ {A B C}
→ A ⊢ C
---------
→ A × B ⊢ C
take t = {!!}
-- The drop combinator evaluates a function on the second component of a pair.
drop : ∀ {A B C}
→ B ⊢ C
---------
→ A × B ⊢ C
drop t = {!!}
-- The injl combinator tags the result of a function with a σᴸ tag.
injl : ∀ {A B C}
→ A ⊢ B
---------
→ A ⊢ B ⊎ C
injl t = {!!}
-- The injr combinator tags the result of a function with a σᴿ tag.
injr : ∀ {A B C}
→ A ⊢ C
---------
→ A ⊢ B ⊎ C
injr t = {!!}
-- The case combinator evalutes of of two functions depending on the tag of
-- the first component of the input.
case : ∀ {A B C D}
→ A × C ⊢ D
→ B × C ⊢ D
---------------
→ (A ⊎ B) × C ⊢ D
case s t = {!!}
--
-- Simplicity isn't meant to be directly programmed in,
-- but we are going to do that anyways.
--
𝟚 = 𝟙 ⊎ 𝟙
true : ∀ {A}
-----
→ A ⊢ 𝟚
true = {!!}
false : ∀ {A}
-----
→ A ⊢ 𝟚
false = {!!}
infix 30 _▵_
_▵_ = pair
infixr 20 _⨾_
_⨾_ = comp
not : 𝟚 ⊢ 𝟚
not = {!!}
or : 𝟚 × 𝟚 ⊢ 𝟚
or = {!!}
import Data.Nat
open Data.Nat
word-2^ : ℕ → Set
word-2^ zero = 𝟚
word-2^ (suc n) = word-2^ n × word-2^ n
adder : 𝟚 × 𝟚 ⊢ word-2^ 1
adder = {!case (drop (false ▵ iden)) (drop (iden ▵ not))!}
fulladder : (𝟚 × 𝟚) × 𝟚 ⊢ word-2^ 1
fulladder = {!take adder ▵ drop iden!}
⨾ {!take (take iden) ▵ (take (drop iden) ▵ drop iden ⨾ adder)!}
⨾ {!(take iden ▵ drop (take iden) ⨾ or) ▵ drop (drop iden)!}
import Relation.Binary.PropositionalEquality
open Relation.Binary.PropositionalEquality
⌈_⌉ : ∀ {n} → word-2^ n → ℕ
⌈_⌉ {n} w = {!!}
fulladder-correct : ∀ a b c → ⌈ a ⌉ + ⌈ b ⌉ + ⌈ c ⌉ ≡ ⌈ fulladder ⟨ ⟨ a , b ⟩ , c ⟩ ⌉
fulladder-correct a b c = {!!}
fulladder-word : ∀ {n}
-------------------------------------------
→ (word-2^ n × word-2^ n) × 𝟚 ⊢ 𝟚 × word-2^ n
fulladder-word {zero} = fulladder
fulladder-word {suc n} = {!take (take (take iden) ▵ drop (take iden))
▵ (take (take (drop iden) ▵ drop (drop iden)) ▵ drop iden
⨾ fulladder-word)!}
⨾ {!(take iden ▵ drop (take iden) ⨾ fulladder-word)
▵ drop (drop iden)!}
⨾ {!take (take iden) ▵ (take (drop iden) ▵ drop iden)!}
open ≡-Reasoning
import Data.Nat.Properties
open Data.Nat.Properties
open SemiringSolver
⌈_⌉₁ : ∀ {n} → 𝟚 × word-2^ n → ℕ
⌈_⌉₁ {n} ⟨ c , y ⟩ = {!⌈ c ⌉ * 2 ^ (2 ^ n) + ⌈ y ⌉!}
fulladder-word-correct : ∀ {n} → (a b : word-2^ n) → (c : 𝟚)
→ ⌈ a ⌉ + ⌈ b ⌉ + ⌈ c ⌉ ≡ ⌈ fulladder-word (⟨ ⟨ a , b ⟩ , c ⟩) ⌉₁
fulladder-word-correct {zero} a b c = fulladder-correct a b c
fulladder-word-correct {suc n} ⟨ ahi , alo ⟩ ⟨ bhi , blo ⟩ c
with fulladder-word ⟨ ⟨ alo , blo ⟩ , c ⟩
| inspect fulladder-word ⟨ ⟨ alo , blo ⟩ , c ⟩
fulladder-word-correct {suc n} ⟨ ahi , alo ⟩ ⟨ bhi , blo ⟩ c | ⟨ c₁ , rlo ⟩ | [ eq₁ ]
with fulladder-word ⟨ ⟨ ahi , bhi ⟩ , c₁ ⟩
| inspect fulladder-word ⟨ ⟨ ahi , bhi ⟩ , c₁ ⟩
fulladder-word-correct {suc n} ⟨ ahi , alo ⟩ ⟨ bhi , blo ⟩ c | ⟨ c₁ , rlo ⟩ | [ eq₁ ]
| ⟨ c₂ , rhi ⟩ | [ eq₂ ] = {!!}
-- ≡⟨ solve 5
-- (λ ah bh rl c₃ z →
-- (ah :+ bh) :* z :+ (c₃ :* z :+ rl) := (ah :+ bh :+ c₃) :* z :+ rl)
-- refl ⌈ ahi ⌉ ⌈ bhi ⌉ ⌈ rlo ⌉ ⌈ c₁ ⌉ (2 ^ (2 ^ n)) ⟩
-- where
-- reasons = trans (solve 4
-- (λ rh rl c₃ z →
-- (c₃ :* z :+ rh) :* z :+ rl := c₃ :* (z :* z) :+ (rh :* z :+ rl))
-- refl ⌈ rhi ⌉ ⌈ rlo ⌉ ⌈ c₂ ⌉ (2 ^ (2 ^ n))) (cong (λ x → ⌈ c₂ ⌉ * x + (⌈ rhi ⌉ * (2 ^ (2 ^ n)) + ⌈ rlo ⌉))
-- (trans
-- (sym (^-distribˡ-+-* 2 (2 ^ n) (2 ^ n)))
-- (cong (λ x → 2 ^ ((2 ^ n) + x)) (sym (+-identityʳ (2 ^ n))))))
-- --
-- --
-- -- Thank You!
-- --
-- -- A Coq implementation and Haskell implementation can be found at
-- --
-- -- ⟨ https://github.com/ElementsProject/simplicity ⟩
-- --
-- --
-- -- Cheat:
-- --
-- -- begin
-- -- ⌈ ahi ⌉ * (2 ^ (2 ^ n)) + ⌈ alo ⌉ +
-- -- (⌈ bhi ⌉ * (2 ^ (2 ^ n)) + ⌈ blo ⌉)
-- -- + ⌈ c ⌉
-- -- ≡⟨ solve 6
-- -- (λ ah al bh bl c₃ z →
-- -- ah :* z :+ al :+ (bh :* z :+ bl) :+ c₃ :=
-- -- (ah :+ bh) :* z :+ (al :+ bl :+ c₃))
-- -- refl ⌈ ahi ⌉ ⌈ alo ⌉ ⌈ bhi ⌉ ⌈ blo ⌉ ⌈ c ⌉ (2 ^ (2 ^ n)) ⟩
-- -- (⌈ ahi ⌉ + ⌈ bhi ⌉) * (2 ^ (2 ^ n)) +
-- -- ( ⌈ alo ⌉ + ⌈ blo ⌉ + ⌈ c ⌉ )
-- -- ≡⟨ cong (λ x → (⌈ ahi ⌉ + ⌈ bhi ⌉) * (2 ^ (2 ^ n)) + x)
-- -- (fulladder-word-correct alo blo c) ⟩
-- -- (⌈ ahi ⌉ + ⌈ bhi ⌉) * (2 ^ (2 ^ n)) +
-- -- ( ⌈ fulladder-word ⟨ ⟨ alo , blo ⟩ , c ⟩ ⌉₁ )
-- -- ≡⟨ cong (λ x → (⌈ ahi ⌉ + ⌈ bhi ⌉) * (2 ^ (2 ^ n)) + ⌈ x ⌉₁) eq₁ ⟩
-- -- (⌈ ahi ⌉ + ⌈ bhi ⌉) * (2 ^ (2 ^ n)) +
-- -- ( ⌈ ⟨ c₁ , rlo ⟩ ⌉₁ )
-- -- ≡⟨⟩
-- -- (⌈ ahi ⌉ + ⌈ bhi ⌉) * (2 ^ (2 ^ n)) +
-- -- ( ⌈ c₁ ⌉ * 2 ^ (2 ^ n) + ⌈ rlo ⌉ )
-- -- ≡⟨ solve 5
-- -- (λ ah bh rl c₃ z →
-- -- (ah :+ bh) :* z :+ (c₃ :* z :+ rl) := (ah :+ bh :+ c₃) :* z :+ rl)
-- -- refl ⌈ ahi ⌉ ⌈ bhi ⌉ ⌈ rlo ⌉ ⌈ c₁ ⌉ (2 ^ (2 ^ n)) ⟩
-- -- (⌈ ahi ⌉ + ⌈ bhi ⌉ + ⌈ c₁ ⌉) * (2 ^ (2 ^ n)) + ⌈ rlo ⌉
-- -- ≡⟨ cong (λ x → x * (2 ^ (2 ^ n)) + ⌈ rlo ⌉) (fulladder-word-correct ahi bhi c₁) ⟩
-- -- (⌈ fulladder-word ⟨ ⟨ ahi , bhi ⟩ , c₁ ⟩ ⌉₁ ) * (2 ^ (2 ^ n)) + ⌈ rlo ⌉
-- -- ≡⟨ cong (λ x → ⌈ x ⌉₁ * (2 ^ (2 ^ n)) + ⌈ rlo ⌉) eq₂ ⟩
-- -- (⌈ c₂ ⌉ * (2 ^ (2 ^ n)) + ⌈ rhi ⌉ ) * (2 ^ (2 ^ n)) + ⌈ rlo ⌉
-- -- ≡⟨ reasons ⟩
-- -- ⌈ c₂ ⌉ * (2 ^ ((2 ^ n) + ((2 ^ n) + zero))) +
-- -- (⌈ rhi ⌉ * (2 ^ (2 ^ n)) + ⌈ rlo ⌉)
-- -- ∎
-- -- where
-- -- reasons = trans (solve 4
-- -- (λ rh rl c₃ z →
-- -- (c₃ :* z :+ rh) :* z :+ rl := c₃ :* (z :* z) :+ (rh :* z :+ rl))
-- -- refl ⌈ rhi ⌉ ⌈ rlo ⌉ ⌈ c₂ ⌉ (2 ^ (2 ^ n))) (cong (λ x → ⌈ c₂ ⌉ * x + (⌈ rhi ⌉ * (2 ^ (2 ^ n)) + ⌈ rlo ⌉))
-- -- (trans
-- -- (sym (^-distribˡ-+-* 2 (2 ^ n) (2 ^ n)))
-- -- (cong (λ x → 2 ^ ((2 ^ n) + x)) (sym (+-identityʳ (2 ^ n))))))
More information about the Simplicity
mailing list