Missing low-level instances

[tahina-pro]

List compiled by @ad-l

Sum types:

• finalizers for explicit sum types
• intro lemmas for implicit sum types
• accessors for explicit sum types
• accessors for implicit sum types

Structs:

• intro lemma

Vlbytes:

• length,
• index, slice Won't do; instead, I strengthen the postcondition of length to allow the user to take the corresponding subbuffer to access the contents
• finalizer

Vldata:

• accessor
• length?
• finalizer

Vlarray:

• count
• list "accessor" done as a strong postcondition given by count
• nth
• finalizer
• (no iterators)

Vllist:

• finalizer,
• list "accessor"
• count, ith: use generic list_length, list_nth from LowParse.Low.Base thanks to the list accessor

FLBytes:

• intro
• slice, nth elim, so that the user can take the subbuffer themselves

FLArray:

• intro,
• list "accessor"

Note that all such needed combinators are already in LowParse, we just need to instantiate them in QuackyDucky.

[tahina-pro]

Boxes checked above track progress on QuackyDucky branch taramana_lowparse.

• Merge into QuackyDucky master
• Test with miTLS

[ad-l]

Intro lemma for structs merged in QD a9e4f96