[lifthrasiir]

While I agree that you don't need the tight bound (especially because I think the tight bound for incomplete trees is not much higher than one for complete trees), you do need to be confident that 1024 is either a loose but correct bound or highly unlikely to be reached in practice. So you need to calculate some kind of bounds anyway... And this is another reason I thought something more than Wuffs is desirable [1]; a dynamic memory allocation, when allowed, makes many things easier to implement and prove.

[1] https://news.ycombinator.com/item?id=37480019

[nigeltao]

1024 is a loose but correct bound. That's what enough.c (or script/print-deflate-huff-table-size.go) says.

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.

[lifthrasiir]

> 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.

[nigeltao]

> 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.