project-everest/mitls-fstar

Implement Extensions

sishtiaq opened this issue · 1 comments

sishtiaq commented

Work item for 1.3 Extensions.

  • Define data type.
  • Define parsing and serializing functions. Write tests for them. Prove them inverse. 
    extensionBytes  : extension -> Tot bytes 
parseExtensions : bytes -> Tot (list extension)
  • Define prepareExtensions: 
    prepareExtensions : config -> extensions
    for Nego.
s-zanella commented

Done for mandatory extensions. Closing.