theory to support potential move to patricia trees

Prove a theorem:
  |- good_label_map ls 0 l fn [] /\ IS_PTREE fn ==>
     code_labels l ls = inst_labels_fn fn ls

Thus, to compute code_labels l ls, it is sufficient to compute
inst_labels_fn for a patricia tree fn (that can be constructed outside
the logic) as long as you can prove good_label_map and IS_PTREE.

inst_labels_fn can be computed as inst_labels currently is, except using
fast patricia conversions instead of the linear lookup based on
FLOOKUP_FUPDATE.

good_label_map is a single pass down the code list looking for Label
instructions and checking that the ptree maps them to the correct
address; it also needs to check the domain of the ptree at the end (i.e.
it doesn't contain extra entries): I'm hoping both lookups and getting
the domain are fast on existing ptrees. also hoping IS_PTREE is easy to
prove on a ptree generated with mk_ptree.

plan is to build the ptree with mk_ptree after doing the collect_labels
algorithm in ML.