> Stepping back, I'm not sure if I understand what you're saying. Perhaps we're just disagreeing on how "formal" (as in, part of a "formal verification" process) the enough.c program (or equivalent) needs to be?
Ah, I think I misremembered that bit of Wuffs code, specifically around `HUFFS_TABLE_SIZE`. The comment does mention enough.c but I thought `HUFFS_TABLE_SIZE` was also set to the tight bound found by it, which was not the case, and wondered why you seemed to downplay the importance of enough.c verification. I agree that you don't need any additional verification in the current code.
> As for dynamic memory allocation, Wuffs has a mechanism for the callee (Wuffs code) to tell the caller (C/C++ glue code) that it needs N bytes of "scratch space" or "work buffer", where N is dynamically dependent (e.g. dependent on the image dimensions in pixels).
Isn't it fixed during the decoding process though? If my understanding is correct `decode_frame` is not supposed to change what `workbuf_len` will return later (or examples don't account for them yet). Technically speaking you can already use the suspend mechanism to request a memory allocation of any size, so it is more about a matter of public API, but such code would be very regular and repetitive. I thought a limited mechanism to enable an in-situ dynamic allocation---preferably desugared---might improve a usability a lot.
> Isn't it fixed during the decoding process though?
For Wuffs' image decoding, it's flexible up until decode_image_config returns. It's fixed afterwards.
In practice, that works fine for BMP, GIF, JPEG and PNG (and I'm confident will work for WebP too). No in-situ dynamic allocation (with or without sugar) needed. Even though, for the libjpeg-turbo C code, `grep mem..alloc_ jd*.c | wc -l` shows more than 50 "allocation" call sites, Wuffs' JPEG decoder does just fine with just the one work buffer.
Ah, I think I misremembered that bit of Wuffs code, specifically around `HUFFS_TABLE_SIZE`. The comment does mention enough.c but I thought `HUFFS_TABLE_SIZE` was also set to the tight bound found by it, which was not the case, and wondered why you seemed to downplay the importance of enough.c verification. I agree that you don't need any additional verification in the current code.
> As for dynamic memory allocation, Wuffs has a mechanism for the callee (Wuffs code) to tell the caller (C/C++ glue code) that it needs N bytes of "scratch space" or "work buffer", where N is dynamically dependent (e.g. dependent on the image dimensions in pixels).
Isn't it fixed during the decoding process though? If my understanding is correct `decode_frame` is not supposed to change what `workbuf_len` will return later (or examples don't account for them yet). Technically speaking you can already use the suspend mechanism to request a memory allocation of any size, so it is more about a matter of public API, but such code would be very regular and repetitive. I thought a limited mechanism to enable an in-situ dynamic allocation---preferably desugared---might improve a usability a lot.