mirror of
https://github.com/GaloisInc/cryptol.git
synced 2024-12-15 18:52:13 +03:00
27 lines
1.2 KiB
Plaintext
27 lines
1.2 KiB
Plaintext
// TMD: I am using this issue for a range of regressions or short-comings with the new type checker.
|
|
// Let me know if you'd like separate github issue numbers.
|
|
|
|
// Want: exact width values is nice (width x == const ==> width x >= const)
|
|
// Issue: Cryptol wants 'width x >= const'
|
|
// width_eq_geq : {n} (32 == width n, n >= 1, 32 >= width n, fin n) => [n]Bit
|
|
width_eq_geq : {n} (32 == width n, n >= 1) => [n]Bit
|
|
width_eq_geq = [True | _ <- [1..n] : [_][32] ]
|
|
|
|
// Want: const >= width (x+1) ==> const > width x
|
|
// or any monotonic function, not just addition.
|
|
//
|
|
// Also Want: const >= width n ==> fin n
|
|
//
|
|
// Issue: Cryptol wants '64 >= width n' and 'fin n'
|
|
// can_not_width : {n} (64 >= width (8*(n+1)), 64 >= width n, fin n) => [64]
|
|
can_not_width : {n} (64 >= width (8*(n+1))) => [64]
|
|
can_not_width = zero # (`n : [width n])
|
|
|
|
// Want: Honestly, I don't know what's going on here. It seems to relate to some of our regressions though.
|
|
// Tell me if there should be another ticket - probably one that already exists. -TMD
|
|
// Issue: Cryptol 2.3 wants 'n == 4 + (?a3 - n % 4)'
|
|
take_knows_no_bounds : {n} (fin n, n >= 4) => [n][8] -> [4 - (n%4)][8]
|
|
take_knows_no_bounds ns = foo
|
|
where
|
|
foo = take `{4 - (n%4)} ns
|