type defaulting for eval_bool

[WeeknightMVP]

Consider an attempt to validate a file's MD5 checksum:

> CRYPTOLPATH="cryptol-specs/Primitive/Keyless/Hash/" saw
 ┏━━━┓━━━┓━┓━┓━┓
 ┃ ━━┓ ╻ ┃ ┃ ┃ ┃
 ┣━━ ┃ ╻ ┃┓ ╻ ┏┛
 ┗━━━┛━┛━┛┗━┛━┛ version 0.2 (dd7121b)
sawscript> import "MD5.cry" as MD5;
sawscript> MD5_bytes <- read_bytes "cryptol-specs/Primitive/Keyless/Hash/MD5.cry";
sawscript> let actual_checksum = {{ (MD5::md5 (join MD5_bytes)):[128] }};
sawscript> let expected_checksum = {{ 0x11abfc5697aa4f1c293dd38c6a8d9e49:[128] }};
sawscript> print {{ actual_checksum == expected_checksum }};
Assuming n = 140
True
sawscript> print (eval_bool {{ actual_checksum == expected_checksum }});

user error ("eval_bool" (<stdin>:1:8-1:17):
eval_bool: not type Bit)
sawscript> type expected_checksum
[128]
sawscript> type actual_checksum
{n} (512 * n >= 71361, 511 >= 512 * n - 71361, fin n) => [128]

Consider the Cryptol definition of MD5::md5:

md5 : {a, b, p} (fin p, 512 * b == 65 + (a + p), 64 >= width a, 511 >= p) =>
      [a] -> [128]
md5 msg = md5output finalState
    where
        // ...

I deduced that b must be the parameter SAW assumes is 140:

sawscript> let actual_checksum = {{ (MD5::md5`{b=140} (join MD5_bytes)):[128] }}
sawscript> type actual_checksum
[128]
sawscript> eval_bool {{ actual_checksum == expected_checksum }}
true

Is there any way to instruct SAW to just trust its assumptions for Term evaluation? Would it be possible to consistently label the assumed parameters?

[brianhuffman]

Ok, it seems like the problem is that eval_bool doesn't perform defaulting on its Term argument, while other functions like print apparently do. I'll look into it.

[brianhuffman]

Here's a smaller self-contained example:

sawscript> print {{ zero == zero }}
[03:46:48.104] Assuming a = Integer
[03:46:48.105] True
sawscript> eval_bool {{ zero == zero }}
saw: Stack trace:
"eval_bool" (<stdin>:1:1-1:10):
eval_bool: not type Bit

At this point the REPL exits.