fstar --indent

[fournet]

Pretty printing is looking good, but we still need to fix a few issues before we can use it to normalize our source code. Here are my notes from a diff on miTLS files TLSConstants.fst and HandshakeLog.fsti.

• perror __SOURCE_FILE__ __LINE__ should not be evaluated! Similarly \n etc should not be evaluated.

• unnecessary empty lines are added, e.g. 9 lines above module at the start of the file.

• comments need work, although I suspect this is hard to fix. Trailing comments as in 41 // or maybe 42? are moved to the line above, or below; this is confusing and often forces new line. For example

  let is_handshake13_signatureScheme = function
  | ECDSA_SECP256R1_SHA256
  | ECDSA_SECP384R1_SHA384
  | ECDSA_SECP521R1_SHA512
  //| ED25519_SHA512
  //| ED448_SHAKE256
  | RSA_PSS_SHA256
  | RSA_PSS_SHA384
  | RSA_PSS_SHA512 -> true
  | _ -> false
  

  becomes

  let is_handshake13_signatureScheme =
  function
  | ECDSA_SECP256R1_SHA256
  | ECDSA_SECP384R1_SHA384
  | ECDSA_SECP521R1_SHA512
  | RSA_PSS_SHA256
  | RSA_PSS_SHA384
  | RSA_PSS_SHA512
    ->
    //| ED25519_SHA512
    //| ED448_SHAKE256
    true
  | _ -> false
  

  and similarly with infix (* foo *) comments.
  It also seems that (**************************************************************************) is entirely dropped, and different kinds of successive comments are reordered.

• Somes sequences of let..in are weird, e.g.

  SIG_UNKNOWN of
  ((codepoint:lbytes 2{
  let v = int_of_bytes codepoint
          
  in
  v <> 0x0401 /\ v <> 0x0501 /\ v <> 0x0601 /\ v <> 0x0403 /\ v <> 0x0503 /\ v <> 0x0603 /\
  v <> 0x0804 /\
  v <> 0x0805 /\
  v <> 0x0806 /\
  // /\ v <> 0x0807 /\ v <> 0x0808
  v <> 0x0201 /\
  v <> 0x0203 /\
  v <> 0x0202 /\
  v <> 0x0402 /\
  v <> 0x0502 /\
  v <> 0x0602 /\
  v <> 0xFFFF }))
  

  and

  val parseCompressions :
  b:bytes{ length b <= 254 } ->
  Tot ((cms:compressions{ List.length cms = length b })) (decreases (length b))
  let rec parseCompressions b =
  if length b = 0
  then
    
  let cms : list compression = []
    
  in
  //libraries?
  assert_norm (List.length cms = 0);
  cms
  else
  (
  let cmB, b' = split b 1ul
      
  in
      
  let cm = parseCompression cmB
      
  in
      
  let cms' = parseCompressions b'
      
  in
      
  let cms = cm :: cms'
      
  in
  //library?
  assert_norm (List.length cms = 1 + List.length cms');
  cms)
  

• there a a few cases of double spaces in | h :: t -> let ct = certTypeBytes h in ct @| certificateTypeListBytes t

• why does this force multiple newlines?

  | NewSessionTicket13 _
  | Finished _
  ->
  true
  

Minor/subjective concrete-syntax issues:

• We'd give up on aligning cases, as above (not a big deal)
• Why we have both syntaxes 23z vs 23uy ?
• I prefer function not to be preceded by a linebreak (see above)
• I prefer to elide Tot. An ugly case is val parseCompression : b:lbytes 1 -> Tot ((cm:compression{ compressionBytes cm == b })) also with double parenthesing
• I miss vertical lists for almost all ADTs, even if they fit on a line
• I wish type x = would not force parentheses (a concrete syntax issue)
• Not sure about spaces before/after :, {, and }
• not sure private, unfold etc deserve their own line