mirror of
https://github.com/vercel-labs/scriptc.git
synced 2026-11-05 08:13:06 +08:00
Chris Tate
61c32fbc48
A borrowed Map.get local holds the entry's own reference, so every use must run before anything that can release the entry. Two cases escaped that proof: - A local declared from the borrowed local (`const copy = held`) is a stable alias of it, with no reference of its own. Its reads after a write to the map were not counted as uses. Reference locals declared from the local, at any depth of the statement that declares them, now count as its uses. - A read from a map that no local holds (`fresh().get(k)`) borrowed an entry of a map released at the end of the declaration. The map must now be a local or a field chain rooted at one, whose changes the proof sees as edge changes. Both keep the owned read. Corpus 8181 covers the two cases, and the emission test checks that their reads retain the value.