further testing needed

Tests/isa/CPrograms/main.c

@@ -0,0 +1,50 @@
+#include <cheriintrin.h>
+#include <stdint.h>
+
+void test() {
+
+    void *__capability c1;
+
+    // Set address
+    c1 = (void *__capability)0x80001009;
+
+    c1 = cheri_bounds_set(c1, 8);
+
+}
+
+// Add delta value for TLB translation
+static inline void * __capability add_delta(void * __capability cap, int offset) {
+    void * __capability result;
+
+    asm volatile (
+        "cincoffset %0, %1, %2"
+        : "=C" (result)  // Output: %0 (result)
+        : "C" (cap),     // Input:  %1 (original cap)
+          "r" (offset)   // Input:  %2 (offset register)
+        :                // No clobbered registers
+    );
+
+    return result;
+}
+
+int main(void) {
+    void *__capability csp1;
+
+    // Set address
+    csp1 = (void *__capability)0x80001000;
+
+    // Set bounds
+    csp1 = cheri_bounds_set(csp1, 1);
+    // Increment offset
+    // csp = cheri_offset_increment(csp, 10);
+    csp1 = add_delta(csp1, 10);
+
+    // uint64_t val = *(uint64_t * __capability)csp1;
+
+
+
+    // uint64_t val = *(uint64_t *__capability)csp1;
+    test();
+
+    return 0;
+}

Tests/isa/CPrograms/start.S

@@ -0,0 +1,41 @@
+    .section .text
+    .globl _start
+    .align 4
+_start:
+    # cspecialr c1, pcc
+
+    # Use csetaddr to build a stack capability
+    # li t0, 0x80001000        # fixed top-of-stack address
+    # csetaddr csp, ct0, t0
+
+    # bound it to 8 bytes (size of dword)
+    # li t2, 8
+    # csetbounds csp, csp, t2
+    # li t5, 4
+    # cincoffsetimm csp, csp, 5
+
+    # Read bounds
+    # cgetbase   t3, csp
+    # ld t0, 0(csp)
+    # derive capability from PCC
+    # csetaddr c1, ct0, t0
+
+    cspecialr ca0, pcc           # Get the root data capability
+    li        t0, 0x80002000     # Set top of stack address
+    csetaddr  csp, ca0, t0       # Set address
+    li        t1, -2048          # 2KB size
+    csetbounds csp, csp, t1      # Restrict bounds so main can't wander
+    cincoffsetimm csp, csp, 12
+
+    # Call main
+    # sw         ra, 12(sp)
+    call main
+
+    # a0 contains return value
+    mv t1, a0
+
+    # la      t0, tohost
+    # Signal success
+    la      t0, 0
+    li      t1, 1
+    sd      t1, 0(t0)

Tests/isa/PageCompileSteps.txt

@@ -1,4 +1,9 @@
 ./riscv64-unknown-elf-gcc -nostdlib -nostartfiles   -Wl,-Ttext=0x80000000   Page.S   -o Page.o
 ./riscv64-unknown-elf-objcopy --remove-section .bss Page.o Page
 # Copy file
-scp home:/home/akilan/Documents/cheri/riscv/riscv/bin/Page .
+scp home:/home/akilan/Documents/cheri/riscv/riscv/bin/Page .
+
+./clang   --target=riscv64-unknown-elf   -march=rv64gcxcheri -mabi=l64pc128 -nostdlib -nostartfiles   -Wl,-Ttext=0x80000000 -o testC cheri-bounds-seal-change-read.S (Compile riscv bare-metal)
+
+# Copy test file back
+scp home:/home/akilan/cheri/output/sdk/bin/testC .

Tests/isa/PageRead.S

@@ -92,7 +92,7 @@ vm_boot:
 
     # l1_pt[0] -> l0_pt
     la      t0, l0_pt
-    srli    t0, t0, 12  
+    srli    t0, t0, 12
     slli    t0, t0, 10
     ori     t0, t0, 0x1         # V
     la      t1, l1_pt

Tests/isa/build-assembler.sh

