Coding Assignment 4: Verification

Due: Friday, May 22 at 5:00 PM | 150 points

Coding Assignment 4 has two parts, and all problems in both parts are required (there are no options this week). Details for each problem will be embedded in starter code in the course repo.

Reflection (30 points): Complete a short reflection (~100–200 words total) answering the following questions. You don't need to answer all of them, just pick a few that feel relevant. For this part only, apply the same course AI policy as for reading reflections, not the course AI policy for code. * While our basic symbolic execution engines only dealt with integers, the concept can be extended to arrays, objects, and more general ideas. Can you see yourself using similar tools to verify code outside of this class? * Did either side of the assignment (counterexample-finding in Part A, or invariant-finding in Part B) come more naturally to you than the other? Why do you think that is? * Did you enjoy this homework assignment? If so, what broader lessons did you take away from it, besides learning to solve these specific problems? If not, what kinds of problems would more useful to you?

You will submit the following to Gradescope:

• One Python file per problem, containing all of your source code for that problem. The expected filename is fixed per problem (see the starter code). Do not use Python packages except Z3 and other built-in packages. Do not import more things from Z3 that are not already imported for you. Do not submit additional code files (in particular, do not submit the engine/ directory — the autograder ships its own copy).
• A Markdown (.md) or text (.txt) file containing your reflection response.

The autograder will automatically grade Parts A and B. For Part A, the autograder will check that your provided counterexample is a real counterexample at 32 bits, and that your verification query computes a real counterexample at whatever bit-width you chose within 5 seconds on Gradescope. For Part B, the autograder will check that each of the postconditions holds within 5 seconds on Gradescope. You may resubmit as many times as you like while submissions are open.

Reminder: The full course collaboration and AI policy may be found in the syllabus. To summarize: You may discuss problems at a high level with classmates, but do not share solutions, code, or detailed derivations with other students. You may use AI tools (Copilot, ChatGPT, Claude, etc.) as part of your workflow, but you must include a short attribution note in your submission listing which tools you used and how.

Part A: Counterexample-finding with the L07 symbolic execution engine

For each problem, use the provided symbolic execution engine (an extended version of the one from L07) to find a specific counterexample that shows why the program has a bug. In particular, you are not expected to find the bug by manual reasoning. Points will be given as follows:

• For half the points, you submit a correct counterexample (at 32 bits).
• For the second half of the points, your query to the symbolic execution engine runs on the Gradescope machine in under 5 seconds and automatically outputs a valid counterexample (at whatever bit width you are using).

In order to find the bug, you may choose to do any of the following:

• Encode preconditions with assume statements
• Encode postconditions with assert statements
• Check loop invariants with assume, assert, and/or havoc
• Introduce new variables that are only used within assume, assert, and/or havoc statements
• Change the number of times each loop is unrolled (default: 1)
• Change the bit width of each bitvector
  • If you choose to do this, you should submit the computationally feasible code (at lower bit width), as well as a counterexample at 32 bits, which you may reason about based on the counterexample at lower bit width.

You must not change the output of the function or any code that affects the outputs.

Problem 1: Clamped subtraction — 20 points

Input: Two 32-bit signed integers $a$ and $b$

Output: If $a-b$ fits in a 32-bit signed integer without overflow, return $a-b$, otherwise return INT_MAX or INT_MIN depending on the direction of overflow.

def clamp_sub(a, b):
    if a > 0 and b < 0 and a - b < 0:
        result = INT_MAX
    elif a < 0 and b > 0 and a - b > 0:
        result = INT_MIN
    else:
        result = a - b

    return result

Problem 2: Safe multiplication — 20 points

Input: Two 32-bit signed integers $a$ and $b$

Output: If $a\times b$ fits in a 32-bit signed integer without overflow, return $a\times b$, otherwise return $0$.

def safe_mul(a, b):
    if a == 0 or b == 0:
        result = 0
    else:
        c = a * b
        if c // a != b:
            result = 0
        else:
            result = c

    return result

Problem 3: Count groups — 30 points

Input: A 32-bit signed integer $a$ with $a\ge 0$, thought of in binary

Output: A group is two or more consecutive 1's. Return the number of groups.

def count_groups(x):
    assume(x >= 0)

    cnt = 0
    in_run = 0
    run_len = 0
    i = 0
    while i < BITWIDTH:
        bit = (x >> i) & 1
        if bit == 1:
            in_run = 1
            run_len = run_len + 1
        else:
            if in_run == 1:
                in_run = 0
                if run_len >= 2:
                    cnt = cnt + 1
                    run_len = 0
        i = i + 1

    return cnt

Part B: Verification with loop invariants and the L08 WP engine

For each program, verify its correctness using invariants. The precondition (assume) and postcondition (assert) are provided. Fill in the invariant(...) call inside each loop so that the L08 WP engine discharges all obligations (entry, preservation, sufficiency). Each problem should take under 5 seconds.

You may not modify the precondition, postcondition, or any code that affects the function's output.

Problem 4: Make change — 20 points

Input: A non-negative integer amount in cents.

Output: A minimal-coin breakdown (quarters, dimes, nickels, pennies) of amount using US denominations, such that the number of larger denominations is maximized.

def make_change(amount):
    assume(amount >= 0)

    orig = amount
    quarters = 0
    dimes = 0
    nickels = 0
    pennies = 0

    while amount >= 25:
        invariant(True)
        amount = amount - 25
        quarters = quarters + 1

    while amount >= 10:
        invariant(True)
        amount = amount - 10
        dimes = dimes + 1

    while amount >= 5:
        invariant(True)
        amount = amount - 5
        nickels = nickels + 1

    while amount >= 1:
        invariant(True)
        amount = amount - 1
        pennies = pennies + 1

    assert 25 * quarters + 10 * dimes + 5 * nickels + pennies == orig
    assert dimes < 3 and nickels < 2 and pennies < 5
    return (quarters, dimes, nickels, pennies)

Problem 5: Newton's isqrt — 30 points

Input: An integer $n$ with $1\le n\le {10}^9$.

Output: $\lfloor \sqrt{n}\rfloor$

def isqrt_newton(n):
    assume(n >= 1)
    assume(n <= 1_000_000_000)

    x = n
    y = (x + 1) // 2
    while y < x:
        invariant(True)
        x = y
        y = (x + n // x) // 2

    assert x * x <= n
    assert (x + 1) * (x + 1) > n
    return x