Exposing vector_add to zok frontend

[edwjchen]

No description provided.

[kwantam]

A few comments so far. I'll have another look once you've got edits to the constant folder!

[kwantam]

I think if you're only going to support one type here it should be field, not u32.

[edwjchen]

I think only BV are currently supported in the FHE backend, which is why I left it as u32.

[kwantam]

Still, it might make sense to support all the basic types, no? It wouldn't be much extra work:

• add vadd_field, vadd_u64, vadd_u32, vadd_u16, vadd_u8 stubs in EMBED
• in builtin_call_, extend the current match clause to catch all of these
• extend the function in zsharp/term.rs to support both bitvector and field types
• the current constant folder may or may not work, but I bet there's a small edit distance to working if no

Since this is so simple, I don't see a reason to leave it half-done. But I could be missing something!

[edwjchen]

I see, updated!

[edwjchen]

@kwantam How would I evaluate the operation on va and vb without the recursive call to fold_cache here?

[kwantam]

High-level answer: the Op::Map(op) match clause starting on line 248 should push a new term onto the stack that is equivalent to the term containing the Op::Map(_), but which eliminates the map. I can give you more details later.

[kwantam]

a few more comments

[kwantam]

High-level answer: the Op::Map(op) match clause starting on line 248 should push a new term onto the stack that is equivalent to the term containing the Op::Map(_), but which eliminates the map. I can give you more details later.

[kwantam]

Sorry for the delay. I'll spend some time reviewing this today, I hope.

[kwantam]

I left a few comments. Happy to jump on a call and discuss in more detail. The upshot is, the functionality looks mostly right but what's currently implemented is unnecessarily inefficient.