@@ -0,0 +1,16 @@
+# Send assembler file to remote machine to run
+# scp Cprograms/start.S home:/home/akilan/cheri/output/sdk/bin/
+# scp Cprograms/main.c home:/home/akilan/cheri/output/sdk/bin/
+
+scp cheri.S home:/home/akilan/cheri/output/sdk/bin/
+
+# Run compiled instruction remotely
+ssh home 'cd /home/akilan/cheri/output/sdk/bin/ && ./clang   --target=riscv64-unknown-elf   -march=rv64gcxcheri -mabi=l64pc128 -nostdlib -nostartfiles   -Wl,-Ttext=0x80000000 -o testC cheri.S'
+
+# ssh home 'cd /home/akilan/cheri/output/sdk/bin/ && ./clang   --target=riscv64-unknown-elf   -march=rv64gcxcheri -mabi=lp64d -nostdlib -nostartfiles   -Wl,-Ttext=0x80000000 -o testC start.S main.c'
+
+# Disassembly ouput
+ssh home 'cd /home/akilan/cheri/output/sdk/bin/ && ./llvm-objdump -d testC'
+
+# Copy file back for testing
+scp home:/home/akilan/cheri/output/sdk/bin/testC .

Tests/isa/cheri.S

@@ -0,0 +1,26 @@
+    .section .text
+    .globl _start
+    .align 4
+_start:
+    cspecialr ct0, pcc
+
+    # Use csetaddr to build a stack capability
+    li t0, 0x80001000        # fixed top-of-stack address
+    csetaddr csp, ct0, t0
+
+    # bound it to 8 bytes (size of dword)
+    li t2, 8
+    csetbounds csp, csp, t2
+    # li t5, 4
+    cincoffsetimm csp, csp, 10
+
+    # Read bounds
+    cgetbase   t3, csp
+    ld t0, 0(csp)
+    # derive capability from PCC
+    # csetaddr c1, ct0, t0
+
+    # la      t0, tohost
+    li      t1, 1
+    csd     t1, 0(c1)
+

Tests/isa/cheri.c

@@ -0,0 +1,20 @@
+#include <cheriintrin.h>
+#include <stdint.h>
+
+int main() {
+    void *__capability csp;
+
+    // Set address
+    csp = (void *__capability)0x80001000;
+
+    // Set bounds
+    csp = cheri_bounds_set(csp, 8);
+
+    // Increment offset
+    csp = cheri_offset_increment(csp, 10);
+
+    uint64_t val = *(uint64_t *__capability)csp;
+
+    while (1) {}
+    return 0;
+}

builds/RV64ACDFIMSUxCHERI_Toooba_bluesim/Makefile

@@ -12,7 +12,8 @@ BSC_COMPILATION_FLAGS += -verbose
 # TEST ?= rv64um-v-mulw
 # TEST ?= Page
 # TEST ?= PageReadWrite
-TEST ?= CheriPage
+# TEST ?= CheriPage
+TEST ?= testC
 
 #================================================================
 # Parameter settings for MIT RISCY, setup paths etc. for Include_Common

builds/RV64ACDFIMSUxCHERI_Toooba_bluesim/checklist.org

@@ -0,0 +1,6 @@
+- [x] Get sample cheri assembly program to quit.
+- [x] Get sample get bounds program working.
+- [x] Check if the hardware handler function is called.
+- [ ] Write a sample C program can boot with capabilities.
+- [ ] Implement new intruction as the form Cseal.
+- [ ] Sample assembler program that calls it.

builds/Resources/Include_RISCY_Config.mk

@@ -112,6 +112,8 @@ BSC_COMPILATION_FLAGS += \
 	-D RISCV \
 	-D TSO_MM \
 	-D RV64 \
+	-D PERF_COUNT \
+	-D PERFORMANCE_MONITORING \
 	-D ISA_PRIV_M  -D ISA_PRIV_S  -D ISA_PRIV_U  \
 	-D SV39 \
 	-D ISA_I  -D ISA_M  -D ISA_A  -D ISA_F  -D ISA_D  -D ISA_FD_DIV  -D ISA_C  \

src_Core/CPU/Core.bsv

@@ -918,6 +918,7 @@ module mkCore#(CoreId coreId)(Core);
     // incr cycle count
     (* fire_when_enabled, no_implicit_conditions *)
     rule incCycleCnt(doStats);
+        // $display("calling cycle");
         cycleCnt.incr(1);
     endrule
 

src_Core/CPU/CsrFile.bsv

@@ -330,7 +330,7 @@ interface StatsCsr;
 endinterface
 
 module mkStatsCsr(StatsCsr);
-    Reg#(Bool) doStats <- mkConfigReg(False);
+    Reg#(Bool) doStats <- mkConfigReg(True);
 
     FIFO#(Bool) writeQ <- mkFIFO1;
 

