Const declaration for array types

use vstd::prelude::*;
verus! {

spec const SPEC_BAR: int = 100;
// works
exec const BAR: u8 ensures BAR@ == SPEC_BAR { 100u8 }

spec const SPEC_FOO: Seq<u8> = seq![1, 0, 0, 0];
// doesn't work
exec const FOO: [u8; 4] ensures FOO@ == SPEC_FOO { [1, 0, 0, 0] }

// works
exec const FOO: [u8; 4] ensures FOO@ == SPEC_FOO { 
    let foo: [u8; 4] = [1,0,0,0];
    assert(foo@ == seq![1u8,0,0,0]);
    foo
}

}

Maybe it's fine to have this explicit assertion for arrarys...

Link to code

verus-lang / verus

Const declaration for array types #1131