Skip to content

fix: constraint generation with duplicate variables #1801

@DavePearce

Description

@DavePearce

Summary

Constraint generation fails when there are multiple variables of the same name in the same function. This can happen in ZkC due to block scoping.

Example 1

Consider the following program:

fn f(x:u16){
   if x == 0 {
      var i:u16 = x+1
   } else {
      var i:u16 = x+2
   }
}

This generates the following constraints (which, as far as I am aware are correct, but could cause problems in e.g. the prover):

(module f)

(inputs
   (x u16 0x0)
)

(computed
   (i u16 0x0)
   (i u16 0x0)
   ($3 u0 0x0)
)


(vanish f:pc0
   (∧ (== $3 0)
      (if (== x $3)
         (== i (+ 1 x)))
      (if (!= x $3)
         (== i (+ 2 x)))))

Example 2

The following fails when generating AIR constraints specifically:

fn f(x:u16) -> (r:u16) {
    r = x
    //
    for i:u8 = 0; i<5; i = i + 1 {
        r = r + 1
    }
    //
    for i:u8 = 0; i<3; i = i + 1 {
        r = r + 2
    }
    //
}

This results in a panic: register "i" already declared error.

Metadata

Metadata

Assignees

No one assigned

    Labels

    bugSomething isn't workingconstraintsIssues directly related to constraint generation.zkcIssues related to ZkC language

    Type

    No type
    No fields configured for issues without a type.

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions