Description

Compact encoding

Named variables

Assignment of parameters

Usage

Build

git clone https://github.com/vsklad/cgenmake

Run

Command Line

cgen encode (SHA1|SHA256) [-r <rounds>] [-v <name> <value>]... [<encoder_options>] [<output_options>] [<output_file_name>]cgen process [<variable>]... [<output_options>] <input_file_name> [<output_file_name>]cgen --helpcgen --version

Commands

    encode (SHA1|SHA256) - generate the encoding and         save it in the chosen format (-f option) to <output_file_name>;        can generate the encoding for specified number of rounds (-r option);        also, assign the message and hash values fully or partially (-v option);        if <output_file_name> is omitted, a default file name is assumed    process - process and existing CNF/DIMACS or ANF file        read the formula from <input_file_name>,        assign existing variables if specified then simplify the formula and save it to <output_file_name>;        for an existing variable, its spefification is updated or replaced (see -v replace);        otherwise if the specified variable does not exist, its definition is added;        this command accepts any CNF/DIMACS files, not necessarily produced by the tool;        if <output_file_name> is omitted, the resulting CNF is not saved;            this can be used to compute values of named variables

Options

    <variable> = -v <variable_name> <variable_value> | -v<variable_name>=<variable_value>        specification of a named variable (template) or a single binary variable         named variable is a sequence of literals and constants represented with bits        its template maps to binary variables and/or constant values        named variable definitions are recorded in custom "var" statements         in comments within the output (e.g. DIMACS) file                <variable_name> is the name of the variable, case sensitive            if a decimal number, treated as a binary variable number              must be a valid binary variable number from the formula            otherwise, treated as a named variable name              may contain characters '0'..'1', 'a'..'z', 'A'..'Z', '_'              with first symbol may not a digit            an option with the particular variable may only appear once        <variable_value> is the variable value or specification            constant binary variables may be grouped into bytes            and further represented as a string, a hexadecinal or binary number            sequential representation can be further optimized as below            if a value includes spaces, it must surrounded with double-quotes            to allow the shell process it as a single argument                    supported specifications:            <value> = ( <value_data> | random | ( compute [<compute_options>] )) [<except>]            <value_data> = ( <value_template> | <str_value> ) [<pad>] [ replace ]                        <value_template> = (<literal> | <hex_value> | <bin_value> | <non_value>)[<sequence_clause>]            <value_template> = "{" <variable_template> ["," <variable_template>]..."}"[<sequence_clause>]                 defines a named variable by describing a set of literals and constants            <sequence_clause> = "/"<count>["/"<step>]                defines a sequence of <count> elements where the first item is the specified value                each subsequent element is produced by adding <step> to the previous one                <step> other than zero is allowed for variable sequences and nested elements only                <step> can be negative but the sequence is limited to valid variable numbers                for nested elements                    the same <step> applies to every variable within the element                    constant and unassigned values are the same for each element in the sequence            <hex_value> = 0x['0'..'9', 'a'..'f', 'A'..'F']...                a big endian hexadecimal constant                each hexadecimal digit is mapped to 4 binary variables            <bin_value> = 0b['0'..'1']...                a big endian binary constant                each symbol is mapped to 1 binary variable            <str_value> = string:[\0x21..\0x7F]... | "[\0x20..\0x7F]..."                an ASCII string, with quotes if includes one or more space symbols                big endian format is assumed if mapped to word(s)                each character is mapped to 8 binary variables            <non_value> = *                for existing named variables, the value should be kept as in the definition                otherwise, means that the value is unassigned and can be anything            random                assigns binary variable or binary variables (bits) of the named variable                   to random values (uniform distribution);                constant binary values remain unchanged;                <except_clause> can be used to control partial assignment,                i.e. to assign certain number of bits or exclude certain range from assigning;                the named variable must be defined (exist) before the assignment                            compute                the value is computed and the formula is processed as follows:                1. assign other variables to the specified values without <except_clause> applied                2. determine the computed value by encoding/evaluating the formula with those assignments                3. encode the formula with all variables and <except_clause> taken into account                the named variable must be defined (exist) in order to compute its value                            <compute_options> = complete | difference | constant                these options define the composition of the computed value                partial representations without variables can be used to map values across formulas                    "complete" - all bits are assigned either from variable template or as calculated;                        when the value is assigned, some binary variables may be assigned to themselves;                        this has no effect on the result however                    "difference" - only those bits that are different from the template, are assigned                        bits with values equal to those in the template, are unasssigned                    "constant" - the value includes all constant binary values but no variables                        all variable bits are unassigned                "difference" is the default value                            <pad> = pad:(SHA1 | SHA256)                the variable treated as a SHA-1/SHA-256 message and is padded accordingly;                not supported for assigning of individual binary variables                not supported for "random" and "compute" modes                            <except> = except:(( <first>..<last> ) | <count> )                <first>..<last> - range of binary positions/variables to prevent from assigning                   one-based index, i.e. <first> and <last> must be between 1 and the size of the variable;                <count> - choose the requested number of bits randomly (uniform distribution)                   and prevent them from being assigned;                   the number of bits is chosen from those set to constants within the specified value                   where the underlying variable has them non-constant                the named variable must be defined previously                not supported for assigning of individual binary variables                            replace                if the named variable exists, forces its redefinition in the DIMACS file                the existing definition is ignored                not supported for assigning of individual binary variables                            Notes:                named variable is interpreted as new if it does not exist or if "replace" option is specified;                otherwise, the value is assigned to the prevously defined variable before processing the formula;                the non-constant bits of the named variable are set to constant bits from the value;                in all other instances the named variable bits and the value bits must match        -r <value>        number of algorithm rounds to encode        the value must be valid for a particular algorithm (e.g. 1 to 80 for SHA-1)        if unspecified, the algorithm is encoded in full with all rounds        this option is only valid for <encode> command            -h | --help        output parameters/usage specification            --version        output version number of the tool        <encoder options>        [--add_max_args=<value>] [--xor_max_args=<value>]            these options define how the encoder processes addition and xor's for multiple operands            these options are allowed for CNF only (not allowed for ANF)            specify maximal number of binary variables to be encoded together, plus the result            any constants are optimized out when encoding and are outside this number             <add_max_args> is a number between 2 and 6 for CNF, 3 for ANF, 3 if not specified;                defines maximal number of binary variables to be added together            <xor_max_args> is a number between 2 and 10, 3 if not specified                defines maximal number of binary variables to be xor'ed together                        [--assign_after_encoding]            assign all variable values if any specified, after encoding;            ignore those values while encoding;            similar to "unoptimized" pre-processing mode in relation to encoding;            i.e. no formula optimization while encoding            i.e. produce SHA-1 CNF formula with 512 variable message bits                then assign provided message bit values according to -m processing option;            if this option is not specified,                the provided variable values are used to encode a simple formula if possible                <output options>        -f<output_format_name>            output type/form/format, CNF if not specified;            the following formats are supported:                ANF - output ANF formula in PolyBoRi output format                (CNF | DIMACS_CNF) - output CNF formula in DIMACS format                (VIG | VIG_GraphML) - output VIG^ obtained from CNF formula, in GraphML format                (VIGW | VIGW_GraphML) - output VIG obtained from CNF formula, with weighted edges                 (VIG_GEXF) - output VIG obtained from CNF formula, in GEXF format            ^VIG stands for Variable Incidence Graph                -m ((unoptimized | u) | (all | a) | (original | o))            mode for pre-processing and assigning of variable values            has no effect on how the formula is encoded if used with <encode>;            (unoptimized | u)                no simplification techniques; assign variable values by                 appending unary clauses or equations to the output formula;                this is the only supported and default mode for ANF            (original | o)                apply simplification techniques; eliminate variables;                output included only clauses present in the formula                 originally after encoding;                determined variable values are propagated                simplifying and eliminating some of the clauses            (all | a)                apply pre-processing techniques; eliminate variables;                output includes the original clauses plus all clauses                 produced by applying resolution rule while pre-processing;                determined variable values are propagated                simplifying and eliminating some of the clauses                        --no_variable_reindexing            do not reindex binary variable numbers after processing;            if this option is not specified the tool would reindex             variable numbers and remove any gaps in numbering;            this option is only applicable following simplification        -n | --normalize_variables            reindex binary variables such that no negations are present             within named variable definitions within the output file;            may add aditional clauses/equations as necessary            supported for encode/process commands                    (-t | --trace)((debug | d) | gexf | (native | n))            record and output a trace of the formula simplification process;            applicable to all output formats based on CNF;            available only when compiled with CNF_TRACE directive;            available formats:            debug | d              print the trace in "native" format            gexf              the trace is recorded as a dynamic graph in a file with               name obtained by adding ".trace.gexf" to output_file_name            native | n              the trace is recorded in a file in "native" format, its name              being the output_file_name with ".trace" expension appended

Pre-defined Variables

    M - message, a sequence of bits (bytes, words), size must be a multiple of 512 (the block size)        any size is acceptable with padding specified (see <pad>)        ASCII/hexadecimal constants or more complex templates can be used to specify the value and/or its size        single block encoding assumes up to 448 bits with padding or 512 bits exact without padding        the message value is used for encoding,        i.e. the formula is produced for the specified value originally, with maximal optimization    H - hash value, a set of 160 bits for SHA-1 grouped into 5 32-bit words,         256 bits and 8 words for SHA-256 respectively        the value is assigned afterwards with recursive UP and euqivalences optimizations

Examples

Verification

Example

sha1-sat --cnf --tseitin-adders --message-bits=0 --hash-bits=0 > vn_original.cnf

cgen process -vM {{32/32/-1}/16/32} -vH {2752/32/-1}/5/32 vn_original.cnf vn_cgen.cnf

cgen assign -vM string:CGen pad:sha1 vn_cgen.cnf vn_evaluated.cnf

var W = {{32/32/-1}/16/32, {543/31/-1, 544}/64/32}var A = {2912/32/-1}/80/32

PolyBoRi Output Format

Acknowledgements & References

Change Log

Version 1.2.1

Version 1.2

Version 1.1

About