Insufficient erasure in trait default methods

[jonhnet]

I have some code that verifies without mischief. When I add --compile, I get errors like these in spec fns. I think the common thread is that they're appearing in trait default methods. Recording: 2024-05-09-13-13-55.zip

error[E0605]: non-primitive cast: `usize` as `builtin::int`
  --> src/marshalling/IntegerMarshalling_v.rs:67:65
   |
67 |     open spec fn spec_this_fits_in_usize(v: int) -> bool { v <= usize::MAX as int }
   |                                                                 ^^^^^^^^^^^^^^^^^ an `as` expression can only be used to convert between primitive types or to coerce to a specific trait object

error[E0277]: can't compare `{integer}` with `builtin::int`
   --> src/marshalling/SeqMarshalling_v.rs:328:26
    |
328 |         forall |i: int| 0<=i && i<len ==> self.gettable(data, i)
    |                          ^^ no implementation for `{integer} < builtin::int` and `{integer} > builtin::int`
    |