vsklad / cgen Goto Github PK

I have faced the same problem impostermido posted so the message and hash when computed as sat instance solved by cryptominisat it doesnt match seems that many people need to know how to be solved need yoyr help !

Hi,
I am trying to generate hard instances in ANF format, but it does not work. I took one of the example command lines(see below) and specified ANF output, but it crashes. CNF works fine.
Can this be fixed?
Thanks

./cgen encode SHA1 -vM random except:8 -vH random -f ANF sha1_random.anf
Encoding SHA-1 into ANF
Assigned 504 bit(s) in "M"
M = {{0xc90c4c, 0b11, *, 0b1, 0x9}, 0x6e690698, {0x687, *, 0b010, 0x9a8c}, 0x85e fafb7, 0x0e71e1d5, 0x02d9ff1c, 0x71e34faf, {0b00, *, 0b0, 0x6140f3b}, 0xb63a2ce8 , 0xc75cbec6, 0xc3b8e820, {0x6, *, 0b001, 0x90, *, 0b100, 0xf77}, 0x22f762bf, {0 x9061, *, 0b01, *, 0x039}, 0xb970b31d, {0b100, *, 0x238f739}}
cgen: ./bal/anf/anf.cpp:200: bal::literalid_t bal::Anf::complete_equation(bal::l iteralid_t, bool): Assertion `(bool)((r) == bal::LITERALID_UNASSIGNED)' failed.
Aborted (core dumped)

Many thanks for fixing ANF output(#1), in most cases it works. But in some rare cases it still crashes. Here is one example:
./cgen encode SHA1 -f ANF -vM 0b00100111011110001100000111100001010111000001000100110001110100110000100010010000001110011000101101010111101100101001110110010010011000010111001000101100110011100011101001000000010110100100000010011010010000101001101100111011100110111011010001100000111100011100101011111000110001101110110001111110001011001100000110101100011001011000011110110110011101100011011010111101000010110100000000000011011100110001000010110101111111011100101100000111110100100010001000111011000111010110100011010111000010100101000011001000 except:1..7 -vH compute -r 17 data.tmp

Encoding SHA-1 into ANF
Assigned 505 bit(s) in "M"
M = {{*/7, 0b1, 0x78c1e1}, 0x5c1131d3, 0x0890398b, 0x57b29d92, 0x61722cce, 0x3a405a40, 0x9a429b3b, 0x9bb460f1, 0xcaf8c6ec, 0x7e2cc1ac, 0x6587b676, 0x36bd0b40, 0x037310b5, 0xfdcb07d2, 0x223b1d68, 0xd70a50c8}
cgen_linux64: ./bal/anf/anf.cpp:200: bal::literalid_t bal::Anf::complete_equation(bal::literalid_t, bool): Assertion `(bool)((r) == bal::LITERALID_UNASSIGNED)' failed.
Aborted (core dumped)

First of all sorry of inconvenience and hope you could help me I have encoded a sha256 instance with no M or H assigned then solved it , i took the 1st 512 variables (M) then convert it to binary by taking true variables as 1 and false as 0 then used the 512 bits as input for an online sha256 then took the resultant output in hex and converted it to binary and when i compared it to the variables contribute to H it doesn't match although it must match as the message is fixed , also i tried to convert message into text or hex but both give hash doesn't match the real hash any ideas to solve this problem ?

I have dev C++ on my system but unable the cgen.exe on my system , do you have any video demo how to generate the cnf file on system

Sorry I can’t interpret -vH and -vM mapping into binary variables and bits could you please explain to me how determine exactly what are variables that contribute and make both hash and message variables,
Thanks in advance !