Skip to content

Extend input declarations in Z# to support structs#218

Closed
lorenzorota wants to merge 0 commit intocircify:masterfrom
lorenzorota:master
Closed

Extend input declarations in Z# to support structs#218
lorenzorota wants to merge 0 commit intocircify:masterfrom
lorenzorota:master

Conversation

@lorenzorota
Copy link
Contributor

Currently, program inputs cannot be declared for structs that are being returned. Take the following program

struct Pt {
    field x
    field y
}
struct Pts {
    Pt[2] pts
}

def main(private Pts[1] pts) -> Pt:
    return Pt {x: pts[0].pts[0].x * pts[0].pts[1].x, y: pts[0].pts[0].y * pts[0].pts[1].y}

with the value maps

(set_default_modulus 52435875175126190479447740508185965837690552500527637822603658699938581184513
(let (
    (pts.0.pts.0.x #f2)
    (pts.0.pts.0.y #f4)
    (pts.0.pts.1.x #f2)
    (pts.0.pts.1.y #f4)
) true ;ignored
)
)

and

(set_default_modulus 52435875175126190479447740508185965837690552500527637822603658699938581184513
(let (
    (return.x #f4)
    (return.y #f16)
) true ;ignored
)
)

for the prover and verifier, respectively. This would throw a not implemented error since precomputations are not handled.

This PR adds the missing precomputations, similar to how it's done for arrays and mutable arrays, i.e., computing the precomputations by unwrapping all the struct fields. For this I included two new functions in T: unwrap_struct and unwrap_struct_ir, which both return a FieldList or an error.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant