search

zetzit / zz

🍺🐙 ZetZ a zymbolic verifier and tranzpiler to bare metal C
MIT License
1.6k stars 52 forks source link

borrow() implementation #68

Closed jwerle closed 4 years ago

jwerle commented 4 years ago

I am not sure I have fully understood how this works yet. I can see that: if a module exports a borrow function, it will automatically be called during compilation triggering any theories attached to it. Is that correct? Does that make sense?

aep commented 4 years ago

yeah. Their intent is to carry a bunch of clauses that are automatically checked whenever a pointer is passed. Unfortunately it's pretty terrible due to lack of infrastructure for what "borrow" actually is. I'll have to do that first before this feature becomes useful.

jwerle commented 4 years ago

Seems powerful. I've brushed up against the borrow() implementation for the slice module (Slice and MutSlice). Finally grok'd last night

aep commented 4 years ago

yeah it will be pretty good once it works. but right now i don't recommend using it because i'll definitely break it. It also slows down the prover dramatically

jwerle commented 4 years ago

i'll stay away until there is a signal stability. Should I stay away from Slice and MutSlice because they implement borrow() or just don't implement a borrow() for my module code?

aep commented 4 years ago

nah, everything that has tests must always pass. i'll fix slice when i break borrow :)

jwerle commented 4 years ago

hell yeah :]

jwerle commented 4 years ago

closing for now