From discussions with Alex, I realized that our current strategy of storing these sequential keys as {[k1 k2] ...} is incorrect. The reason is that we want to be able to generate proposals for nested sequences of choicemaps without having to copy the whole nested structure in our proposal generators.
So tracing to k2 internal to a trace to k1 should result in the same stored values as tracing to [k1 k2].
And if you do the latter, you should NOT be able to do the former afterward (since the k1 address is already taken). This is a touch subtle, because traces to [k1 k2], [k1 k3] etc at the same level need to succeed, even though k1 is already written to at when [k1 k3] comes along.
From discussions with Alex, I realized that our current strategy of storing these sequential keys as
{[k1 k2] ...}is incorrect. The reason is that we want to be able to generate proposals for nested sequences of choicemaps without having to copy the whole nested structure in our proposal generators.So tracing to
k2internal to a trace tok1should result in the same stored values as tracing to[k1 k2].And if you do the latter, you should NOT be able to do the former afterward (since the
k1address is already taken). This is a touch subtle, because traces to[k1 k2],[k1 k3]etc at the same level need to succeed, even thoughk1is already written to at when[k1 k3]comes along.