<table>
  <tr>
    <td>Buffer code</td>
    <td>(2)</td>
    <td>examples/buffer.v</td>
    <td>buffer_code</td>
  </tr>
  <tr>
    <td>Counter code</td>
    <td>(3)</td>
    <td>examples/minimal_counter.v</td>
    <td>counter_init0</td>
  </tr>
  <tr>
    <td>Semantics basics</td>
    <td>(4)</td>
    <td>machine_base.v</td>
    <td></td>
  </tr>
  <tr>
    <td>Operational semantics</td>
    <td>(5)</td>
    <td>caplang.v</td>
    <td></td>
  </tr>
  <tr>
    <td>Points-to predicates</td>
    <td>(6)</td>
    <td>rules/rules_base.v</td>
    <td></td>
  </tr>
  <tr>
    <td>Region points-to</td>
    <td>(7)</td>
    <td>region.v</td>
    <td>region_mapsto</td>
  </tr>
  <tr>
    <td>Program logic specs</td>
    <td>(8)</td>
    <td>rules.v</td>
    <td></td>
  </tr>
  <tr>
    <td>Rule for subseg (success)</td>
    <td>(10)</td>
    <td>rules/rules_Subseg.v</td>
    <td>wp_subsegsuccess_lr</td>
  </tr>
  <tr>
    <td>Rule for subseg (failure)</td>
    <td>(11)</td>
    <td>rules/rules_Subseg.v</td>
    <td>wp_subseg_fail_lr</td>
  </tr>
  <tr>
    <td>Rule for load</td>
    <td>(12)</td>
    <td>rules/rule_Load.v</td>
    <td>wp_loadsuccess_notinstr</td>
  </tr>
  <tr>
    <td>Rule for store</td>
    <td>(13)</td>
    <td>rules/rule_Store.v</td>
    <td>wp_storesuccess_reg</td>
  </tr>
  <tr>
    <td>General WP rule for subseg</td>
    <td>(14)</td>
    <td>rules/rules_Subseg.v</td>
    <td>wp_Subseg</td>
  </tr>
  <tr>
    <td>Rule for rclear</td>
    <td>(15)</td>
    <td>examples/macros_new.v</td>
    <td>rclear_spec</td>
  </tr>
  <tr>
    <td>Memory invariant</td>
    <td>(17)</td>
    <td>examples/template_adequacy.v</td>
    <td>memory_inv</td>
  </tr>
  <tr>
    <td>In region</td>
    <td>(19)</td>
    <td>logrel.v</td>
    <td>in_region</td>
  </tr>
  <tr>
    <td>Adequacy</td>
    <td>(18)</td>
    <td>examples/template_adequacy.v</td>
    <td>with_adv.template_adequacy</td>
  </tr>
  <tr>
    <td>Logical relation</td>
    <td>(20)</td>
    <td>logrel.v</td>
    <td>interp</td>
  </tr>
  <tr>
    <td>FTLR</td>
    <td>(21)</td>
    <td>fundamental.v</td>
    <td>fundamental_cap</td>
  </tr>
  <tr>
    <td>Regions are safe</td>
    <td>(22)</td>
    <td>logrel.v</td>
    <td>region_valid_in_region</td>
  </tr>
  <tr>
    <td>Jump to safe word</td>
    <td>(23)</td>
    <td>fundamental.v</td>
    <td>jmp_to_unknown</td>
  </tr>
  <tr>
    <td>Buffer spec</td>
    <td>(24)</td>
    <td>examples/buffer.v</td>
    <td>buffer_spec</td>
  </tr>
  <tr>
    <td>Buffer run spec</td>
    <td>(25)</td>
    <td>examples/buffer.v</td>
    <td>buffer_full_run_spec</td>
  </tr>
  <tr>
    <td>Buffer adequacy</td>
    <td>(26)</td>
    <td>examples/buffer.v</td>
    <td>adequacy</td>
  </tr>
  <tr>
    <td>Counter init spec</td>
    <td>(27)</td>
    <td>examples/minimal_counter.v</td>
    <td>counter_init_spec</td>
  </tr>
  <tr>
    <td>Increment spec</td>
    <td>(28)</td>
    <td>examples/minimal_counter.v</td>
    <td>counter_code_spec</td>
  </tr>
  <tr>
    <td>Counter adequacy</td>
    <td>(30)</td>
    <td>examples/minimal_counter.v</td>
    <td>adequacy</td>
  </tr>
  <tr>
    <td>Malloc invariant</td>
    <td>(31)</td>
    <td>examples/malloc.v</td>
    <td>malloc_inv</td>
  </tr>
  <tr>
    <td>Malloc spec</td>
    <td>(32)</td>
    <td>examples/malloc.v</td>
    <td>simple_malloc_subroutine_spec</td>
  </tr>
  <tr>
    <td>Malloc is safe</td>
    <td>(33)</td>
    <td>examples/malloc.v</td>
    <td>simple_malloc_subroutine_valid</td>
  </tr>
  <tr>
    <td>Assert invariant</td>
    <td>(34)</td>
    <td>examples/assert.v</td>
    <td>assert_inv</td>
  </tr>
  <tr>
    <td>Assert spec</td>
    <td>(35)</td>
    <td>examples/assert.v</td>
    <td>assertsuccess_spec</td>
  </tr>
  <tr>
    <td>Call spec</td>
    <td>(36)</td>
    <td>examples/call.v</td>
    <td>call_spec</td>
  </tr>
  <tr>
    <td>Activation code</td>
    <td>(37)</td>
    <td>examples/call.v</td>
    <td>hw_1</td>
  </tr>
  <tr>
    <td>Activation spec</td>
    <td>(38)</td>
    <td>examples/callback.v</td>
    <td>scall_epilogue_spec</td>
  </tr>
  <tr>
    <td>RO spec</td>
    <td>(40)</td>
    <td>examples/lse.v</td>
    <td>roe_spec</td>
  </tr>
  <tr>
    <td>RO adequacy</td>
    <td>(41)</td>
    <td>examples/lse_adequacy.v</td>
    <td>roe_adequacy</td>
  </tr>
  <tr>
    <td>Interval library</td>
    <td>(42)</td>
    <td>examples/interval.v</td>
    <td></td>
  </tr>
  <tr>
    <td>Interval client</td>
    <td>(43)</td>
    <td>examples/interval_client.v</td>
    <td></td>
  </tr>
  <tr>
    <td>Seal spec</td>
    <td>(45)</td>
    <td>examples/dynamic_sealing.v</td>
    <td>seal_spec</td>
  </tr>
  <tr>
    <td>Unseal spec</td>
    <td>(46)</td>
    <td>examples/dynamic_sealing.v</td>
    <td>unseal_spec</td>
  </tr>
  <tr>
    <td>Seal invariant</td>
    <td>(44)</td>
    <td>examples/keylist.v</td>
    <td>seallL</td>
  </tr>
  <tr>
    <td>FindB code</td>
    <td>(47)</td>
    <td>examples/keylist.v</td>
    <td>findb</td>
  </tr>
  <tr>
    <td>Append code</td>
    <td>(48)</td>
    <td>examples/keylist.v</td>
    <td>appendb</td>
  </tr>
  <tr>
    <td>isInterval</td>
    <td>(49)</td>
    <td>examples/interval.v</td>
    <td>isInterval</td>
  </tr>
  <tr>
    <td>isInterval agree</td>
    <td>(50)</td>
    <td>examples/interval.v</td>
    <td>intervals_agree</td>
  </tr>
  <tr>
    <td>Interval adequacy</td>
    <td>(51)</td>
    <td>examples/interval_client_adequacy.v</td>
    <td>template_adequacy</td>
  </tr>
</table>