// Hand-optimized TASM baseline: os.neptune.locks.symmetric

// 5-field preimage lock: divine lock_hash, divine preimage (5 fields),
// hash, assert matches, read kernel hash.

os_neptune_locks_symmetric__main:
    divine 5
    divine 5
    push 0
    push 0
    push 0
    push 0
    push 0
    swap 9
    swap 1
    swap 8
    swap 1
    swap 2
    swap 7
    swap 2
    swap 3
    swap 6
    swap 3
    swap 4
    swap 5
    swap 4
    hash
    swap 4
    swap 1
    swap 3
    swap 1
    assert_vector
    pop 5
    read_io 5
    pop 5
    return

Graph