spec: clarify readFile semantics (#115)

## Summary

Express the semantics of `readFile` using the currently available
meta-language features.

## Details

The previous idea boiled down to treating the result of `readFile` as
fully random (within the bounds of the value's inhabited type). This is
wrong, as it *is* possible to precisely know the value, where afforded
by the context.

The dynamic execution context is extended with a function that maps a
file path and "time" to a UTF-8 character sequence, which is used to
provide the result of a file system read access. The purpose of the
time value is to model the fact that successive reads with the same
path may yield different results, without the program changing anything
itself. Without the time parameter, the definition - due to the meta-
language's side-effect free nature - would define `readFile` as always
yielding the same value for successive calls with the same path.

languages/source.nim

@@ -733,12 +733,6 @@ const lang* = language:
     rule "E-builtin-concat":
       conclusion Call("concat", `array`(*val_1), val_2), `array`(...val_1, val_2)
 
-    rule "E-builtin-readFile":
-      # TODO: implement unknown but bounded values (the `such` clause)
-      #such val_1, `array`(*ch)
-      where val_2, 1 # XXX: temporary hack to make the code valid
-      conclusion Call("readFile", val_1), val_2
-
     rule "E-call-reduce":
       # the call is replaced with the procedure's body (in which all
       # occurrences of the parameters were substituted with a copy of the
@@ -794,6 +788,16 @@ const lang* = language:
       where C_2, C_1 + {"errOutput": `array`(...val_2, ...val_1)}
       conclusion C_1, Call("writeErr", val_1), C_2, TupleCons()
 
+    rule "E-builtin-readFile":
+      # the extra time parameter is used to model the fact that the file
+      # access doesn't always yield the same result, even when the program
+      # does nothing
+      where val_2, C_1.files(val_1, C_1.time)
+      where `array`(*ch), val_2
+      where n_1, C_1.time + 1
+      where C_2, C_1 + {"time": n_1}
+      conclusion C_1, Call("readFile", val_1), C_2, val_2
+
   inductive step(inp, inp, out, out), "$1; $2 \\rightarrow $3; $4":
     rule "E-reduce-pure":
       premise pReducesTo(e_1, e_2)