src_Core/RISCY_OOO/procs/RV64G_OOO/MemExePipeline.bsv

@@ -124,6 +124,8 @@ typedef struct {
     // result
     ByteOrTagEn shiftedBE;
     CapPipe vaddr;         // virtual addr
+    Bit#(25) delta;
+
 `ifdef INCLUDE_TANDEM_VERIF
     // for those mem instrs that store data
     Data    store_data;
@@ -597,13 +599,11 @@ module mkMemExePipeline#(MemExeInput inIfc)(MemExePipeline);
         });
     endrule
 
-    rule doExeMem;
+    rule doExeAndDoMem;
         regToExeQ.deq;
         let regToExe = regToExeQ.first;
         let x = regToExe.data;
-        // trollToExeQ.enq(regToExe);
-        // ==============================
-        if(verbose) $display("%t : [doExeMem] ", $time, fshow(regToExe));
+        if(verbose) $display("%t : [doExeAndDoMem] ", $time, fshow(regToExe));
 
         let shiftBE = DataMemAccess(x.shiftBEData);
         if (x.origBE == TagMemAccess) begin
@@ -618,11 +618,53 @@ module mkMemExePipeline#(MemExeInput inIfc)(MemExePipeline);
             accessByteCount = fromInteger(valueOf(CacheUtils::CLineNumMemDataBytes));
         end
 
+    // rule doExeMem;
+    //     regToExeQ.deq;
+    //     let regToExe = regToExeQ.first;
+    //     let x = regToExe.data;
+    //     // trollToExeQ.enq(regToExe);
+    //     // ==============================
+    //     if(verbose) $display("%t : [doExeMem] ", $time, fshow(regToExe));
+
+    //     let shiftBE = DataMemAccess(x.shiftBEData);
+    //     if (x.origBE == TagMemAccess) begin
+    //         shiftBE = TagMemAccess;
+    //     end
+
+    //     CapPipe ddc = cast(inIfc.scaprf_rd(scrAddrDDC));
+
+    //     // get size of the access
+    //     Bit#(TAdd#(CacheUtils::LogCLineNumMemDataBytes,1)) accessByteCount = zeroExtend(pack(countOnes(pack(x.origBE.DataMemAccess))));
+    //     if (x.origBE == TagMemAccess) begin
+    //         accessByteCount = fromInteger(valueOf(CacheUtils::CLineNumMemDataBytes));
+    //     end
+
+    //     // Test delta value read from the pointer
+    //     Bit#(25) delta = decodeDelta(x.vaddr);
+    //     $display("Decoded delta = %0d", delta);
+    //     x.vaddr = encodeDelta(x.vaddr, 0);
+
+
+
 `ifdef KONATA 
         $display("KONATAE\t%0d\t%0d\t0\tMem2", cur_cycle, x.u_id);
         $display("KONATAS\t%0d\t%0d\t0\tMem3", cur_cycle, x.u_id);
         $fflush;
 `endif
+        // Test delta value read from the pointer
+        Bit#(25) delta = decodeDelta(x.vaddr);
+        $display("Decoded delta from register = %0d", delta);
+
+        // 33554431 is 2^25 - 1 (all ones)
+        if (delta == 33554431) begin
+            delta = 0;
+        end else begin
+            x.vaddr = encodeDelta(x.vaddr, 0);
+        end
+        // x.vaddr = encodeDelta(x.vaddr, 0);
+        // x.vaddr = (x.vaddr >> 25) << 25;
+        // x.vaddr = (x.vaddr >> 25) << 25;
+
         // go to next stage by sending to TLB
         dTlb.procReq(DTlbReq {
             inst: MemExeToFinish {
@@ -631,6 +673,7 @@ module mkMemExePipeline#(MemExeInput inIfc)(MemExePipeline);
                 ldstq_tag: x.ldstq_tag,
                 shiftedBE: shiftBE,
                 vaddr: x.vaddr,
+                delta: delta,
 `ifdef INCLUDE_TANDEM_VERIF
                 store_data: x.rVal2,
                 store_data_BE: origBE,
@@ -658,6 +701,11 @@ module mkMemExePipeline#(MemExeInput inIfc)(MemExePipeline);
         let dTlbResp = dTlb.procResp;
         let x = dTlbResp.inst;  
         let {paddr, expCause, allowCapPTE} = dTlbResp.resp;
+        Bit#(25) delta = x.delta;
+        $display("Received delta = %0d", delta);
+
+        paddr = paddr + zeroExtend(delta);
+
         // paddr = getAddr(lol.vaddr);
         // expCause = False;
         // allowCapPTE = True;

src_Core/RISCY_OOO/procs/lib/DTlb.bsv

@@ -233,6 +233,14 @@ module mkDTlb#(
             L1TlbAllMissCycles: (allMissCycles);
             default: (0);
         endcase);
