timeout at whnf in array heavy code

Stream: new members

[One Happy Fellow]

hi, I'm implementing SHA-256 is lean and I've run into problem with this function: https://github.com/happyfellow-one/lush/blob/master/lush/Crypto/SHA.lean#L99

I'm getting (deterministic) timeout at `whnf`, maximum number of heartbeats (200000) has been reached and I can't find the source of the error. I've tried replacing the proofs that indexes are valid with (by sorry) but it didn't help.

Could you help me with debugging this? Thanks!

[Michael Rothgang]

Can you make an #mwe?

[One Happy Fellow]

This file is self contained if that's what you meant? If you mean that the example is too large I'll try making a smaller one.

[Johannes Tantow]

Adding '(by simp[hworkinglen]) to every array access operation and replacing trivial with simp[working] suffices in the web editor

[One Happy Fellow]

Thank you! Do you have an idea why I get a timeout otherwise? Or if there's a way to avoid annotating all array accesses with the simp proofs?

[Henrik Böving]

Likely because the default tactic for doing Array access proofs gets lost due to the size of the Array literals

[One Happy Fellow]

I managed to solve it by wrapping working[i] in a function which constructed the proof term for array access, thanks all for help! I still have zero intuition about why lean struggled so much in this case though :(