Heapster bugfixes for sha512 example#1523

Merged

mergify[bot] merged 11 commits intomasterfrom heapster/sha512-bugfixes

Nov 23, 2021

+452-31

Commits on Nov 22, 2021

Commits on Nov 23, 2021

Merge branch 'master' into heapster/sha512
Eddy Westbrook
committed
bug fix: changed tcJumpTarget to freshen up the argument names in any jump, as both the type-checker and translator rely on all arguments being distinct variables
Eddy Westbrook
committed
added a line to turn off translation checks when type-checking sha512_block_data_order
Eddy Westbrook
committed
changed the translation of calls to multi-entry blocks so they no longer accumulate Hobbits variables from the caller
Eddy Westbrook
committed
whoops, removed an infinite loop in splitLLVMBlockPerm when it is called on a block with the empty shape
Eddy Westbrook
committed
commented out the sha512 example from the _CoqProject, because it takes a while to run...
Eddy Westbrook
committed
remove foldrAndBuildDistPerms
m-yac
authored
get mbox_proofs.v working again
m-yac
committed