GitLab

Squash the following:
- add bf_nested; test pgtable abstract stage functions
- try BFInline
- typed BFInline; test pgtable
- frontend: no-arg bitfield by default
- add constraints and wf conditions to bitfield type
- prove inline rules
- more typeclasses for inlining rule side conditions
- move signature axioms into SigWf
- update BitfieldDesc in exampels
- remove bitfield_raw typing rules
- bf_inline during simplify_hyp
- support nested signatures
- add bitfield init annot
- refactor mask core
- remove diverging instances
- support int -> term conversion
- prove properties for int_to_tm
- clean up most typing rules
- support negated int mask; test examples
- clean up mask_core
- fix stage2_map_set_prot_attr
- solve land and lor sideconditions
- solve_sig_wf tactic
- clean admits in pgtable_lemmas.v
- clean admits in other examples
- frontend: generate basic instances
- frontend test: pgtable
- wrap calculus defs in a module
- support rc::record; test frontend for tcp_input
- verify mt76_mac_tx_rate_val
- annotations for mt7601u/mac