saw-core terms stemming from accessing sequences with @ in Cryptol contain seemingly avoidable ites

[nano-o]

The following saw-core term contains a trivial ite that checks whether the access is within bounds. Those terms can be annoying in proofs because the ite term often needs to be hoisted out before applying rewrites.
It seems that it would be easy to determine statically that the access is within bounds. Could this be implemented?

(rewrite (cryptol_ss ()) {{ \(x:[2]) -> x@1 }})

results in:

let { x@1 = Prelude.natToInt 1
    }
 in \(x : Prelude.Vec 2 Prelude.Bool) ->
      Prelude.ite Prelude.Bool
        (Prelude.intLe (Prelude.natToInt 0) x@1)
        (Prelude.at 2 Prelude.Bool x (Prelude.intToNat x@1))
        (Prelude.at 2 Prelude.Bool x 0)

[robdockins]

The normalize_term function I've been working on (CF #1310) does a pretty good job with this.

sawscript> enable_experimental
sawscript> normalize_term {{ \(x:[2]) -> x@1 }}

[18:22:40.537] \(x : Prelude.Vec 2 Prelude.Bool) ->
  Prelude.at 2 Prelude.Bool x 1

The trick going forward will (I think) be keeping the normalization routine from doing more computation than you want.

[msaaltink]

The feature of issue #1001 would also address this problem, if it were ever implemented.

[RyanGlScott]

As a workaround, one can write x @ (1 : [8]) (or whatever bitvector type you prefer) to avoid the use of Integer.

[nano-o]

Thanks! I've been using x1 where [x1,_] = x.