Formal Correctness Proos of us_to_ticks conversion in the initialiser

[midnightveil]

With #95 once it is merged we will have a conversion from us to ticks implemented.

Ideally, we should formally verify and link into CI the implementation of this to make it sure it upholds the guarantees we provide (i.e. rounded to nearest tick or failure).

I am confident in this code from prior SMT verification of similar code for ns_to_ticks in sDDF or a dirtier version but with proper rounding in a GIST.

However, we should link this into our CI and the us_to_ticks conversion we are doing. Also, I have a (TS group) monday talk behind the motivation on this:

Monday_Talk_22_June_2026___Of__Formally__Correct_Time_Conversions.pdf

[midnightveil]

Here's a brief modification of the Z3 model in sDDF to work for us. This tells us that this will work for any output that fits in 56 bits; however, the rounding check is not perfect (it's ±1 tick not nearest tick) and also the (div us 1000000) (div 72057594037927936 freq) only works in the truncation logic, so there can be cases that it fails at runtime. (edit: well it reports unsat but it is not a tight bound)

; Copyright 2026, UNSW
; SPDX-License-Identifier: BSD-2-Clause

; Improvements (TODO)
; - Make the proof about period_shift generic, instead of two instantiations
;   one for ticks2ns and ns2ticks with duplicated internals.
; - Link more closely to C code.

(set-option :produce-unsat-cores true)

(declare-const GHz Int)
(assert (= GHz 1000000000))

(declare-const MHz Int)
(assert (= MHz 1000000))

(define-fun precise_period_shift ((period Int) (target_freq Int) (input_freq Int)) Real
    (/ (* period target_freq) input_freq))

(define-fun precise_us_to_ticks ((us Int) (freq Int)) Real
    (precise_period_shift us freq (* 1 MHz)))

; TODO: this really should be "rounded" and allows a bit more slack than we really should but
; compare some integer b to floating point xxx.yyy and check if it is xxx or xxx + 1
(define-fun real_is_within_unit_distance ((a Real) (b Int)) Bool
    ; either: b == a, or b < a < b + 1, or b - 1 < a < b
    (or
        ; b == a
        (= b a)
        ; b < a < b + 1
        (< b a (+ b 1))
        (< (- b 1) a b)
    ))

(define-fun is_64_bit_int ((x Int)) Bool (<= 0 x 18446744073709551615))
(define-fun is_61_bit_int ((x Int)) Bool (<= 0 x 2305843009213693951))
(define-fun is_56_bit_int ((x Int)) Bool (<= 0 x 72057594037927935))
(define-fun is_48_bit_int ((x Int)) Bool (<= 0 x 281474976710655))
(define-fun is_32_bit_int ((x Int)) Bool (<= 0 x 4294967295))

; (push)
;     (echo "=== precise_ticks_to_ns test")
;     (declare-const ns Int)
;     (declare-const ticks Int)
;     (assert (= ticks 2))
;     ; 2 ticks at 1Hz is = 2e9 nanoseconds
;     (assert (= ns (precise_ticks_to_ns ticks 1)))
;     (assert (= ns 2000000000))
;     (check-sat)
;     ; (get-model)
; (pop)

; (push)
;     (echo "=== precise_ns_to_ticks test")
;     (declare-const ns Int)
;     (declare-const ticks Int)
;     (assert (= ns 2000000000))
;     ; 2e9 nanoseconds at 1Hz is 2 ticks
;     (assert (= ticks (precise_ns_to_ticks ns 1)))
;     (assert (= ticks 2))
;     (check-sat)
;     ; (get-model)
; (pop)


