SMT Arrays

[filipeom]

Model linear memory using arrays

[hra687261]

Do you have any literature/specification on the memory models in question? Can the SMT theory of sequences be used?

[filipeom]

The idea behind this is simply to attempt to utilize the array theory presented in Z3 (https://microsoft.github.io/z3guide/docs/theories/Arrays/) to model our linear memory in Wasm. I don't expect this to be that efficient, but we need to compare it against our other models to argue their efficiency.

We could also potentially employ sequences. I would need to investigate further, but with some effort, I believe we could probably make this work :)

Edit: paper https://www.microsoft.com/en-us/research/publication/generalized-efficient-array-decision-procedures/

[hra687261]

Alright. Yes I am familiar with that paper, I was asking about literature/specification, because I was wondering if the basic SMT theory of arrays (with only the select and store operators) would be enough, or the additional operators described in that paper are necessary (like const, map ...)

[filipeom]

Oh, yes, I apologize for the misunderstanding. Sections 2.1.1 and 2.1.2 of this paper provide an overview of what we aim to achieve. And, yes I expect that only 'select' and 'store' operations are necessary.