For reference: the Noir verify_proof

fn verify_proof(
_verification_key : [Field], 
_proof : [Field], 
_public_inputs : [Field], 
_key_hash : Field, 
_input_aggregation_object : [Field]) 
-> [Field] {}

Procedure to compute r from sub-hashes and valid paths to r for sub hashes

fn ( addr_sorted_0, time_sorted_0 ) {
    var r0 = 0;
    for (var i = 0..addr_sorted_0.len) {
        r0 = Hash(addr_sorted[i], r)
    }
	for (var i = 0..time_sorted_0.len) {
        r0 = Hash(time_sorted[i], r)
    }    
    
    r0
}

// recursive
fn (r0, r1, ...) {
    verify_proof(..., r0, )
    verify_proof(..., r1, )
    ...
    
    compute_merkle_root_and_paths(sub_hashes_r)
}

Procedure to compute sub permutation products

fn ( addr_sorted_0, time_sorted_0, r, paths0 ) {
    var addr_perm_0 = 0
    var time_perm_0 = 0
    var r0 = 0;
    for (var i = 0..addr_sorted_0.len) {
        addr_perm_0 = (addr_sorted_0[i] - r)*addr_perm_0
        r0 = Hash(addr_sorted[i], r)
    }
	for (var i = 0..time_sorted_0.len) {
        time_perm_0 = (time_perm_0[i] - r)*addr_perm_0
        r0 = Hash(time_sorted[i], r)
    }    
    
    is_valid_path(r0, paths0, r)
    
    
    (addr_perm_0, time_perm_0)
}


//recursive
fn(addr_perm_0,...addr_perm_n, time_perm_0,...,time_perm_n) {
    verify_proof(..., addr_perm_0, )
    verify_proof(..., time_perm_0, )    
    ...
    
    var final_addr_perm = addr_perm_0 * ... * addr_perm_n
    var final_time_perm = time_perm_0 * ... * time_perm_n
    
    assert final_addr_perm = final_time_perm
}

Procedure to verify begin and end sequences

fn (time_sorted_0, time_sorted_n_old, r) {
    //should be same length, we assume emulator reads out memory in order
    for (var i = 0 .. time_sorted_0.len) {
        assert time_sorted_0[i] = time_sorted_n_old[i]
    }
    
    compute_permutation_check(time_sorted_0, r)
}

//can recursively collect permutations and assertions if readout is too large

Procedure to verify opcodes

//selected subset of array which includes read opcodes, read args, and relavant reads/writes for each op
fn (time_sorted_opcodes, r) {
    while (i < time_sorted_opcodes.len) {
        // check time_sorted_opcodes reads opcode
        // check the arg is correct to address mode
        // check computation of reads / writes
        //update i
    }
    
    compute_permutation_check(time_sorted_opcodes, r)
}

//recursively collect opcodes and compute final permutation check for full time_sorted_array
fn ( ... , r) {
    verify(op1_0)
    verify(op1_1)
    ...
    verify(opN_N)
    
    compute_permutation_check(..., r)
}

The final aggregate proof will bring all procedures together, can make assertions all the permutation checks across the aggregates match