+        // Print the requested counter and its value
+        $display("[doPerf] Request Type: %0d, Value: %0d", t, d);
+
+        // (Optional) More detailed debug info
+        $display("  accessCnt=%0d, missParentCnt=%0d, missParentLat=%0d",
+             accessCnt, missParentCnt, missParentLat);
+        $display("  L1TlbmissPeerCnt=%0d, L1TlbmissPeerLat=%0d, L1TlbhitUnderMissCnt=%0d, L1TlballMissCycles=%0d",
+             missPeerCnt, missPeerLat, hitUnderMissCnt, allMissCycles);
         perfRespQ.enq(PerfResp {
             pType: t,
             data: d
@@ -471,93 +479,93 @@ module mkDTlb#(
             noAction;
         end
 `endif
-        else if (vm_info.sv39) begin
-            let vpn = getVpn(r.addr);
-            let trans_result = tlb.translate(vpn, vm_info.asid);
-            if (!validVirtualAddress(r.addr)) begin
-                // page fault
-                Exception fault = r.write ? excStorePageFault : excLoadPageFault;
-                pendWait[idx] <= None;
-                pendResp[idx] <= tuple3(?, Valid (fault), False);
-                if(verbose) $display("[DTLB] req invalid virtual address: idx %d; ", idx, fshow(r));
-            end else if (trans_result.hit) begin
-                // TLB hit
-                let entry = trans_result.entry;
-                // check permission
-            $display("procReq: vm_info: ", fshow(vm_info),
-                     "         en     : ", fshow(entry),
-                     "         r      : ", fshow(r)
-                     );
-                let permCheck = hasVMPermission(vm_info,
-                                                entry.pteType,
-                                                entry.pteUpperType,
-                                                entry.ppn,
-                                                entry.level,
-                                                r.write ? DataStore : DataLoad,
-                                                r.capStore,
-                                                r.potentialCapLoad);
-                $display("Permission check output 2: ", fshow(permCheck));
-                if (permCheck.allowed) begin
-                    // update TLB replacement info
-                    tlb.updateRepByHit(trans_result.index);
-                    // translate addr
-                    Addr trans_addr = translate(r.addr, entry.ppn, entry.level);
-                    pendWait[idx] <= None;
-                    pendResp[idx] <= tuple3(trans_addr, Invalid, permCheck.allowCap);
-                    if(verbose) begin
-                        $display("[DTLB] req (hit): idx %d; ", idx, fshow(r),
-                                 "; ", fshow(trans_result));
-                    end
-`ifdef PERF_COUNT
-                    // perf: hit under miss
-                    if(doStats && readVReg(pendWait) != replicate(None)) begin
-                        hitUnderMissCnt.incr(1);
-                    end
-`endif
-                end
-                else begin
-                    // page fault
-                    Exception fault = permCheck.excCode;
-                    pendWait[idx] <= None;
-                    pendResp[idx] <= tuple3(?, Valid (fault), False);
-                    if(verbose) $display("[DTLB] req no permission: idx %d; ", idx, fshow(r));
-                end
-            end
-            else begin
-                // TLB miss, req to parent TLB only if there is no existing req
-                // for the same VPN already waiting for parent TLB resp
-                function Bool reqSamePage(DTlbReqIdx i);
-                    // we can ignore pendValid here, because not-None pendWait implies
-                    // pendValid is true
-                    let r_i = getTlbReq(pendInst[i]);
-                    return pendWait[i] == WaitParent && getVpn(r.addr) == getVpn(r_i.addr);
-                endfunction
-                Vector#(DTlbReqNum, DTlbReqIdx) idxVec = genWith(fromInteger);
-                if(find(reqSamePage, idxVec) matches tagged Valid .i) begin
-                    // peer entry has already requested, so don't send duplicate req
-                    pendWait[idx] <= WaitPeer (i);
-                    doAssert(pendValid_procReq[i], "peer entry must be valid");
-                    if(verbose) begin
-                        $display("[DTLB] req miss, pend on peer: idx %d, ",
-                                 idx, "; ", fshow(r), "; ", fshow(i));
-                    end
-                end
-                else begin
-                    // this is the first req for this VPN
-                    pendWait[idx] <= WaitParent;
-                    rqToPQ.enq(DTlbRqToP {
-                        vpn: vpn,
-                        id: idx
-                    });
-                    if(verbose) begin
-                        $display("[DTLB] req miss, send to parent: idx %d, ",
-                                 idx, fshow(r));
-                    end
-                end
-                // perf: miss
-                latTimer.start(idx);
-            end
-        end
+//         else if (vm_info.sv39) begin
+//             let vpn = getVpn(r.addr);
+//             let trans_result = tlb.translate(vpn, vm_info.asid);
+//             if (!validVirtualAddress(r.addr)) begin
+//                 // page fault
+//                 Exception fault = r.write ? excStorePageFault : excLoadPageFault;
+//                 pendWait[idx] <= None;
+//                 pendResp[idx] <= tuple3(?, Valid (fault), False);
+//                 if(verbose) $display("[DTLB] req invalid virtual address: idx %d; ", idx, fshow(r));
+//             end else if (trans_result.hit) begin
+//                 // TLB hit
+//                 let entry = trans_result.entry;
+//                 // check permission
+//             $display("procReq: vm_info: ", fshow(vm_info),
+//                      "         en     : ", fshow(entry),
+//                      "         r      : ", fshow(r)
+//                      );
+//                 let permCheck = hasVMPermission(vm_info,
+//                                                 entry.pteType,
+//                                                 entry.pteUpperType,
+//                                                 entry.ppn,
+//                                                 entry.level,
+//                                                 r.write ? DataStore : DataLoad,
+//                                                 r.capStore,
+//                                                 r.potentialCapLoad);
+//                 $display("Permission check output 2: ", fshow(permCheck));
+//                 if (permCheck.allowed) begin
+//                     // update TLB replacement info
+//                     tlb.updateRepByHit(trans_result.index);
+//                     // translate addr
+//                     Addr trans_addr = translate(r.addr, entry.ppn, entry.level);
+//                     pendWait[idx] <= None;
+//                     pendResp[idx] <= tuple3(trans_addr, Invalid, permCheck.allowCap);
+//                     if(verbose) begin
+//                         $display("[DTLB] req (hit): idx %d; ", idx, fshow(r),
+//                                  "; ", fshow(trans_result));
+//                     end
+// `ifdef PERF_COUNT
+//                     // perf: hit under miss
+//                     if(doStats && readVReg(pendWait) != replicate(None)) begin
+//                         hitUnderMissCnt.incr(1);
+//                     end
+// `endif
+//                 end
+//                 else begin
+//                     // page fault
+//                     Exception fault = permCheck.excCode;
+//                     pendWait[idx] <= None;
+//                     pendResp[idx] <= tuple3(?, Valid (fault), False);
+//                     if(verbose) $display("[DTLB] req no permission: idx %d; ", idx, fshow(r));
+//                 end
+//             end
+//             else begin
+//                 // TLB miss, req to parent TLB only if there is no existing req
+//                 // for the same VPN already waiting for parent TLB resp
+//                 function Bool reqSamePage(DTlbReqIdx i);
+//                     // we can ignore pendValid here, because not-None pendWait implies
+//                     // pendValid is true
+//                     let r_i = getTlbReq(pendInst[i]);
+//                     return pendWait[i] == WaitParent && getVpn(r.addr) == getVpn(r_i.addr);
+//                 endfunction
+//                 Vector#(DTlbReqNum, DTlbReqIdx) idxVec = genWith(fromInteger);
+//                 if(find(reqSamePage, idxVec) matches tagged Valid .i) begin
+//                     // peer entry has already requested, so don't send duplicate req
+//                     pendWait[idx] <= WaitPeer (i);
+//                     doAssert(pendValid_procReq[i], "peer entry must be valid");
+//                     if(verbose) begin
+//                         $display("[DTLB] req miss, pend on peer: idx %d, ",
+//                                  idx, "; ", fshow(r), "; ", fshow(i));
+//                     end
+//                 end
+//                 else begin
+//                     // this is the first req for this VPN
+//                     pendWait[idx] <= WaitParent;
+//                     rqToPQ.enq(DTlbRqToP {
+//                         vpn: vpn,
+//                         id: idx
+//                     });
+//                     if(verbose) begin
+//                         $display("[DTLB] req miss, send to parent: idx %d, ",
+//                                  idx, fshow(r));
+//                     end
+//                 end
+//                 // perf: miss
+//                 latTimer.start(idx);
+//             end
+//         end
         else begin
             // bare mode
             pendWait[idx] <= None;

src_Core/RISCY_OOO/procs/lib/Exec.bsv

@@ -241,9 +241,12 @@ function CapPipe capModify(CapPipe a, CapPipe b, CapModifyFunc func);
     new_hard_perms.global = new_hard_perms.global && getHardPerms(b).global;
     Bool unsealIllegal = !isValidCap(b) || getKind(b) != UNSEALED || getKind(a) == UNSEALED || a_res || getAddr(b) != a_type || !getHardPerms(b).permitUnseal || !isInBounds(b, False);
     Bool buildCapIllegal = !isValidCap(b) || getKind(b) != UNSEALED || !isDerivable(a) || (getPerms(a) & getPerms(b)) != getPerms(a) || getBase(a) < getBase(b) || getTop(a) > getTop(b); // XXX needs optimisation
+    // TODO: Delta handler function 
     CapPipe res = (case(func) matches
             tagged ModifyOffset .offsetOp :
-                modifyOffset(a_mut, getAddr(b), offsetOp == IncOffset).value;
+                // modifyOffset(a_mut, getAddr(b), offsetOp == IncOffset).value;
+                // To test this
+                encodeDelta(a_mut, getAddr(b));
             tagged SetBounds .boundsOp    :
                 setBoundsALU(a_mut, getAddr(b), boundsOp);
             tagged SpecialRW .scrType     :
@@ -274,6 +277,8 @@ function CapPipe capModify(CapPipe a, CapPipe b, CapModifyFunc func);
                 (getAddr(a) == 0 ? nullCap : setAddr(b_mut, getAddr(a)).value);
             tagged SetHigh:
                 fromMem(tuple2(False, {getAddr(b), getAddr(a)}));
+                // capFromAddrs(a,b);
+                // getTruncatedTuple(getAddr(b))
             tagged BuildCap               :
                 setKind(setValidCap(a_mut, !buildCapIllegal), getKind(a)==SENTRY ? SENTRY : UNSEALED);
             tagged Move                   :
@@ -285,6 +290,38 @@ function CapPipe capModify(CapPipe a, CapPipe b, CapModifyFunc func);
     return res;
 endfunction
 
+// function CapPipe capFromAddrs (CapPipe a, CapPipe b)
+// provisos (
+//     CHERICap#(CapPipe, o, f, addrW, CapW, m, d)
+// );
+
+//     // Get full serialized capability of 'a'
+//     match {.tag, .rawA} = toMem(a);   // rawA : Bit#(inMemW)
+
+//     // Replace low addrW bits with address from b
+//     Bit#(addrW) newAddr = getAddr(b);
+
+//     Bit#(inMemW) newRaw =
+//         { rawA[CapW-1 : addrW]   // keep upper metadata
+//         , newAddr                  // replace address field
+//         };
+
+//     return fromMem(tuple2(tag, newRaw));
+
+// endfunction
+// function CapPipe capFromAddrs(capT a, capT b)
+//     // Extract addresses
+//     Bit#(64) addrA = getAddr(a);
+//     Bit#(64) addrB = getAddr(b);
+//     // Extra bits to reach inMemW = 180
+//     Bit#(52) extra  = 0; // can be zeros or delta bits if needed
+
+//     // Concatenate explicitly typed
+//     Bit#(180) rawBits = {addrB, addrA, extra};
+
+//     return fromMem(tuple2(False, rawBits));
+// endfunction
+
 (* noinline *)
 function Data capInspect(CapPipe a, CapPipe b, CapInspectFunc func);
     Data res = (case(func) matches
@@ -323,6 +360,17 @@ function Data capInspect(CapPipe a, CapPipe b, CapInspectFunc func);
     return res;
 endfunction
 
+// function CapPipe getTruncatedTuple(AddrType a, AddrType b)
+//     provisos (
+//         Add#(a__, b__, 180) // Defines that a__ + b__ must equal 180
+//     );
+
+//     // Use a list literal or a Tuple constructor
+//     let address_bits = { getAddr(b), getAddr(a) };
+    
+//     return fromMem(tuple2(False, address_bits));
+// endfunction
+
 function CapPipe capALU(CapPipe a, CapPipe b, CapFunc func);
     CapPipe res = (case (func) matches
         tagged CapInspect .x: