Exposing vector_add to zok frontend #78
Conversation
kwantam
left a comment
kwantam
left a comment
There was a problem hiding this comment.
A few comments so far. I'll have another look once you've got edits to the constant folder!
| // vector functions | ||
| def vector_add<N>(u32[N] a, u32[N] b) -> u32[N]: | ||
| return [0; N] |
There was a problem hiding this comment.
I think if you're only going to support one type here it should be field, not u32.
There was a problem hiding this comment.
I think only BV are currently supported in the FHE backend, which is why I left it as u32.
There was a problem hiding this comment.
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.rsto 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!
src/ir/opt/cfold.rs
Outdated
| let mut new_map: BTreeMap<Value, Value> = BTreeMap::new(); | ||
| for (a_ind, a_val) in &a.map { | ||
| let b_val = &b.map[a_ind]; | ||
| let res = fold_cache( |
There was a problem hiding this comment.
@kwantam How would I evaluate the operation on va and vb without the recursive call to fold_cache here?
There was a problem hiding this comment.
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.
src/ir/opt/cfold.rs
Outdated
| let mut new_map: BTreeMap<Value, Value> = BTreeMap::new(); | ||
| for (a_ind, a_val) in &a.map { | ||
| let b_val = &b.map[a_ind]; | ||
| let res = fold_cache( |
There was a problem hiding this comment.
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.
|
Sorry for the delay. I'll spend some time reviewing this today, I hope. |
kwantam
left a comment
kwantam
left a comment
There was a problem hiding this comment.
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.
No description provided.