Fix encoding of assumptions about reading after buffer size.

[blishko]

Previously, the case of reading 32 bytes (a word) was treated in a special way when encoding in SMT assumptions about reading after buffer size. However, the assumptions were too weak and allowed wrong SMT models where the buffer length were too small and values read after this length were not zero according to the SMT model.

We fix this by removing the special treatment.

Fixes #679.

Description

Checklist

• tested locally
• added automated tests
• updated the docs
• updated the changelog

[blishko]

@msooseth, do you know how to write a good test for this? How to turn the example from #679 into a test case?

[msooseth]

Thanks, this looks like REALLY good work. Let me try to write a test case out of #679

Do you think you could improve the assertReads comment in the meanwhile? I think it needs a bit of love :) It's not documenting this change too well, and in general it seems a bit less-than-optimal.

[msooseth]

(I'll push the test case into this branch, I hope that's OK)

[blishko]

Thanks, this looks like REALLY good work. Let me try to write a test case out of #679

Do you think you could improve the assertReads comment in the meanwhile? I think it needs a bit of love :) It's not documenting this change too well, and in general it seems a bit less-than-optimal.

I think the comment is still valid. It seems to me the special treatment of value 32 was supposed to be an optimization.
But the constraint for the special case was too weak.

I can't think of a better documentation at the moment.

[msooseth]

OK, nice. I have now added a test case. Let me know what you think. Your fix is good as far as I'm concerned. The test case passes with your fix, and fails without it. It does not assume anything about the CEX beyond the first 32 bytes. So it won't break if we e.g. make the CEX shorter, which is what I'm hoping to do :)

[blishko]

The test case is good. I think we can merge?