Our strategy for compiling equality constraints is to first transform the two source expres-sions in an equality constraint into their corresponding R1CS constraints (including the type constraints), then assert the two resulting vector of variables to solve to the same values.
Suppose that we have an equality constraint between the two Source expressions Ind refl (3∷ []) and Add (Lit 5) (Mul (Lit 6) (Ind refl (7 ∷ []))) of type Source ‘Base. We would transform the literals into Inds by applying varEqLit recursively, and the resulting Inds would then be pieced together with additive constraints for the additive expressions, multiplicative constraints for the multiplicative expressions, and finally the equality con-straint for the equality of the two Source expressions. In the cases other than equality constraints over ‘Base, we would add the corresponding type constraints for Inds with indToIR and assert that the resulting variable of indToIR solves to 1 to make sure that the vector of variables in the Inds are representations of a literal of the same type.
First we define the function sourceToR1CS that transforms source expressions into R1CS. In the case of literals, we transform them into R1CS variables with litToInd by first
allocating a new R1CS variable vector, and then asserting that the literal and the vector of R1CS variables are “equal” (with varEqLit).
Definition 5.7.1 (litToInd).
litToInd : ∀ (u : U) → ⟦ u ⟧ → SI-Monad (Vec Var (tySize u)) litToInd u l = do
vec ← newVarVec (tySize u)
add (Hint (litEqVecHint u l vec)) r ← varEqLit u vec l
assertTrue r return vec
The main compilation function sourceToR1CS is then defined as follows:
Definition 5.7.2 (sourceToR1CS).
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 ∷ [])
With the sourceToR1CS function defined, what is left is of compiling equality con-straints is to assert the two components of the equality concon-straints to solve to the same values. We define the following function assertVarEqVar to do so.
Definition 5.7.3 (assertVarEqVar).
assertVarEqVar : ∀ (n : ℕ) → Vec Var n → Vec Var n → SI-Monad ⊤ assertVarEqVar .0 [] [] = return tt
assertVarEqVar .(suc _) (x ∷ v₁) (x₁ ∷ v₂) = do add (IAdd zero ((one , x) ∷ (- one , x₁) ∷ [])) assertVarEqVar _ v₁ v₂
These components are then composed together into compAssert and compAssertsHints.
Definition 5.7.4 (compAssert).
compAssert : (∃ (λ u → Source u × Source u)) → SI-Monad ⊤ compAssert (u , s₁ , s₂) = do
r₁ ← sourceToR1CS u s₁ r₂ ← sourceToR1CS u s₂ assertVarEqVar _ r₁ r₂
Definition 5.7.5 (compAssertsHints).
compAssertsHints :
List (∃ (λ u → Source u × Source u)
⊎ (M.Map Var ℕ → M.Map Var ℕ))
→ SI-Monad ⊤
compAssertsHints [] = return tt compAssertsHints (inj₁ x ∷ ls) = do
compAssert x
compAssertsHints ls
compAssertsHints (inj₂ y ∷ ls) = do add (Hint y)
compAssertsHints ls
The whole compilation process is then combined together with compileSource.
Definition 5.7.6 (compileSource).
compileSource : ∀ (n : ℕ) (u : U) → (S-Monad (Source u))
→ Var × List R1CS × (Vec Var (tySize u) × List ℕ) compileSource n u source =
let v , (asserts , input) , output = source (tt , 1) ((v' , (cs₁ , cs₂) , outputVars) , inv) = (do
compAssertsHints (asserts [])
sourceToR1CS _ output) ((NormalMode , n) , v) in v' , cs₁ ++ cs₂ , outputVars , input []
Chapter 6
Formal Verification of the Compiler
In this chapter, we will describe how the translational soundness of the compiler is proved.
There are two parts to the translational correctness of a compiler: soundness and complete-ness. Soundness is the property that if the generated constraints are satisfiable, then the solution must be correct, and completeness is the property that the generated constraints are satisfiable. We will only be proving the soundness of the compiler in this thesis.
Recall that in the compilation pipeline, we first execute a program written in S-Monad with some initial states, then the result is piped into assertVarEqVar and sourceToR1CS to generate the corresponding R1CS constraints. In this chapter, we will describe the formal verification of the soundness of the main compilation functions in detail.
Given functionsℕtoF : ℕ → f and fToℕ : f → ℕ, the soundness of the compiler is proved under the following conditions:
1. _≟F_ : Decidable {A = f} _≡_
2. _≟U_ : ∀ {u} → Decidable {A = ⟦ u ⟧} _≡_
3. field’ : Field f
4. isField : IsField f field’
5. finite : Finite f
6. ℕtoF-1≡1 : ℕtoF 1 ≡ onef
7. ℕtoF-0≡0 : ℕtoF 0 ≡ zerof
8. ℕtoF∘fToℕ≡ : ∀ x → ℕtoF (fToℕ x) ≡ x 9. prime : ℕ
10. isPrime : Prime prime 11. onef≠zerof :¬ onef ≡ zerof
12. The functionℕtoF is additively and multiplicatively homomorphic. i.e.
(a) ℕtoF-+hom : ∀ x y → ℕtoF (x + y) ≡ (ℕtoF x) + (ℕtoF y) (b) ℕtoF-*hom : ∀ x y → ℕtoF (x * y) ≡ (ℕtoF x) * (ℕtoF y)
where isPrime is a proof that prime is indeed a prime number, onef is the multiplicative identity in field’, and zerof is the additive identity in field’.
A solution to a set of R1CS constraints is defined as a partial map List (Var ×ℕ) that maps variables to their corresponding values. Because the variables are mapped to natural numbers, it is necessary to have conversion functions (fToℕ : f → ℕ) (ℕtoF : ℕ → f) in order to define what it means to say that a List (Var ×ℕ) is a solution to an R1CS constraint.
Before we define the soundness of sourceToR1CS, we need a couple of auxiliary defi-nitions, including a semantic function on Source expressions, a lookup relation for R1CS variables in a partial map, and a value representation relation between a literal and a vec-tor of natural numbers representing prime field elements. Our sourceToR1CS soundness lemma says that given a solution sol to the constraints generated by sourceToR1CS, then under good enough conditions, the result of the semantic function coincides (meaning that they are related by the value representation relation) with the solution of the vector of variables generated by sourceToR1CS in sol.
Since we are using natural numbers to represent prime field elements, we first define the following equivalence relation _≈_ that “quotients” elements that are mapped to the same values by the functionℕtoF. This relation will then be used to define the solution relation for a partial map of type List (Var ×ℕ) to be considered a solution of an R1CS constraint.
Definition 6.0.1 (_≈_). _≈_ is the equivalence relation naturally induced by the function ℕtoF.
_≈_ : ℕ → ℕ → Prop
x ≈ y = Squash (ℕtoF x ≡ ℕtoF y)
_≈_ is an equivalence relation since the underlying propositional equality is an equiv-alence relation:
≈-refl : ∀ {n} → n ≈ n
≈-sym : ∀ {m n} → m ≈ n → n ≈ m
≈-trans : ∀ {m n o} → m ≈ n → n ≈ o → m ≈ o
With _≈_ defined, next we define the lookup relation of one or more variables for a partial map of type List (Var ×ℕ).
Definition 6.0.2 (ListLookup).
data ListLookup : Var → List (Var × ℕ) → ℕ → Prop where LookupHere : ∀ v l n n' → n ≈ n'
→ ListLookup v ((v , n) ∷ l) n' LookupThere : ∀ v l n t
→ ListLookup v l n → ¬ v ≡ proj₁ t
→ ListLookup v (t ∷ l) n
Given a variable v : Var, a partial map sol : List (Var × ℕ), and a value n : ℕ, ListLookup v sol n holds if the first occurrence of v in sol maps to n. We generalize the above relation from a single variable to a vector of variables with the following relation BatchListLookup.
Definition 6.0.3 (BatchListLookup).
data BatchListLookup : {n : ℕ} → Vec Var n → List (Var × ℕ)
→ Vec ℕ n → Prop where
BatchLookupNil : ∀ l → BatchListLookup [] l []
BatchLookupCons : ∀ {len} v n (vec₁ : Vec Var len) vec₂ l
→ ListLookup v l n
→ BatchListLookup vec₁ l vec₂
→ BatchListLookup (v ∷ vec₁) l (n ∷ vec₂)
Recall from the definition of R1CS in Chapter 2 that an R1CS constraint is either an additive constraint (IAdd), a multiplicative constraint (IMul), a Hint, or a Log. We define a partial map sol : List (Var ×ℕ) to be a solution to an additive constraint IAdd f1 ((f2, i2)
∷ (f3, i3) ... ∷ []) if after looking up the variables i2, i3, ... in sol, the linear combination sums to zero (in the finite field). The solution of a multiplicative constraint is defined similarly. For the cases Hint and Log, we define any partial map sol : List (Var ×ℕ) to be a solution of a Hint or a Log since they are not actual constraints. This is formally defined with the Agda definitions in the following section.
6.1 Solution of R1CS Constraints
Given a partial map sol : List (Var ×ℕ) and a linear combination of variables List (f × Var), the value of the linear combination is defined with the following relation LinearCombVal.
Definition 6.1.1 (LinearCombVal).
data LinearCombVal (sol : List (Var × ℕ)) : List (f × Var) → f → Prop where
LinearCombValBase : LinearCombVal solution [] zerof LinearCombValCons : ∀ coeff var varVal {l} {acc}
→ ListLookup var solution varVal
→ LinearCombVal solution l acc
→ LinearCombVal solution ((coeff , var) ∷ l) ((coeff *F ℕtoF varVal) +F acc)
(where +F, *F are the additive and multiplicative field operations)
A List (Var ×ℕ) is a solution to an R1CS constraint if the following relation holds.
Definition 6.1.2 (R1CSSolution).
data R1CSSolution (solution : List (Var × ℕ)) : R1CS → Prop where
addSol : ∀ {coeff} {linComb} {linCombVal}
→ LinearCombVal solution linComb linCombVal
→ linCombVal +F coeff ≡ zerof
→ R1CSSolution solution (IAdd coeff linComb) multSol : ∀ a b bval c cval d e eval
→ ListLookup b solution bval
→ ListLookup c solution cval
→ ListLookup e solution eval
→ ((a *F (ℕtoF bval)) *F (ℕtoF cval))
≡ (d *F (ℕtoF eval))
→ R1CSSolution solution (IMul a b c d e) hintSol : ∀ f → R1CSSolution solution (Hint f) logSol : ∀ s → R1CSSolution solution (Log s)
Since the writer component of SI-Monad is defined as a pair of List R1CS, in order to facilitate the development of lemmas and proofs related to SI-Monad, we define the following relation ConstraintsSol that expresses the proposition that every constraint in xs ++ ys is satisfied by sol.
Definition 6.1.3 (ConstraintsSol).
ConstraintsSol :
List R1CS × List R1CS → List (Var × ℕ) → Prop ConstraintsSol (xs , ys) sol
= ∀ x → x ∈ (xs ++ ys) → R1CSSolution sol x
Next we define the low level representation of a literal in Source expressions. This rep-resentation relation is used in the main soundness lemma to relate the output of sourceToR1CS to the semantics function on Source (which will be defined later).