max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2
lean4-htt/src/runtime
History
Mario Carneiro 62cdb51ed5
feat: UTF-8 string validation (#3958) 
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.
2024-04-20 18:36:37 +00:00
..
alloc.cpp chore: fix more typos in comments 2023-10-08 14:37:34 -07:00
alloc.h chore: reduce src/include/lean 2021-09-07 08:24:54 -07:00
allocprof.cpp chore: reduce src/include/lean 2021-09-07 08:24:54 -07:00
allocprof.h chore: reduce src/include/lean 2021-09-07 08:24:54 -07:00
apply.cpp chore: update script/apply.lean semantics 2022-11-07 19:47:04 -08:00
apply.h fix: split libInit_shared out of libleanshared (#3421) 2024-02-22 19:16:32 +00:00
array_ref.h chore: reduce src/include/lean 2021-09-07 08:24:54 -07:00
buffer.h chore: use size_t at buffer 2021-11-30 16:46:53 -08:00
CMakeLists.txt fix: do not dllexport symbols in core static libraries (#3601) 2024-03-15 11:58:34 +00:00
compact.cpp doc: expand an error message about compacting closures (#3627) 2024-03-07 20:02:23 +00:00
compact.h fix: split libInit_shared out of libleanshared (#3421) 2024-02-22 19:16:32 +00:00
debug.cpp feat: reimplement assert without system headers 2021-11-18 09:42:35 +01:00
debug.h fix: split libInit_shared out of libleanshared (#3421) 2024-02-22 19:16:32 +00:00
exception.cpp chore: reduce src/include/lean 2021-09-07 08:24:54 -07:00
exception.h fix: split libInit_shared out of libleanshared (#3421) 2024-02-22 19:16:32 +00:00
flet.h chore: reduce src/include/lean 2021-09-07 08:24:54 -07:00
hash.cpp chore: replace all hashes by murmurhash 2022-12-01 20:18:14 -08:00
hash.h chore: replace all hashes by murmurhash 2022-12-01 20:18:14 -08:00
init_module.cpp fix: split libInit_shared out of libleanshared (#3421) 2024-02-22 19:16:32 +00:00
init_module.h fix: split libInit_shared out of libleanshared (#3421) 2024-02-22 19:16:32 +00:00
int64.h chore: reduce src/include/lean 2021-09-07 08:24:54 -07:00
interrupt.cpp fix: do not throw C++ heartbeat exceptions in pure functions (#3224) 2024-01-29 20:27:27 +00:00
interrupt.h fix: split libInit_shared out of libleanshared (#3421) 2024-02-22 19:16:32 +00:00
io.cpp feat: isTty (#3930) 2024-04-18 08:50:43 +00:00
io.h fix: split libInit_shared out of libleanshared (#3421) 2024-02-22 19:16:32 +00:00
list_ref.h chore: reduce src/include/lean 2021-09-07 08:24:54 -07:00
load_dynlib.cpp chore: define WIN32_LEAN_AND_MEAN 2022-04-06 09:38:19 +02:00
load_dynlib.h fix: split libInit_shared out of libleanshared (#3421) 2024-02-22 19:16:32 +00:00
memory.cpp chore: put throws in separate function for debugger 2023-01-23 09:27:09 -08:00
memory.h fix: split libInit_shared out of libleanshared (#3421) 2024-02-22 19:16:32 +00:00
mpn.cpp feat: add mpn module 2021-10-25 15:57:19 -07:00
mpn.h feat: add mpn module 2021-10-25 15:57:19 -07:00
mpz.cpp feat: introduce native functions for Int.ediv / Int.emod (#3376) 2024-02-19 15:04:51 +00:00
mpz.h fix: split libInit_shared out of libleanshared (#3421) 2024-02-22 19:16:32 +00:00
mutex.cpp feat: Mutex, Condvar 2022-09-05 08:52:46 -07:00
mutex.h feat: Mutex, Condvar 2022-09-05 08:52:46 -07:00
object.cpp feat: UTF-8 string validation (#3958) 2024-04-20 18:36:37 +00:00
object.h fix: split libInit_shared out of libleanshared (#3421) 2024-02-22 19:16:32 +00:00
object_ref.cpp chore: reduce src/include/lean 2021-09-07 08:24:54 -07:00
object_ref.h fix: split libInit_shared out of libleanshared (#3421) 2024-02-22 19:16:32 +00:00
option_ref.h chore: reduce src/include/lean 2021-09-07 08:24:54 -07:00
optional.h chore: reduce src/include/lean 2021-09-07 08:24:54 -07:00
pair_ref.h chore: reduce src/include/lean 2021-09-07 08:24:54 -07:00
platform.cpp feat: add internal flag lean_has_llvm_backend 2023-11-02 23:21:47 +01:00
platform.h chore: reduce src/include/lean 2021-09-07 08:24:54 -07:00
process.cpp feat: IO.Process.getPID & IO.FS.Mode.writeNew 2023-08-08 16:23:43 -04:00
process.h chore: reduce src/include/lean 2021-09-07 08:24:54 -07:00
sharecommon.cpp refactor: generalize ShareCommon to a typeclass (#1537) 2022-08-29 09:34:38 -07:00
sstream.h chore: reduce src/include/lean 2021-09-07 08:24:54 -07:00
stack_overflow.cpp feat: Web Assembly Build (#2599) 2023-10-04 09:04:20 +02:00
stack_overflow.h chore: reduce src/include/lean 2021-09-07 08:24:54 -07:00
stackinfo.cpp fix: split libInit_shared out of libleanshared (#3421) 2024-02-22 19:16:32 +00:00
stackinfo.h fix: split libInit_shared out of libleanshared (#3421) 2024-02-22 19:16:32 +00:00
string_ref.h chore: reduce src/include/lean 2021-09-07 08:24:54 -07:00
thread.cpp feat: thread initialization for reverse FFI (#3632) 2024-03-07 17:02:47 +00:00
thread.h feat: thread initialization for reverse FFI (#3632) 2024-03-07 17:02:47 +00:00
utf8.cpp feat: UTF-8 string validation (#3958) 2024-04-20 18:36:37 +00:00
utf8.h feat: UTF-8 string validation (#3958) 2024-04-20 18:36:37 +00:00