Exception not raised

[Pytheas01]

Hello,
why aren't any exceptions raised in the below code?
Many thanks.

module Ex01a
// print_string
open FStar.IO
// ML string
open FStar.All

type filename = string

let canWrite (f: filename) = 
  match f with
  | "demo/tempfile" -> true
  | _ -> false

let canRead (f: filename) =
  canWrite f 
  || f = "demo/README"

// filename argument f for which canRead f evaluates to true and returning a string
// filename is implemented by system
val read : f:filename{canRead f} -> ML string
let read f = FStar.IO.print_string ("Dummy read of file " ^ f ^ "\n"); f 

// filename argument f for which canWrite f evaluates to true, a string, and returning an unit
val write : f:filename{canWrite f} -> string -> ML unit 
let write f s = FStar.IO.print_string ("Dummy write of string " ^ s ^ "to file " ^ f ^ "\n")

let passwd  : filename = "demo/password"
let readme  : filename = "demo/README"
let tmp     : filename = "demo/tempfile"

exception InvalidRead

val checkedRead : filename -> ML string 
let checkedRead f =  
  if canRead f then read f else raise InvalidRead

val staticChecking : unit -> ML unit 
let staticChecking () = 
  // You can write to demo/tempfile
  let v1 = read tmp in
  // You can write to README
  let v2 = read readme in 
  // You can't write to passwd
  // let v3 = read passwd in
  write tmp "hello!"
  // You can't write to passd
  // write passwd "junk"
  
exception InvalidWrite
val checkedWrite : filename -> string -> ML unit 
let checkedWrite f s = 
  if canWrite f then write f s else raise InvalidWrite

let dynamicChecking () =
  let v1 = checkedRead tmp in
  let v2 = checkedRead readme in
  let v3 = checkedRead passwd in (* this raises exception *)
  checkedWrite tmp "hello!";
  checkedWrite passwd "junk" (* this raises exception *)

[Pytheas01]

According to ChatGPT :

our code does not raise exceptions because:

read and write are protected by static refinement types

Ill-typed calls are rejected at compile time

Refinements are erased at runtime

Only checkedRead / checkedWrite perform dynamic checks and raise exceptions

[mtzguido]

This snippet does raise exceptions when executed, but it typechecks just fine (as intended). To build it and run it, you can add a call to the function in the tail of the file

let _ = dynamicChecking ()

(This makes sure it's actually called, otherwise this file just defines a bunch of functions.)

And then build it and run it like so (the warnings are benign)

$ fstar.exe --codegen OCaml X.fst 
* Warning 272 at X.fst(63,0-63,26):
  - Top-level let-bindings must be total; this term may have effects

Extracted module X
Verified module: X
All verification conditions discharged successfully
$ fstar.exe --ocamlopt X.ml 
File "X.ml", line 23, characters 6-8:
23 |   let v1 = read tmp in let v2 = read readme in write tmp "hello!"
           ^^
Warning 26 [unused-var]: unused variable v1.

File "X.ml", line 23, characters 27-29:
23 |   let v1 = read tmp in let v2 = read readme in write tmp "hello!"
                                ^^
Warning 26 [unused-var]: unused variable v2.

File "X.ml", line 30, characters 6-8:
30 |   let v1 = checkedRead tmp in
           ^^
Warning 26 [unused-var]: unused variable v1.

File "X.ml", line 31, characters 6-8:
31 |   let v2 = checkedRead readme in
           ^^
Warning 26 [unused-var]: unused variable v2.

File "X.ml", line 32, characters 6-8:
32 |   let v3 = checkedRead passwd in
           ^^
Warning 26 [unused-var]: unused variable v3.
$ ./a.out 
Dummy read of file demo/tempfile
Dummy read of file demo/README
Fatal error: exception X.InvalidRead