62cdb51ed5
Previously, there was a function `opaque fromUTF8Unchecked : ByteArray -> String` which would convert a list of bytes into a string, but as the name implies it does not validate that the string is UTF-8 before doing so and as a result it produces unsound results in the compiler (because the lean model of `String` indirectly asserts UTF-8 validity). This PR replaces that function by ```lean opaque validateUTF8 (a : @& ByteArray) : Bool opaque fromUTF8 (a : @& ByteArray) (h : validateUTF8 a) : String ``` so that while the function is still "unchecked", we have a proof witness that the string is valid. To recover the original, actually unchecked version, use `lcProof` or other unsafe methods to produce the proof witness. Because this was the only `ByteArray -> String` conversion function, it was used in several places in an unsound way (e.g. reading untrusted input from IO and treating it as UTF-8). These have been replaced by `fromUTF8?` or `fromUTF8!` as appropriate. |
||
|---|---|---|
| .. | ||
| bench | ||
| compiler | ||
| elabissues | ||
| ir | ||
| lean | ||
| pkg | ||
| playground | ||
| plugin | ||
| simpperf | ||
| .gitignore | ||
| common.sh | ||
| lean-toolchain | ||