Change close to also raise exn on bad fd input.

fgetc doesn't raise an exception on fd input and just returns NONE.
This is sort of consistent with the way fgetc on Unix will return -1 on a
stream that is in an error state.

compiler/bootstrap/io/catScript.sml

@@ -430,8 +430,16 @@ val close_e =
   ``Let (SOME "_") (Apps [Var (Long "Word8Array" "update");
                           Var (Short "onechar");
                           Lit (IntLit 0);
-                          Var (Short "w8")])
-        (App (FFI 3) [Var (Short "onechar")])`` |> EVAL |> concl |> rand
+                          Var (Short "w8")]) (
+    Let (SOME "u2") (App (FFI 3) [Var (Short "onechar")]) (
+    Let (SOME "okw") (Apps [Var (Long "Word8Array" "sub");
+                            Var (Short "onechar");
+                            Lit (IntLit 0)]) (
+    Let (SOME "ok") (Apps [Var (Short "word_eq1"); Var (Short "okw")]) (
+      If (Var (Short "ok"))
+         (Con NONE [])
+         (Raise (Con (SOME (Short "InvalidFD")) []))))))``
+    |> EVAL |> concl |> rand
 val _ = ml_prog_update (add_Dlet_Fun ``"close"`` ``"w8"`` close_e "close_v")
 
 val _ = ml_prog_update (close_module NONE);
@@ -653,11 +661,24 @@ val close_spec = Q.store_thm(
   xlet `POSTv u.
          &UNIT_TYPE () u * W8ARRAY onechar_loc [fdw] * CHAR_IO_fname * CATFS fs`
   >- (xapp >> simp[onechar_loc_def] >> xsimpl >> simp[LUPDATE_def]) >>
-  simp[CATFS_def] >> xpull >> xffi >> simp[onechar_loc_def] >> xsimpl >>
-  `MEM 3 [0;1;2;3;4n]` by simp[] >> instantiate >> xsimpl >>
-  simp[fs_ffi_next_def, wfFS_DELKEY, closeFD_def, EXISTS_PROD] >>
-  fs[wfFS_def, MEM_MAP, EXISTS_PROD, PULL_EXISTS, validFD_def] >>
-  simp[RO_fs_component_equality] >> metis_tac[])
+  xlet `POSTv u2.
+          &UNIT_TYPE () u2 * W8ARRAY onechar_loc [1w] * CHAR_IO_fname *
+          CATFS (fs with infds updated_by A_DELKEY (w2n fdw))`
+  >- (simp[CATFS_def] >> xpull >> xffi >> simp[onechar_loc_def] >> xsimpl >>
+      `MEM 3 [0;1;2;3;4n]` by simp[] >> instantiate >> xsimpl >>
+      simp[fs_ffi_next_def, wfFS_DELKEY, closeFD_def, EXISTS_PROD] >>
+      `∃p. ALOOKUP fs.infds (w2n fdw) = SOME p`
+        by (fs[validFD_def, MEM_MAP, EXISTS_PROD] >>
+            metis_tac[PAIR,EXISTS_PROD, ALOOKUP_EXISTS_IFF]) >>
+      simp[LUPDATE_def, RO_fs_component_equality]) >>
+  qabbrev_tac `fs' = fs with infds updated_by A_DELKEY (w2n fdw)` >>
+  xlet `POSTv okwv. &WORD (1w:word8) okwv * CHAR_IO * CATFS fs'`
+  >- (simp[CHAR_IO_def, CHAR_IO_char1_def] >> xapp >> simp[onechar_loc_def] >>
+      xsimpl) >>
+  simp[GSYM CHAR_IO_char1_def, GSYM CHAR_IO_def] >>
+  xlet `POSTv okbv. &BOOL T okbv * CHAR_IO * CATFS fs'`
+  >- (xapp >> xsimpl >> qexists_tac `1w` >> simp[]) >>
+  xif >> qexists_tac `T` >> simp[] >> xret >> xsimpl);
 
 (*
 

compiler/bootstrap/io/catfileSystemScript.sml

@@ -94,6 +94,7 @@ val _ = Datatype`
 val wfFS_def = Define`
   wfFS fs =
     ∀fd. fd ∈ FDOM (alist_to_fmap fs.infds) ⇒
+         fd < 255 ∧
          ∃fnm off. ALOOKUP fs.infds fd = SOME (fnm,off) ∧
                    fnm ∈ FDOM (alist_to_fmap fs.files)
 `;
@@ -112,6 +113,7 @@ val openFile_def = Define`
      let fd = nextFD fsys
      in
        do
+          assert (fd < 255) ;
           ALOOKUP fsys.files fnm ;
           return (fd, fsys with infds := (nextFD fsys, (fnm, 0)) :: fsys.infds)
        od
@@ -128,6 +130,7 @@ val wfFS_openFile = Q.store_thm(
   "wfFS_openFile",
   `wfFS fs ⇒ wfFS (openFileFS fnm fs)`,
   simp[openFileFS_def, openFile_def] >>
+  Cases_on `nextFD fs < 255` >> simp[] >>
   Cases_on `ALOOKUP fs.files fnm` >> simp[] >>
   dsimp[wfFS_def, MEM_MAP, EXISTS_PROD, FORALL_PROD] >> rw[] >>
   metis_tac[ALOOKUP_EXISTS_IFF]);
@@ -377,8 +380,10 @@ val fs_ffi_next_def = Define`
              od
       | 3 => do (* close *)
                assert(LENGTH bytes = 1);
-               (_, fs') <- closeFD (w2n (HD bytes)) fs;
-               return (bytes, encode fs')
+               do
+                 (_, fs') <- closeFD (w2n (HD bytes)) fs;
+                 return (LUPDATE 1w 0 bytes, encode fs')
+               od ++ return (LUPDATE 0w 0 bytes, encode fs)
              od
       | 4 => do (* eof check *)
                assert(LENGTH bytes = 1);
@@ -393,13 +398,15 @@ val fs_ffi_next_def = Define`
 
 val closeFD_lemma = Q.store_thm(
   "closeFD_lemma",
-  `fd ∈ FDOM (alist_to_fmap fs.infds) ∧ fd < 256
+  `validFD fd fs ∧ wfFS fs
      ⇒
    fs_ffi_next 3 [n2w fd] (encode fs) =
-     SOME ([n2w fd], encode (fs with infds updated_by A_DELKEY fd))`,
+     SOME ([1w], encode (fs with infds updated_by A_DELKEY fd))`,
   simp[fs_ffi_next_def, decode_encode_FS, closeFD_def, PULL_EXISTS,
-       theorem "RO_fs_component_equality", MEM_MAP, FORALL_PROD,
-       ALOOKUP_EXISTS_IFF] >> metis_tac[]);
+       MEM_MAP, FORALL_PROD, ALOOKUP_EXISTS_IFF, validFD_def, wfFS_def,
+       EXISTS_PROD] >>
+  rpt strip_tac >> res_tac >> simp[LUPDATE_def] >>
+  simp[theorem "RO_fs_component_equality"]);
 
 val write_lemma = Q.store_thm(
   "write_lemma",