GaloisInc / cryptol

Cryptol: The Language of Cryptography
https://galoisinc.github.io/cryptol/master/RefMan.html
BSD 3-Clause "New" or "Revised" License
1.14k stars 126 forks source link

Fixes #1696 #1697

Open yav opened 4 months ago

RyanGlScott commented 4 months ago

Some assorted test suite failures arising from this patch—I'm not sure if they are expected or not. e.g.,

      issue1617.icry: [Failed]
5c5
< {a, n} (fin n) => n / 2 == n - n /^ 2
---
> {a, n} (fin n) => n / 2 + n /^ 2 == n

# If output is OK:
cp /home/runner/work/cryptol/cryptol/output/./tests/issues/issue1617.icry.stdout \
     /home/runner/work/cryptol/cryptol/tests/issues/issue1617.icry.stdout

      issue1663.icry: [OK]
      issue167.icry: [OK]
      issue171.icry: [OK]
      issue177.icry: [OK]
      issue184.icry: [OK]
      issue185.icry: [OK]
      issue187.icry: [OK]
      issue198.icry: [OK]
      issue202.icry: [OK]
      issue211.icry: [OK]
      issue212.icry: [Failed]
3a4,22
> 
Error: r] at issue212.cry:18:1--18:40:
>   Failed to infer the following types:
>     • ?m, type argument 'front' of '(#)' at issue212.cry:18:17--18:40
>   while validating user-specified signature
>     in the definition of 'Main::can_not_width', at issue212.cry:18:1--18:14,
>     we need to show that
>       for any type n
>       assuming
>         • 64 >= width (8 * (1 + n))
>       the following constraints hold:
>         • 64 == ?m + width n
>             arising from
>             matching types
>             at issue212.cry:18:17--18:40
>         • fin ?m
>             arising from
>             use of expression (#)
>             at issue212.cry:18:17--18:40

# If output is OK:
cp /home/runner/work/cryptol/cryptol/output/./tests/issues/issue212.icry.stdout \
     /home/runner/work/cryptol/cryptol/tests/issues/issue212.icry.stdout