prover: RISC-V: implication rules around the "C" extension

riscv-c-implications.py

#! /usr/bin/env python3
import z3

# Input variables
rv32 = z3.Bool('RV32')
f    = z3.Bool('F')
d    = z3.Bool('D')
c    = z3.Bool('C')
zca  = z3.Bool('Zca')
zcf  = z3.Bool('Zcf')
zcd  = z3.Bool('Zcd')

def get_constraints(zcf, zcd):
    global rv32, f, d, c, zca
    return z3.And(*[
        # Each constraint comes from text of the ISA Manual.
        z3.Implies(d, f),                       # D   -> F
        z3.Implies(z3.Not(rv32), z3.Not(zcf)),  # Zcf is RV32 only
        z3.Implies(zcf, z3.And(zca, f)),        # Zcf -> Zca + F (no RV32 checking required here)
        z3.Implies(zcd, z3.And(zca, d)),        # Zcd -> Zca + D

        # [Note that it can be proven from stronger equality form in `statements`]
        # RISC-V ISA Manual:
        # > The C extension is the superset of the following extensions:
        z3.Implies(
            z3.And(
                zca,
                z3.Implies(z3.And(rv32, f), zcf),
                z3.Implies(d, zcd),
            ),
            c,
        ),

        # [Note that they can be proven from stronger equality form in `statements`]
        # RISC-V ISA Manual:
        # > As C defines the same instructions as Zca, Zcf and Zcd, the rule is that:
        z3.Implies(c, zca),                     # C   -> Zca
        z3.Implies(z3.And(c, f, rv32), zcf),    # C+F -> Zcf (RV32)
        z3.Implies(z3.And(c, d),       zcd),    # C+D -> Zcd
    ])

statements = [
    # Practically the same as the ISA Manual definition
    # but in a stronger equality form.
    c == \
        z3.And(
            zca,
            z3.Implies(z3.And(rv32, f), zcf),
            z3.Implies(d, zcd),
        ),

    #   Implication checker to imply "C" *from* others.
    #   Using `c == PROP` instead of `z3.Implies(PROP, c)` ensures that
    #   no other PROPs can imply "C" on each clause (unless equivalent).
    #
    #   Note that, appearance of "zcd" and "zcf" on a clause denotes that
    #   we cannot say anything about "C" on the given clause if we need to
    #   rely on rustc's target features.
    z3.If(
        rv32,
        z3.If(
            d,
            c == z3.And(zcf, zcd),
            z3.If(
                f,
                c == zcf,
                c == zca,
            )
        ),
        z3.If(
            d,
            c == zcd,
            c == zca,
        ),
    ),

    # Imply certain extensions in a best-effort manner (with rustc's
    # `target_feature`s; avoids using zcd and zcf on the left).
    # For "C", there is a stronger statement.
    z3.Implies(z3.And(c, d), zcd),                                           # Zcd
    z3.Implies(z3.And(rv32, c, f), zcf),                                     # Zcf
    z3.Implies(z3.And(z3.Not(d), z3.Or(z3.Not(rv32), z3.Not(f))), zca == c), # C

    #   For "C", check that if the expression above is not satisfied and "C"
    #   is enabled, either "Zcd" or "Zcf" must be true.
    #
    #   This is equivalent to the statement:
    #   the condition above is optimal to force "C" to be enabled
    #   if we are not allowed to depend on "Zcd" or "Zcf".
    z3.Implies(
        z3.Not(z3.And(z3.Not(d), z3.Or(z3.Not(rv32), z3.Not(f)))),
        z3.Implies(c, z3.Or(zcd, zcf))
    ),

    #   For "Zcf" and "Zcd", check that each condition (depending on other
    #   variables) above to imply target extension is indeed optimal unless
    #   equivalent to the condition in the proof.
    #
    #   Accidentally, those optimal solutions (where only tautology is avoided)
    #   do not involve uses of `"zcd"` or `"zcf"`.
    #
    #   This is expressed as follows:
    #
    #   1.  Even if the condition is *not* satisfied, there may be cases
    #       where the all constraints are satisfied if the target is true.
    #   2.  Even in such cases, the same model except target == false
    #       *also* satisfies the given constraints.
    #   3.  That means, the target is not forced to be true
    #       by other variables.

    # Zcd
    z3.Implies(
        z3.Not(z3.And(c, d)),
        z3.Implies(
            # Substitute `zcd` with constants.
            get_constraints(zcf, True),
            get_constraints(zcf, False),
        )
    ),
    # Zcf
    z3.Implies(
        z3.Not(z3.And(rv32, c, f)),
        z3.Implies(
            # Substitute `zcf` with constants.
            get_constraints(True,  zcd),
            get_constraints(False, zcd),
        )
    ),
]

# For each statement, find counterexamples.
for statement in statements:
    solver = z3.Solver()
    solver.add(get_constraints(zcf, zcd))
    solver.add(z3.Not(statement))

    # Expect "unsat" but print counterexample on "sat".
    result = solver.check()
    if result == z3.sat:
        print(f'Failed on: {statement}')
        print(solver.model())
    assert(result == z3.unsat)