Megalodon 1.7

by Brown, Friday, September 03, 2021, 10:23 (93 days ago)

Here is Megalodon version 1.7:

http://grid01.ciirc.cvut.cz/~chad/megalodon-1.7.tgz

I've added some basic automation. If you're writing a proof term to close a goal with an exact, you can write ?xx? and Megalodon will try to generate the proof term that should be in that position. If the xx is some hex characters (up to 64 hex chars, i.e., 32 bytes), then it is taken as a seed to determine random choices made during the search. If the xx is "+" or starts with "*", then Megalodon will search for an appropriate seed. The "+" option only tries the shortest 64K seeds (up to 4 hex chars). The "*" option can try more (or fewer) seeds optionally chosen by the -masl command line option, with default 64K. The "*" option can also include some hex characters as an initial seed which is then incremented if it doesn't work.

Here are a few examples:

exact ??. (This does a basic search with seed 0. Proof checking halts on failure.)

exact ?ab?. (This does a basic search given by the 32 bytes starting with byte ab with remaining bytes 0. Proof checking halts on failure.)

exact ?+?. (This tries to find a seed where at most the first two bytes are 0, admitting the subgoal if none is found.)

exact ?*ab0d25?. (This starts with the seed ab0d25000...000 and increments until a seed solving it is found, or the -masl limit is reached. Upon failure, the subgoal is admitted.)