(push)
    (echo "=== us to ticks (unsat is proof; sat shows a counterexample)")
    ; Corresponds to us2ticks(ticks, freq) which calls period_shift(ticks, freq, 1 MHz)
    ; Due to limitations of this smtlib language we have to inline the definitions of both.

    (declare-const freq Int)
    (declare-const us Int)
    (declare-const ticks_precise Real)
    (declare-const ticks_sddf   Int)

    ; 1 <= freq <= 2^32 - 1 (~ 4GHz)
    (assert (is_32_bit_int freq))
    (assert (not (= freq 0)))
    ; 0 <= ... <= 2^64 - 1
    (assert (is_64_bit_int us)); by input

    ; This is "equivalent" to the asserts below, but done symbolically
    ; This shows us that this algorithm should be fine for any input where
    ; output matches this.
    ; However the assert below was useful for checking whether it would overflow.
    (assert (is_56_bit_int ticks_precise))

    ; (assert (
    ;     ; note log base 2
    ;     ; log(out_period_whole) = log(period) + (log(target_freq) - log(input_freq))
    ;     ; log(out_period_whole) < 56
    ;     ; log(period) + log(target_freq) - log(input_freq) < 56
    ;     ; log(period) - log(input_freq) < 56 - log(target_freq)
    ;     ;
    ;     ; For us2ticks; period = us, input_freq = 10^6, target_freq = freq
    ;     ;
    ;     ;     log(ns) - log(10^6) < 56 - log(freq)
    ;     ;     log(ns) - log(10^6) < 56 - log(freq)
    ;     ; 2^(log(ns) - log(10^6)) < 2^(56 - log(freq))
    ;     ;               ns / 10^6 < 2^56 / freq
    ;     ;
    ;     ; Alternative form that requires >64 bits to evaluate:
    ;     ;               ns * freq < 2^56 * 10^6
    ;     ; (useful for z3 to prove tightest bound)
    ;     ;

    ;   TODO: This check does work until we add the round-exactness modification
    ;     ; < (div us 1000000) (div 72057594037927936 freq)

    ;     < (* us freq) 72057594037927936000000
    ;     ; This times out, so z3 can't prove it works.
    ;     ; < (* us freq) 72057594037927936000001
    ; ))

    ;; Note: most of these comments are wrong

    ; This is the oracle done in z3's 'Real' (i.e. rational) numbers
    (assert (= ticks_precise (precise_us_to_ticks us freq)))

    ; The arguments to period_shift.
    (declare-const period Int)
    (assert (= period us))
    (declare-const input_freq Int)
    (assert (= input_freq (* 1 MHz)))
    (declare-const target_freq Int)
    (assert (= target_freq freq))
    (declare-const out_period Int)
    (assert (= out_period ticks_sddf))

    (declare-const period_whole Int)
    (declare-const out_period_whole Int)
    (declare-const period_remainder Int)
    (declare-const out_period_remainder_intermediate Int)
    (declare-const out_period_remainder_intermediate2 Int)
    (declare-const out_period_remainder Int)

    ; C: `uint64_t out_period_whole = (period / input_freq) * target_freq`
    ; log(period_whole) = log(period) - log(input_freq).
    ; No overflow, just truncation.
    (assert (= period_whole (/ period input_freq)))
    ; log(out_period_whole) = log(period_whole) + log(target_freq) = log(period) + (log(target_freq) - log(input_freq))
    ; No overflow if input_freq <= target_freq. Permissible overflow (out of range input) otherwise.
    (assert (= out_period_whole (* period_whole target_freq)))

    ; C: `uint64_t period_remainder = period % input_freq`.
    ; log(period_remainder) <= log(input_freq)
    (assert (= period_remainder (rem period input_freq)))

    ; C: `uint64_t out_period_remainder = (period_remainder * target_freq) / input_freq;`
    ; log(out_period_remainder_intermediate) = log(period_remainder) + log(target_freq)
    ;                                        <= log(input_freq) + log(target_freq)
    ; No overflow if input_freq * target_freq is <= 2^64. Non-permissible overflow otherwise.
    (assert (= out_period_remainder_intermediate (* period_remainder target_freq)))
    (assert (= out_period_remainder_intermediate2 (+ out_period_remainder_intermediate (div (* 1 MHz) 2))))
    ; log(out_period_remainder) = log(out_period_remainder_intermediate) - log(input_freq).
    ; No overflow, just truncation.
    (assert (= out_period_remainder (/ out_period_remainder_intermediate2 input_freq)))

    ; C: `return out_period_whole + out_period_remainder;`
    ; As remainder < whole, permissible overflow (out of range input) only when near 2^64 input.
    (assert (= out_period (+ out_period_whole out_period_remainder)))

    (
        assert
        (
            or
            (not (is_64_bit_int period_whole))
            (not (is_64_bit_int out_period_whole))
            (not (is_64_bit_int period_remainder))
            (not (is_64_bit_int out_period_remainder_intermediate))
            (not (is_64_bit_int out_period_remainder_intermediate2))
            (not (is_64_bit_int out_period_remainder))
            ; note: 56 bits here
            (not (is_56_bit_int out_period))
            (not (real_is_within_unit_distance ticks_precise ticks_sddf))
        )
    )

    (check-sat)
    (get-model)
    ; (get-unsat-core)
(pop)

[lsf37]

This is quite nice. Is there a way to automatically extract the behaviour part of this from the C code snippet we use? Could be ad-hoc and geared just for this particular example, as long as it is mechanical and gives us a failure if we change the code in a way that deviates from what we prove here.

Other random side idea would be looking at whether we could add a mode to the C parser to generate an smt-lib representation of const functions that only operate on word types. We don't have a huge amount of them, but where we do have then, something like this would inspire more confidence than manual review.

[midnightveil]

One annoyance of this (which I described in the talk PDF) is that I have to manually name each individual variable and assert each fits in 64 bits. Which requires naming each individual expression. It's probably doable with the knowledge the l4v C parser has, yes.

(another thing I could have done is assert that the 56-bit output precondition implies the easy-to-check input condition, though that only works if it doesn't limit the inputs unnecessarily which could be annoying)

I'm not entirely convinced smtlib was really the best way to do this, it was really annoying. For our sDDF work it was proposed we use the Viper tools for encoding this, since it's what our other verification is.

[lsf37]

One annoyance of this (which I described in the talk PDF) is that I have to manually name each individual variable and assert each fits in 64 bits. Which requires naming each individual expression. It's probably doable with the knowledge the l4v C parser has, yes.

That sounds doable, yes

I'm not entirely convinced smtlib was really the best way to do this, it was really annoying.

It's basically verification assembly language, yes. Usually mostly used as an interface language for multiple prover backends, but for small things like this it's still doable.

For our sDDF work it was proposed we use the Viper tools for encoding this, since it's what our other verification is.

That would also work yes. You'd lose the standard input language aspect, but it'd work and it would likely be nicer to deal with.