Failing to understand Ivy at all; how can I convince it I actually want the usual numbers?

output.txt

Isolate sum_absolute_pairs:

    The following action implementations are present:
        sum_ordered_lists.ivy: line 75: implementation of sum_absolute_pairs.get_sum
        sum_ordered_lists.ivy: line 63: implementation of sum_absolute_pairs.left_val
        sum_ordered_lists.ivy: line 67: implementation of sum_absolute_pairs.right_val

    The following action monitors are present:
        sum_ordered_lists.ivy: line 37: monitor of sum_absolute_pairs.left_val
        sum_ordered_lists.ivy: line 48: monitor of sum_absolute_pairs.right_val
        sum_ordered_lists.ivy: line 42: monitor of sum_absolute_pairs.right_val

    The following initializers are present:
        sum_ordered_lists.ivy: line 59: sum_absolute_pairs.init[after13]
        sum_ordered_lists.ivy: line 32: sum_absolute_pairs.init[after5]

    The following program assertions are treated as assumptions:
        in action sum_absolute_pairs.left_val when called from the environment:
            sum_ordered_lists.ivy: line 38: assumption
        in action sum_absolute_pairs.right_val when called from the environment:
            sum_ordered_lists.ivy: line 43: assumption
            sum_ordered_lists.ivy: line 44: assumption

    The following program assertions are treated as guarantees:
        in action sum_absolute_pairs.right_val when called from the environment,the environment:
            sum_ordered_lists.ivy: line 49: guarantee ... FAIL
searching for a small model... done
[
    sum_absolute_pairs.stored_left = 1
    0:num + 0 = 0
    0:num + 1 = 0
    1:num + 0 = 0
    1:num + 1 = 0
    sum_absolute_pairs.sum = 1
    sum_absolute_pairs.side = right
    sum_absolute_pairs.prev_sum = 1
]
fail call sum_absolute_pairs.right_val
{
    [
        fml:x = 0
    ]
sum_ordered_lists.ivy: line 43: 
    assume [sum_absolute_pairs.asrt8] sum_absolute_pairs.side = right

sum_ordered_lists.ivy: line 44: 
    assume [sum_absolute_pairs.asrt9] sum_absolute_pairs.prev_sum = sum_absolute_pairs.sum

sum_ordered_lists.ivy: line 45: 
    sum_absolute_pairs.side := left

    [
        sum_absolute_pairs.side = left
    ]
sum_ordered_lists.ivy: line 70: 
    sum_absolute_pairs.sum := sum_absolute_pairs.sum + sum_absolute_pairs.stored_left - fml:x

    [
        sum_absolute_pairs.sum = 0
    ]
sum_ordered_lists.ivy: line 49: 
    assert [sum_absolute_pairs.asrt11] sum_absolute_pairs.sum > sum_absolute_pairs.prev_sum | sum_absolute_pairs.sum = sum_absolute_pairs.prev_sum

}

sum_absolute_pairs.ivy

#lang ivy1.7
# Toy model: accept a left number, then a right number, and
# add their absolute difference to a running sum

type side_t = {left, right}
type num

interpret num -> nat

# Throwing spaghetti at the wall here to try to get a 
# sensible model.
axiom X:num < Y & Y < Z -> X < Z
axiom ~(X:num < X)
axiom X:num < Y | X = Y | Y < X
axiom [monotonic] X:num < Y -> X+Z < Y+Z
axiom [nonneg] X:num + Y:num = 0 -> X = 0 & Y = 0
axiom [nonneg2] X:num >= 0

isolate sum_absolute_pairs = {
    action left_val(x:num)
    action right_val(x:num)
    action get_sum returns (r:num)

    specification {
	type this

	individual prev_sum : num

	## Must give one half of the pair, then the other
	individual side : side_t
	
	after init {
	    side := left;
	    prev_sum := sum;
	}

	before left_val(x:num) {
	    require side = left;
	    side := right;	    
	}
	
	before right_val(x:num) {
	    require side = right;
	    require prev_sum = sum;
	    side := left;
	}

	after right_val(x:num) {
	    ensure sum > prev_sum | sum = prev_sum;
	    prev_sum := sum;
	}
    }

    implementation {
	individual stored_left : num
	individual sum : num

	after init {
	    sum := 0
	}

	implement left_val(x:num) {
	    stored_left := x
	}

	implement right_val(x:num) {
	    if x >= stored_left {
		sum := sum + (x - stored_left)
	    } else {
		sum := sum + (stored_left - x)
            }
	}

	implement get_sum returns (r:num) {
	    r := sum
	}
    }
}

export sum_absolute_pairs.left_val
export sum_absolute_pairs.right_val
export sum_absolute_pairs.get_sum