Theorem 6.4.1 (sourceToR1CSSound). Soundness of sourceToR1CS.
sourceToR1CSSound :
∀ (r : WriterMode) (u : U)
→ (s : Source u)
→ (sol : List (Var × ℕ))
→ ListLookup 0 sol 1
→ SourceStore sol u s
→ ∀ init →
let result = sourceToR1CS u s ((r , prime) , init) in ConstraintsSol (writerOutput result) sol
→ Squash (∃ (λ ⟦u⟧ → ∃ (λ val → ValRepr u ⟦u⟧ val × ∃ (λ ss →
Σ′ (sourceSem u s sol ss ≡ ⟦u⟧) (λ _ → BatchListLookup
(output result) sol val)))))
This lemma says that given a Source expression s : Source u and a partial map sol : List (Var ×N) such that
1. sol is a solution of the generated constraints from sourceToR1CS
2. The variable 0 maps to 1 in sol
3. SourceStore sol u s holds
then there is
⟦u⟧ : ⟦ u ⟧
val : Vec ℕ (tySize u)
ss : SourceStoreRepr store u s
such that the following diagram holds
s ⟦u⟧
out val
sourceSemss,sol
primary output (sourceToR1CS) V alRepr
BatchListLookupsol
for any initial state init.
The proof of sourceToR1CSSound follows the definition of sourceToR1CS. Recall the definition of sourceToR1CS from Chapter 5:
sourceToR1CS : ∀ (u : U) → Source u
→ SI-Monad (Vec Var (tySize u)) sourceToR1CS u (Ind refl x)
= withMode PostponedMode (indToIR u x) sourceToR1CS u (Lit x) = litToInd u x
sourceToR1CS `Base (Add source source₁) = do r₁ ← sourceToR1CS `Base source
r₂ ← sourceToR1CS `Base source₁ v ← new
add (IAdd zero ((one , head r₁) ∷
(one , head r₂) ∷ (- one , v) ∷ [])) return (v ∷ [])
sourceToR1CS `Base (Mul source source₁) = do r₁ ← sourceToR1CS `Base source
r₂ ← sourceToR1CS `Base source₁ v ← new
add (IMul one (head r₁) (head r₂) one v)
return (v ∷ [])
In the Ind case of sourceToR1CS, we want indToIR to generate the correct type con-straints for the R1CS variables, and in the Lit case of sourceToR1CS, we want litToInd to return R1CS variables that solve to the representation of the given literal. In the Add and Mul cases, sourceToR1CS is proved by straightforward induction on the Source expres-sion.
What does it mean to say that indToIR generates the correct type constraints? The type of indToIR is:
indToIR : ∀ (u : U)
→ Vec Var (tySize u)
→ SI-Monad (Vec Var (tySize u))
Given a type code u and a vector of variables vec, we want indToIR to generate enough constraints so that given a good enough solution sol : List (Var ×ℕ) to the constraints generated by indToIR u vec, vec solves to a representation of some elem : ⟦ u ⟧ in sol.
This is expressed as the following lemma:
Lemma 6.4.2 (indToIRSound). Soundness of indToIR.
indToIRSound :
∀ (r : WriterMode) (u : U)
→ (vec : Vec Var (tySize u))
→ (val : Vec ℕ (tySize u))
→ (sol : List (Var × ℕ))
→ BatchListLookup vec sol val
→ ListLookup 0 sol 1
→ ∀ init →
let result = indToIR u vec ((r , prime) , init) in ConstraintsSol (writerOutput result) sol
→ Squash (∃ (λ elem → ValRepr u elem val))
For litToInd, we want the constraints generated by litToInd u l to ensure that the vector of variables returned by litToInd u l solves to a representation of the literal l for any good enough solution sol : List (Var ×ℕ) to the generated constraints. This is expressed as the following lemma:
Lemma 6.4.3 (litToIndSound). Soundness of litToInd.
litToIndSound :
∀ (r : WriterMode) (u : U)
→ (elem : ⟦ u ⟧)
→ (sol : List (Var × ℕ))
→ ListLookup 0 sol 1
→ ∀ init →
let result = litToInd u elem ((r , prime) , init) in ConstraintsSol (writerOutput result) sol
→ Squash (∃ (λ val → Σ′ (ValRepr u elem val)
(λ _ → BatchListLookup (output result) sol val)))
In order to prove indToIRSound and litToIndSound, we proved that similar soundness properties hold for tyCond, varEqLit, and assertTrue, and to do so, we proved that similar soundness properties hold for the components (including land, lor, limp et cetera) used in the definition of tyCond, varEqLit, and assertTrue. Here we will give an example on what proving these soundness lemmas are like. Readers interested in the details on the lemmas used to prove indToIRSound and litToIndSound should check out Appendix B for a comprehensive view of the soundness lemmas and the auxiliary definitions used to define and prove these soundness lemmas.
Take the following definition of limp from Chapter 5 for example:
limp : Var → Var → SI-Monad Var limp n₁ n₂ = do
notN₁ ← lnot n₁ lor notN₁ n₂
Given a solution sol to the constraints generated by limp n₁ n₂ such that n₁ maps to v₁ and n₂ maps to v₂ in sol and that v₁, v₂ ∈ {0, 1}, the variable that limp returns solves to 1 if v₁ → v₂ (material implication) holds. This is captured with the following definition:
limpSound : ∀ (r : WriterMode)
→ (n₁ n₂ : Var) → (v₁ v₂ : ℕ)
→ (sol : List (Var × ℕ))
→ ListLookup n₁ sol v₁
→ ListLookup n₂ sol v₂
→ isBool v₁ → isBool v₂
→ ∀ (init : ℕ) →
let result = limp n₁ n₂ ((r , prime) , init) in BuilderProdSol (writerOutput result) sol
→ ListLookup (output result) sol (limpFunc v₁ v₂)
where limpFunc a b evaluates to 0 if and only if a ≈ 1 and b ≈ 0 and isBool a holds if a ≈ 0 or a ≈ 1.
Since the inputs of limp solve to 0 or 1 in sol, the input condition for lnot is satisfied, and notN₁ must also solve to 0 or 1 in sol. Therefore, the input condition for lor (both input variables solve to 0 or 1 in sol) is satisfied, and the output variable solves to the result calculated by limpFunc (up to _≈_) in sol.
Chapter 7 Conclusion
In this thesis, I constructed and formally proved the soundness of a dependently typed verifiable computation compiler. By using a tarski style universe in the domain specific language, users are able to write dependently typed domain specific programs that can be directly type checked by the dependently typed language Agda. The result from the Agda programs can then be subsequently piped into the zkSNARK library libsnark to generate the corresponding cryptographic proof. Overall, this was an attempt that I undertook to construct and formally verify a compiler that compiles to rank 1 constraints.
Appendix A
Full Definition of enum
Definition A.0.1 (enum, enumComplete, FuncInstLem).
enum : (u : U) → List ⟦ u ⟧
enumComplete : ∀ (u : U) → (x : ⟦ u ⟧) → x ∈ enum u
enum `One = [ tt ]
enum `Two = false ∷ true ∷ []
enum `Base = Finite.elems finite enum (`Vec u zero) = [ [] ]
enum (`Vec u (suc x)) = do r ← enum u
rs ← enum (`Vec u x) return (r ∷ rs)
enum (`Σ u x) = do r ← enum u
rs ← enum (x r) return (r , rs) enum (`Π u x) =
let pairs = do
r ← enum u
return (r , enum (x r)) funcs = genFunc _ _ pairs
in listFuncToPi u x (enum u) (enumComplete u) funcs (λ x₁ x₁∈genFunc →
trans (genFuncProj₁ u x pairs x₁ x₁∈genFunc) (map-proj₁->>= (enum u) (enum ∘ x)))
FuncInstLem : ∀ u x (f : ⟦ `Π u x ⟧) (l : List ⟦ u ⟧)
→ FuncInst ⟦ u ⟧ (λ v → ⟦ x v ⟧) (piToList u x l f) (l >>= (λ r → (r , enum (x r)) ∷ []))
FuncInstLem u x f [] = InstNil FuncInstLem u x f (x₁ ∷ l)
= InstCons (piToList u x l f)
(l >>= (λ r → (r , enum (x r)) ∷ []))
x₁ (f x₁) (enum (x x₁)) (enumComplete (x x₁) (f x₁)) (FuncInstLem u x f l)
enumComplete `One tt = here refl enumComplete `Two false = here refl
enumComplete `Two true = there (here refl) enumComplete `Base x = Finite.a∈elems finite x enumComplete (`Vec u zero) [] = here refl
enumComplete (`Vec u (suc x₁)) (x ∷ x₂) =
∈l-∈l'-∈r (enum u) _∷_ x x₂ (enumComplete u x)
(λ _ → enum (`Vec u x₁)) (enumComplete (`Vec u x₁) x₂) enumComplete (`Σ u x₁) (fst , snd) =
∈l-∈l'-∈r (enum u) _,_ fst snd (enumComplete u fst) (λ r → enum (x₁ r)) (enumComplete (x₁ fst) snd) enumComplete (`Π u x₁) f =
let pairs = do r ← enum u
return (r , enum (x₁ r)) genFuncs = genFunc u x₁ pairs
fToList = piToList u x₁ (enum u) f fToListFuncInstPairs
= FuncInstLem u x₁ f (enum u) fToList∈genFuncs
= FuncInst→genFunc u x₁ pairs fToList fToListFuncInstPairs prf = trans
(genFuncProj₁ u x₁ pairs
fToList fToList∈genFuncs) (map-proj₁->>= (enum u)
(λ x₂ → enum (x₁ x₂))) f≗piFromList∘piToList
= piFromList∘piToList≗id u x₁
(enum u) (enumComplete u) f prf in f∈listFuncToPi u x₁ _ _ genFuncs fToList _
f fToList∈genFuncs
(ext f≗piFromList∘piToList)
where ext is the principle of function extensionality, and trans is transitivity for proposi-tional equality.
The reasoning for the Π case of enumComplete is that since enum (‘Π u x) is defined with listFuncToPi, we show that f :⟦ ‘Π u x ⟧ when transformed into fToList with piToList, must be a member of genFuncs, and that piFromList∘piToList is the identity function.
Appendix B
Additional Formal Verification Lemmas and Definitions
Definition B.0.1 (Vec-≈).
data Vec-≈ : ∀ {n} → Vec ℕ n → Vec ℕ n → Prop where
≈-Nil : Vec-≈ [] []
≈-Cons : ∀ {n} x y {l : Vec ℕ n} {l'} → x ≈ y
→ Vec-≈ l l'
→ Vec-≈ (x ∷ l) (y ∷ l')
Definition B.0.2 (isBool).
data isBool : ℕ → Set where
isZero : ∀ n → ℕtoF n ≡ zerof → isBool n isOne : ∀ n → ℕtoF n ≡ onef → isBool n
isBool n says thatℕtoF n is either 1 or 0. If isBool n holds for some (n : ℕ), then n is said to be boolean.
Definition B.0.3 (isBoolStrict).
data isBoolStrict : ℕ → Set where
isZeroS : ∀ {n} → n ≡ 0 → isBoolStrict n isOneS : ∀ {n} → n ≡ 1 → isBoolStrict n
isBoolStrict n says that n is either 1 or 0. If isBoolStrict n holds for some (n : ℕ), then n is said to be strictly boolean.
The following lemma says that if a natural number n is strictly boolean, then n is boolean:
Lemma B.0.1 (isBoolStrict→isBool).
isBoolStrict→isBool : ∀ {n} → isBoolStrict n → isBool n
Proof. Immediate from definition of isBoolStrict.
Lemma B.0.2 (addSound). addSound says that if there is a solution sol to the constraints
generated by add ir, then sol must be a solution to ir.
addSound : ∀ (r : WriterMode)
→ (ir : R1CS)
→ (sol : List (Var × ℕ))
→ ∀ (init : ℕ) →
let result = add ir ((r , prime) , init) in ConstraintsSol (writerOutput result) sol
→ R1CSSolution sol ir
Proof. Since add ir adds ir to the resulting contraints, any solution to the constraints gen-erated by add ir must satisfy ir.
Lemma B.0.3 (assertTrueSound). assertTrueSound says that if there is a solution sol to
the constraints generated by assertTrue v, then v is mapped to 1 in sol.
assertTrueSound : ∀ (r : WriterMode)
→ ∀ (v : Var) → (sol : List (Var × ℕ))
→ ∀ (init : ℕ) →
let result = assertTrue v ((r , prime) , init) in
ConstraintsSol (writerOutput result) sol
→ ListLookup v sol 1
Proof. By addSound.
In order to give specifications to the logical functions, functions like the following neqzFunc are defined:
Definition B.0.4 (neqzFunc). Specification of neqz.
neqzFunc : ℕ → ℕ
neqzFunc n with ℕtoF n ≟F zerof neqzFunc n | yes p = 0
neqzFunc n | no ¬p = 1
The following two lemmas are immediate from the definition of neqzFunc:
neqzFuncIsBoolStrict says that neqzFunc n is strictly boolean for all n : ℕ.
Lemma B.0.4 (neqzFuncIsBoolStrict).
neqzFuncIsBoolStrict : ∀ n → isBoolStrict (neqzFunc n)
neqzFuncIsBool says that neqzFunc n is boolean for all n : ℕ.
Lemma B.0.5 (neqzFuncIsBool).
neqzFuncIsBool : ∀ n → isBool (neqzFunc n)
Since neqz is constructed with add, we prove the soundness of neqz with respect to neqzFunc by first applying addSound, then we apply the reasoning in Section 5.4 on neqz:
Lemma B.0.6 (neqzSound).
neqzSound : ∀ (r : WriterMode)
→ ∀ (v : Var) → (val : ℕ) → (sol : List (Var × ℕ))
→ ListLookup v sol val
→ ∀ (init : ℕ) →
let result = neqz v ((r , prime) , init) in ConstraintsSol (writerOutput result) sol
→ ListLookup (output result) sol (neqzFunc val)
Similarly, we proved that neqzIsBool solves to zero or one given a solution map that satisfies the constraints generated by neqz v by applying addSound and some simple field arithmetic:
Lemma B.0.7 (neqzIsBool).
neqzIsBool : ∀ (r : WriterMode)
→ (v : Var)
→ (sol : List (Var × ℕ))
→ ∀ init →
let result = neqz v ((r , prime) , init) in ConstraintsSol (writerOutput result) sol
→ Squash (∃ (λ val → Σ′ (isBool val)
(λ _ → ListLookup (output result) sol val)))
This is the leitmotif of the proofs of these lemmas: first we try to obtain the soundness proofs of the underlying components, then we apply a higher level reasoning that uses the subcomponents as basic building blocks.
The following lemma says that given a solution sol to the constraints generated by neqz v such that neqz outputs a variable that solves to 0 in sol, the input variable must solve to 0 in sol:
Lemma B.0.8 (neqzSound₀).
neqzSound₀ : ∀ (r : WriterMode)
→ (v : Var)
→ (sol : List (Var × ℕ))
→ ListLookup 0 sol 1
→ ∀ init →
let result = neqz v ((r , prime) , init) in ConstraintsSol (writerOutput result) sol
→ ListLookup (output result) sol 0
→ Squash (∃ (λ val → (Σ′′ (ListLookup v sol val) (λ _ → 0 ≈ val))))
By applying similar techniques, we can prove that other basic components used in the construction of the compiler are well-behaved when the generated constraints are satisfi-able.
Definition B.0.5 (lorFunc). Specification of lor.
lorFunc : ℕ → ℕ → ℕ
lorFunc a b with ℕtoF a ≟F zerof
lorFunc a b | yes p with ℕtoF b ≟F zerof lorFunc a b | yes p | yes p₁ = 0
lorFunc a b | yes p | no ¬p = 1 lorFunc a b | no ¬p = 1
Lemma B.0.9 (lorFuncIsBoolStrict).
lorFuncIsBoolStrict : ∀ a b → isBoolStrict (lorFunc a b)
Lemma B.0.10 (lorFuncIsBool).
lorFuncIsBool : ∀ a b → isBool (lorFunc a b)
With the specification defined, we proved that lor is sound with respect to lorFunc when the input variables are mapped to boolean values in the solution.
Lemma B.0.11 (lorSound).
lorSound : ∀ (r : WriterMode)
→ (v v' : Var) → (val val' : ℕ)
→ (sol : List (Var × ℕ))
→ ListLookup v sol val
→ ListLookup v' sol val'
→ isBool val → isBool val'
→ ∀ (init : ℕ) →
let result = lor v v' ((r , prime) , init) in ConstraintsSol (writerOutput result) sol
→ ListLookup (output result) sol (lorFunc val val')
Given a solution sol to the constraints generated by lor v v’, if the output variable of lorFunc solves to 0, and both inputs to lor solve to boolean values, then it must be the case that both input variables solve to 0:
Lemma B.0.12 (lorSound₀).
lorSound₀ : ∀ (r : WriterMode)
→ (v v' : Var) (val val' : ℕ)
→ (sol : List (Var × ℕ))
→ ∀ init
→ ListLookup v sol val
→ ListLookup v' sol val'
→ isBool val
→ isBool val' →
let result = lor v v' ((r , prime) , init) in ConstraintsSol (writerOutput result) sol
→ ListLookup (output result) sol 0
→ Squash (Σ′′ (ListLookup v sol 0)
(λ _ → ListLookup v' sol 0))
Similarly, for the logical and gate, we can define the following specification:
Definition B.0.6 (landFunc). Specification of land.
landFunc : ℕ → ℕ → ℕ
landFunc a b with ℕtoF a ≟F zerof landFunc a b | yes p = 0
landFunc a b | no ¬p with ℕtoF b ≟F zerof
landFunc a b | no ¬p | yes p = 0 landFunc a b | no ¬p | no ¬p₁ = 1
Suppose that landFunc a b outputs 1, and that isBoolStrict a holds, then a must be propositionally equal to 1.
Lemma B.0.13 (landFunc⁻₁).
landFunc⁻₁ : ∀ {a} {b}
→ isBoolStrict a → landFunc a b ≡ 1 → a ≡ 1
Suppose that landFunc a b outputs 1, and that isBoolStrict b holds, then b must be propositionally equal to 1.
Lemma B.0.14 (landFunc⁻₂).
landFunc⁻₂ : ∀ {a} {b}
→ isBoolStrict b → landFunc a b ≡ 1 → b ≡ 1
For arbitrary (a b : ℕ), landFunc a b is strictly boolean.
Lemma B.0.15 (landFuncIsBoolStrict).
landFuncIsBoolStrict : ∀ a b → isBoolStrict (landFunc a b)
For arbitrary (a b : ℕ), landFunc a b is boolean.
Lemma B.0.16 (landFuncIsBool).
landFuncIsBool : ∀ a b → isBool (landFunc a b)
We proved that given a solution sol to the constraints generated by land v v’ such that the variable 0 maps to 1, and that both inputs to land solve to boolean values, then the output of land also solves to a boolean value.
Lemma B.0.17 (landIsBool).
landIsBool : ∀ r v v' sol val val'
→ ListLookup v sol val
→ ListLookup v' sol val'
→ isBool val
→ isBool val'
→ ListLookup 0 sol 1
→ ∀ init →
let result = land v v' ((r , prime) , init) in ConstraintsSol (writerOutput result) sol
→ Squash (∃ (λ val'' → Σ′ (isBool val'')
(λ _ → ListLookup (output result) sol val'')))
The following lemma says that land is sound with respect to its specification landFunc when the input variables map to boolean values in the solution:
Lemma B.0.18 (landSound).
landSound : ∀ (r : WriterMode)
→ (v v' : Var) → (val val' : ℕ)
→ (sol : List (Var × ℕ))
→ ListLookup v sol val
→ ListLookup v' sol val'
→ isBool val → isBool val'
→ ∀ (init : ℕ) →
let result = land v v' ((r , prime) , init) in ConstraintsSol (writerOutput result) sol
→ ListLookup (output result) sol (landFunc val val')
landSound₁, proved with landSound and addSound, says that given a solution sol to the constraints generated by land v v’ such that the output variable of land solves to 1, and that both input variables are boolean in sol, then it must be the case that both inputs solve to 1 in sol.
Lemma B.0.19 (landSound₁).
landSound₁ : ∀ (r : WriterMode)
→ (v v' : Var) (val val' : ℕ)
→ (sol : List (Var × ℕ))
→ ∀ init
→ ListLookup v sol val
→ ListLookup v' sol val'
→ isBool val
→ isBool val' →
let result = land v v' ((r , prime) , init) in ConstraintsSol (writerOutput result) sol
→ ListLookup (output result) sol 1
→ Squash (Σ′′ (ListLookup v sol 1)
(λ _ → ListLookup v' sol 1))
Similar to the case of lor and land, we define and prove similar lemmas for the other components used in the compiler:
Definition B.0.7 (lnotFunc). Specification of lnot.
lnotFunc : ℕ → ℕ
lnotFunc a with ℕtoF a ≟F zerof lnotFunc a | yes p = 1
lnotFunc a | no ¬p = 0
lnotFuncIsBoolStrict says that for any (n : ℕ), lnotFunc n is strictly boolean.
Lemma B.0.20 (lnotFuncIsBoolStrict).
lnotFuncIsBoolStrict : ∀ n → isBoolStrict (lnotFunc n)
For any (n : ℕ), lnotFunc n is boolean:
Lemma B.0.21 (lnotFuncIsBool).
lnotFuncIsBool : ∀ n → isBool (lnotFunc n)
lnotSound says that lnot is sound with respect to the specification lnotFunc when the input variable to lnot maps to a boolean in the solution.
Lemma B.0.22 (lnotSound).
lnotSound : ∀ (r : WriterMode)
→ (v : Var) → (val : ℕ)
→ (sol : List (Var × ℕ))
→ ListLookup v sol val
→ isBool val
→ ∀ (init : ℕ) →
let result = lnot v ((r , prime) , init) in ConstraintsSol (writerOutput result) sol
→ ListLookup (output result) sol (lnotFunc val)
lnotSound₁ says that given a solution sol to the constraints generated by lnot v, if the output variable of lnot solves to 1 in sol, then the input variable solves to 0 in sol.
Lemma B.0.23 (lnotSound₁).
lnotSound₁ : ∀ (r : WriterMode) v val sol init
→ ListLookup v sol val
→ isBool val →
let result = lnot v ((r , prime) , init) in ConstraintsSol (writerOutput result) sol
→ ListLookup (output result) sol 1
→ ListLookup v sol 0
Definition B.0.8 (limpFunc). Specification of limp.
limpFunc : ℕ → ℕ → ℕ
limpFunc a b = lorFunc (lnotFunc a) b
Lemma B.0.24 (limpFuncImp).
limpFuncImp : ∀ {a} {b} → a ≡ 1
→ isBoolStrict b → limpFunc a b ≡ 1 → b ≡ 1
limpFuncIsBool says that for any (a b : ℕ), limpFunc a b must be boolean.
Lemma B.0.25 (limpFuncIsBool).
limpFuncIsBool : ∀ a b → isBool (limpFunc a b)
limpFuncIsBoolStrict says that for any (a b : ℕ), limpFunc a b must be strictly boolean.
Lemma B.0.26 (limpFuncIsBoolStrict).
limpFuncIsBoolStrict : ∀ a b → isBoolStrict (limpFunc a b)
Soundness of the logical implication gate given a solution sol to the constraints generated by limp v v’ that maps input variables to boolean:
Lemma B.0.27 (limpSound).
limpSound : ∀ (r : WriterMode)
→ (v v' : Var) → (val val' : ℕ)
→ (sol : List (Var × ℕ))
→ ListLookup v sol val
→ ListLookup v' sol val'
→ isBool val → isBool val'
→ ∀ (init : ℕ) →
let result = limp v v' ((r , prime) , init) in ConstraintsSol (writerOutput result) sol
→ ListLookup (output result) sol (limpFunc val val')
anyNeqzIsBool says that given a solution sol to the constraints generated by anyNeqz vec, it must be the case that the output variable is boolean.
Lemma B.0.28 (anyNeqzIsBool).
anyNeqzIsBool : ∀ r {n} (vec : Vec Var n) sol init
→ let result = anyNeqz vec ((r , prime) , init) in ConstraintsSol (writerOutput result) sol
→ Squash (∃ (λ val → Σ′ (isBool val)
(λ _ → ListLookup (output result) sol val)))
anyNeqzSound₀ says that given a solution sol to the constraints generated by anyNeqz vec such that 0 maps to 1 in sol, and that the output variable solves to 0, then it must be the case that the input variables all solve to 0.
Lemma B.0.29 (anyNeqzSound₀).
anyNeqzSound₀ : ∀ (r : WriterMode)
→ ∀ {n} → (vec : Vec Var n)
→ (sol : List (Var × ℕ))
→ ListLookup 0 sol 1
→ ∀ init →
let result = anyNeqz vec ((r , prime) , init) in ConstraintsSol (writerOutput result) sol
→ ListLookup (output result) sol 0
→ Squash (∃ (λ val → (Σ′′ (BatchListLookup vec sol val) (λ _ → All (_≈_ 0) val))))
where All is the usual inductively defined predicate that says that all elements in the given vector satisfies the given predicate:
data All {A : Set} (P : A → Prop) : ∀ {n} → Vec A n → Prop where [] : All P []
_∷_ : ∀ {n x} {xs : Vec A n} (px : P x) (pxs : All P xs) → All P (x ∷ xs)
Definition B.0.9 (varEqBaseLitFunc). Specification of varEqBaseLit
varEqBaseLitFunc : ℕ → f → ℕ
varEqBaseLitFunc v l with ℕtoF v ≟F l varEqBaseLitFunc v l | yes p = 1
varEqBaseLitFunc v l | no ¬p = 0
varEqBaseLitSound says that varEqBaseLit is sound with respect to the specification varEqBaseLitFunc if the input variable to varEqBaseLit is mapped to something in the solution.
Lemma B.0.30 (varEqBaseLitSound).
varEqBaseLitSound : ∀ (r : WriterMode)
→ (v : Var) → (val : ℕ) → (l : f)
→ (sol : List (Var × ℕ))
→ ListLookup v sol val
→ ∀ (init : ℕ) →
let result = varEqBaseLit v l ((r , prime) , init) in ConstraintsSol (writerOutput result) sol
→ ListLookup (output result) sol (varEqBaseLitFunc val l)
varEqBaseLitSound₁ says that given a solution sol to the constraints generated by varEqBaseLit v l that maps 0 to 1, and that the output variable of varEqBaseLit solves to 1, then it must be the case that the input variable to varEqBaseLit maps to l:
Lemma B.0.31 (varEqBaseLitSound₁).
varEqBaseLitSound₁ : ∀ (r : WriterMode)
→ (v : Var) (l : f)
→ (sol : List (Var × ℕ))
→ ListLookup 0 sol 1
→ ∀ init →
let result = varEqBaseLit v l ((r , prime) , init) in ConstraintsSol (writerOutput result) sol
→ ListLookup (output result) sol 1
→ Squash (∃ (λ val → Σ′ (ℕtoF val ≡ l) (λ _ → ListLookup v sol val)))
varEqBaseLitSound₁ r v l sol tri init isSol look
Proof. Recall the definition of varEqBaseList:
varEqBaseLit : Var → f → SI-Monad Var varEqBaseLit n l = do
n-l ← new
add (IAdd (- l) ((one , n) ∷ (- one , n-l) ∷ []))
¬r ← neqz n-l r ← lnot ¬r return r
Given a solution sol to the constraints generated by varEqBaseLit v l such that 0 maps to 1 in sol, by neqzIsBool, lnotSound₁, and neqzSound₀, n-l solves to 0 in sol. By addSound, n solves to l in sol.
varEqBaseLitIsBool says that given a solution sol to the constraints generated by varE-qBaseLit v l, it must be the case that the output variable of varEvarE-qBaseLit maps to a boolean value.
Lemma B.0.32 (varEqBaseLitIsBool).
varEqBaseLitIsBool : ∀ r (v : Var) (l : f)
→ ∀ sol init →
let result = varEqBaseLit v l ((r , prime) , init) in ConstraintsSol (writerOutput result) sol
→ Squash (∃ (λ val → Σ′ (isBool val)
(λ _ → ListLookup (output result) sol val)))
Proof. By neqzIsBool, lnotFuncIsBool, and lnotSound.
Definition B.0.10 (anyNeqzFunc). Specification of anyNeqz.
anyNeqzFunc : ∀ {n} → Vec ℕ n → ℕ anyNeqzFunc [] = 0
anyNeqzFunc (x ∷ vec) with ℕtoF x ≟F zerof
anyNeqzFunc (x ∷ vec) | yes p = anyNeqzFunc vec anyNeqzFunc (x ∷ vec) | no ¬p = 1
anyNeqzFuncIsBool says that anyNeqzFunc vec is boolean for any vector vec.
Lemma B.0.33 (anyNeqzFuncIsBool).
anyNeqzFuncIsBool : ∀ {n} (vec : Vec ℕ n)
→ isBool (anyNeqzFunc vec)
anyNeqzFuncIsBoolStrict says that anyNeqzFunc vec is strictly boolean for any vector vec.
Lemma B.0.34 (anyNeqzFuncIsBoolStrict).
anyNeqzFuncIsBoolStrict : ∀ {n} (vec : Vec ℕ n)
→ isBoolStrict (anyNeqzFunc vec)
anyNeqzSound says that given a solution sol to the constraints generated by anyNeqz vec, and that the input vector vec solves to valVec in sol, then it must be the case that the output variable solves to anyNeqzFunc valVec in sol.
Lemma B.0.35 (anyNeqzSound).
anyNeqzSound : ∀ (r : WriterMode)
→ ∀ {n}
→ (vec : Vec Var n) → (valVec : Vec ℕ n)
→ (sol : List (Var × ℕ))
→ BatchListLookup vec sol valVec
→ ∀ (init : ℕ) →
let result = anyNeqz vec ((r , prime) , init) in ConstraintsSol (writerOutput result) sol
→ ListLookup (output result) sol (anyNeqzFunc valVec)
Definition B.0.11 (allEqzFunc).
allEqzFunc : ∀ {n} → Vec ℕ n → ℕ allEqzFunc [] = 1
allEqzFunc (x ∷ vec) with ℕtoF x ≟F zerof allEqzFunc (x ∷ vec) | yes p = allEqzFunc vec allEqzFunc (x ∷ vec) | no ¬p = 0
allEqzFuncIsBool says that allEqzFunc vec is boolean for all vec : Vecℕ n.
Lemma B.0.36 (allEqzFuncIsBool).
allEqzFuncIsBool : ∀ {n} (vec : Vec ℕ n)
→ isBool (allEqzFunc vec)
allEqzFuncIsBoolStrict says that allEqzFunc vec is strictly boolean for all vec : Vecℕ n.
Lemma B.0.37 (allEqzFuncIsBoolStrict).
allEqzFuncIsBoolStrict : ∀ {n} (vec : Vec ℕ n)
→ isBoolStrict (allEqzFunc vec)
allEqzIsBool says that given a solution sol to the constraints generated by allEqz vec that maps 0 to 1, the output variable of allEqz solves to a booelan value.
Lemma B.0.38 (allEqzIsBool).
allEqzIsBool : ∀ (r : WriterMode)
→ ∀ {n} → (vec : Vec Var n)
→ (sol : List (Var × ℕ))
→ ListLookup 0 sol 1
→ ∀ init →
let result = allEqz vec ((r , prime) , init) in ConstraintsSol (writerOutput result) sol
→ Squash (∃ (λ val → Σ′ (isBool val)
(λ _ → ListLookup (output result) sol val)))
Proof. Recall the definition of allEqz:
allEqz : ∀ {n} → Vec Var n → SI-Monad Var allEqz vec = do
¬r ← anyNeqz vec r ← lnot ¬r
return r
Given a solution sol to the constraints generated by allEqz vec such that 0 is mapped to 1 in sol, by anyNeqzIsBool and lnotSound, r solves to the result specified by lnotFunc in sol. The desired result can then be obtained by applying lnotFuncIsBool.
allEqzSound says that given a solution sol to the constraints generated by allEqz vec such that the input variables map to valVec, then it must be the case that the output variable solves to allEqzFunc valVec.
Lemma B.0.39 (allEqzSound).
allEqzSound : ∀ (r : WriterMode)
→ ∀ {n}
→ (vec : Vec Var n) → (valVec : Vec ℕ n)
→ (sol : List (Var × ℕ))
→ BatchListLookup vec sol valVec
→ ∀ (init : ℕ) →
let result = allEqz vec ((r , prime) , init)
in ConstraintsSol (writerOutput result) sol
→ ListLookup (output result) sol (allEqzFunc valVec)
allEqzSound₁ says that given a solution sol to the constraints generated by allEqz vec such that 0 maps to 1 in sol, and that the output variable solves to 1, then it must be the case that the entries in the input vector all solve to 0.
Lemma B.0.40 (allEqzSound₁).
allEqzSound₁ : ∀ (r : WriterMode)
→ ∀ {n} → (vec : Vec Var n)
→ (sol : List (Var × ℕ))
→ ListLookup 0 sol 1
→ ∀ init →
let result = allEqz vec ((r , prime) , init) in ConstraintsSol (writerOutput result) sol
→ ListLookup (output result) sol 1
→ Squash (∃ (λ val → (Σ′′ (BatchListLookup vec sol val) (λ _ → All (_≈_ 0) val))))
Proof. Recall the definition of allEqz:
allEqz : ∀ {n} → Vec Var n → SI-Monad Var allEqz vec = do
¬r ← anyNeqz vec r ← lnot ¬r
return r
Given a solution sol to the constraints generated by allEqz vec such that 0 maps to 1 in sol, by anyNeqzIsBool and lnotSound₁, we get that ¬r solves to 0. Then by anyNeqzSound₀, vec solves to the 0 vector.
Definition B.0.12 (piVarEqLitFunc, varEqLitFunc). Specification of piVarEqLit and varE-qLit.
piVarEqLitFunc : ∀ {u} (x : ⟦ u ⟧ → U) → (eu : List ⟦ u ⟧)
→ (vec : Vec ℕ (tySumOver eu x))
→ ⟦ `Π u x ⟧ → ℕ
varEqLitFunc : ∀ u → Vec ℕ (tySize u) → ⟦ u ⟧ → ℕ varEqLitFunc `One (x ∷ vec) lit with ℕtoF x ≟F zerof varEqLitFunc `One (x ∷ vec) lit | yes p = 1
varEqLitFunc `One (x ∷ vec) lit | no ¬p = 0
varEqLitFunc `Two (x ∷ vec) false with ℕtoF x ≟F zerof varEqLitFunc `Two (x ∷ vec) false | yes p = 1
varEqLitFunc `Two (x ∷ vec) false | no ¬p = 0
varEqLitFunc `Two (x ∷ vec) true with ℕtoF x ≟F onef varEqLitFunc `Two (x ∷ vec) true | yes p = 1
varEqLitFunc `Two (x ∷ vec) true | no ¬p = 0
varEqLitFunc `Base (x ∷ vec) lit with ℕtoF x ≟F lit varEqLitFunc `Base (x ∷ vec) lit | yes p = 1
varEqLitFunc `Base (x ∷ vec) lit | no ¬p = 0 varEqLitFunc (`Vec u zero) vec lit = 1
varEqLitFunc (`Vec u (suc x)) vec (l ∷ lit) with splitAt (tySize u) vec
... | fst , snd = landFunc (varEqLitFunc u fst l) (varEqLitFunc (`Vec u x) snd lit) varEqLitFunc (`Σ u x) vec (fstₗ , sndₗ)
with splitAt (tySize u) vec
... | fst , snd with maxTySplit u fstₗ x snd ... | vecₜ₁ , vecₜ₂
= landFunc (landFunc
(varEqLitFunc u fst fstₗ)
(varEqLitFunc (x fstₗ) vecₜ₁ sndₗ)) (allEqzFunc vecₜ₂)
varEqLitFunc (`Π u x) vec lit
= piVarEqLitFunc x (enum u) vec lit
piVarEqLitFunc x [] vec pi = 1 piVarEqLitFunc x (x₁ ∷ eu) vec pi
with splitAt (tySize (x x₁)) vec ... | fst , snd
= landFunc (varEqLitFunc (x x₁) fst (pi x₁)) (piVarEqLitFunc x eu snd pi)
varEqLitFuncIsBoolStrict and piVarEqLitFuncIsBoolStrict say that varEqLitFunc and piVarEqLitFunc produce values that are strictly boolean.
Lemma B.0.41 (varEqLitFuncIsBoolStrict, piVarEqLitFuncIsBoolStrict).
varEqLitFuncIsBoolStrict : ∀ u vec v
→ isBoolStrict (varEqLitFunc u vec v) piVarEqLitFuncIsBoolStrict :
∀ {u} (x : ⟦ u ⟧ → U) eu vec pi
→ isBoolStrict (piVarEqLitFunc x eu vec pi)
varEqLitFuncIsBool and piVarEqLitFuncIsBool say that varEqLitFunc and piVarE-qLitFunc produce values that are strictly boolean.
Lemma B.0.42 (varEqLitFuncIsBool, piVarEqLitFuncIsBool).
varEqLitFuncIsBool : ∀ u vec v
→ isBool (varEqLitFunc u vec v)
piVarEqLitFuncIsBool : ∀ {u} (x : ⟦ u ⟧ → U) eu vec pi
→ isBool (piVarEqLitFunc x eu vec pi)
varEqLitSound says that given a solution sol to the constraints generated by varEqLit u vec l such that 0 maps to 1 in sol and that the input variable vector vec maps to val, then
the output variable solves to the value specified by varEqLitFunc. piVarEqLitSound says that given a solution sol to the constraints generated by piVarEqLit that maps 0 to 1 and vec to val, the output variable solves to the value specified by piVarEqLitFunc.
Lemma B.0.43 (varEqLitSound, piVarEqLitSound).
varEqLitSound : ∀ (r : WriterMode)
→ ∀ u → (vec : Vec Var (tySize u))
→ (val : Vec Var (tySize u))
→ (l : ⟦ u ⟧)
→ (sol : List (Var × ℕ))
→ BatchListLookup vec sol val
→ ListLookup 0 sol 1
→ ∀ (init : ℕ) → let result
= varEqLit u vec l ((r , prime) , init) in ConstraintsSol (writerOutput result) sol
→ ListLookup (output result) sol (varEqLitFunc u val l)
piVarEqLitSound : ∀ (r : WriterMode)
→ ∀ u (x : ⟦ u ⟧ → U) (eu : List ⟦ u ⟧)
→ (vec : Vec Var (tySumOver eu x))
→ (val : Vec ℕ (tySumOver eu x))
→ (pi : ⟦ `Π u x ⟧)
→ (sol : List (Var × ℕ))
→ BatchListLookup vec sol val
→ ListLookup 0 sol 1
→ ∀ (init : ℕ) →
let result = piVarEqLit u x eu vec pi ((r , prime) , init) in ConstraintsSol (writerOutput result) sol
→ ListLookup (output result)
sol (piVarEqLitFunc x eu val pi)
piVarEqLitIsBool and varEqLitIsBool say that the respective output variables solve to boolean values given a solution sol satisfying the corresponding generated constraints that maps 0 to 1.
Lemma B.0.44 (piVarEqLitIsBool, varEqLitIsBool).
piVarEqLitIsBool : ∀ (r : WriterMode)
→ ∀ u x eu vec f sol
→ ListLookup 0 sol 1
→ ∀ init →
let result = piVarEqLit u x eu vec f ((r , prime) , init) in ConstraintsSol (writerOutput result) sol
→ Squash (∃ (λ val → Σ′ (isBool val)
(λ _ → ListLookup (output result) sol val)))
varEqLitIsBool : ∀ (r : WriterMode)
→ ∀ u → (vec : Vec Var (tySize u))
→ (l : ⟦ u ⟧)
→ (sol : List (Var × ℕ))
→ ListLookup 0 sol 1
→ ∀ init →
let result = varEqLit u vec l ((r , prime) , init) in ConstraintsSol (writerOutput result) sol
→ Squash (∃ (λ val → Σ′ (isBool val)
(λ _ → ListLookup (output result) sol val))) Lemma B.0.45 (varEqLitSound₁, piVarEqLitSound₁).
varEqLitSound₁ : ∀ (r : WriterMode)
→ ∀ u → (vec : Vec Var (tySize u))
→ (l : ⟦ u ⟧)
→ (sol : List (Var × ℕ))
→ ListLookup 0 sol 1
→ ∀ init →
let result = varEqLit u vec l ((r , prime) , init) in ConstraintsSol (writerOutput result) sol
→ ListLookup (output result) sol 1
→ Squash (∃ (λ val → Σ′ (ValRepr u l val) (λ _ → BatchListLookup vec sol val)))
piVarEqLitSound₁ : ∀ (r : WriterMode)
→ ∀ u x eu vec f sol
→ ListLookup 0 sol 1
→ ∀ init → let result
= piVarEqLit u x eu vec f ((r , prime) , init) in ConstraintsSol (writerOutput result) sol
→ ListLookup (output result) sol 1
→ Squash (∃ (λ val → Σ′ (PiRepr u x f eu val) (λ _ → BatchListLookup vec sol val)))
Definition B.0.13 (tyCondFunc, enumSigmaCondFunc, enumPiCondFunc).
Specifica-tion of tyCond, enumSigmaCond and enumPiCond.
tyCondFunc : ∀ u → (vec : Vec ℕ (tySize u)) → ℕ enumSigmaCondFunc : ∀ u → (eu : List ⟦ u ⟧)
→ (x : ⟦ u ⟧ → U)
→ (val₁ : Vec ℕ (tySize u))
→ (val₂ : Vec ℕ (maxTySizeOver (enum u) x))
→ ℕ
enumPiCondFunc : ∀ u → (eu : List ⟦ u ⟧) → (x : ⟦ u ⟧ → U)
→ Vec ℕ (tySumOver eu x) → ℕ
tyCondFunc `One (x ∷ vec) with ℕtoF x ≟F zerof tyCondFunc `One (x ∷ vec) | yes p = 1
tyCondFunc `One (x ∷ vec) | no ¬p = 0
tyCondFunc `Two (x ∷ vec) with ℕtoF x ≟F zerof tyCondFunc `Two (x ∷ vec) | yes p = 1
tyCondFunc `Two (x ∷ vec) | no ¬p with ℕtoF x ≟F onef tyCondFunc `Two (x ∷ vec) | no ¬p | yes p = 1
tyCondFunc `Two (x ∷ vec) | no ¬p with ℕtoF x ≟F onef tyCondFunc `Two (x ∷ vec) | no ¬p | yes p = 1