PR #231 introduced initial support for BitVector sorts. This has allowed us to conduct first successful experiments in formalization of Tinyrossa.
Large-scale application of this code to complete refinement-type formalization of Isla, is limited by two problems.
Isla uses many more lengths (almost every length from 1 to 128?) than the predefined small set in PR 231. The problem is even quadratic, O²(128) because of ops like Z3_mk_concat and Z3_mk_extract.
With things like Z3_mk_extract you don't even know the resulting length (or at least it's not explicit in the static type declaration; so it's like "dependent sorts"). Isla makes heavy use of "any-length bitvector" sort. In fact even when some x is trivially known to be, say, %bv32, most often it's declared as %bv, relying on type inference. This is true also for function types (both of "fun defs" and "externs"), resulting in extensive type-instantiation.
The present Issue calls to implement these Any-Length BitVectors. The core machinery is already in place (MA already has fully-general Hindley–Milner sorts and polymorphism-as-naturality); but we rely on #332 so we (and downstream Isla code) can regard it as stable API. My estimation is that the changes needed here, can stay local to Sprite and not affect Fixpoint at all.
PR #231 introduced initial support for BitVector sorts. This has allowed us to conduct first successful experiments in formalization of Tinyrossa.
Large-scale application of this code to complete refinement-type formalization of Isla, is limited by two problems.
Z3_mk_concatandZ3_mk_extract.Z3_mk_extractyou don't even know the resulting length (or at least it's not explicit in the static type declaration; so it's like "dependent sorts"). Isla makes heavy use of "any-length bitvector" sort. In fact even when somexis trivially known to be, say,%bv32, most often it's declared as%bv, relying on type inference. This is true also for function types (both of "fun defs" and "externs"), resulting in extensive type-instantiation.The present Issue calls to implement these Any-Length BitVectors. The core machinery is already in place (MA already has fully-general Hindley–Milner sorts and polymorphism-as-naturality); but we rely on #332 so we (and downstream Isla code) can regard it as stable API. My estimation is that the changes needed here, can stay local to Sprite and not affect Fixpoint at all.