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?
---
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).
It's not "dynamic memory allocation" in that Wuffs still doesn't malloc/new and free/delete per se. But it is dynamically (run time, not compile time) sized.
Grepping for "work buffer" or "workbuf" in Wuffs' example/ or std/ code (or SkWuffsCodec.cpp) should give some leads, if you want to study some code. The workbuf_len is often zero but, for Wuffs' std/jpeg and std/png, it is positive. Manage the work buffer in the same way as the pixel buffer: it's always caller-owned and callee-borrowed.
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.
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.
In comparison, "array size is always 1024, array index is always bitwise-anded with 1023, therefore always in-bounds" is undeniably simple and, per "The Fastest, Safest PNG Decoder in the World", practical and fast.