Disallow dollars in names in safe mode

[odersky]

Dollars are reserved for internal, compiler-generated names. Normally, they are "use at your own risk". For safe mode, we don't want any risk, hence $s are disallowed.

[odersky]

There's an exception in Interactive mode for repl-wrapper names, which do contain $s. This is implemented in the SafeRefs.allow method. We also should include doc snippet names once they are written with dollars.

[bracevac]

Is checking for interactive mode the right call here? This is also used by the REPL, and tacit uses it IIRC. I.e., could this be used by an agent to bypass vital checks. cc @noti0na1

[noti0na1]

I agree. The interactive mode check looks too relaxed for me.

[odersky]

Are Tacit code snippets compiled in interactive mode? Not sure what's different between Tacit and general repl sessions.

[noti0na1]

Yes, the code written by agent is compiled in interactive mode. There is no difference compared to typing in repl. Maybe the check here is ok. I can verify this PR with TACIT later.

[odersky]

@bracevac What changes do you suggest? I believe in order to do anything we'd first have to make sure there is some difference between a Tacit run and a normal repl session. Once we have that, we can do another PR to refine the allow test.

[bracevac]

Maybe we should have an extra mode bit that flags an interactive REPL session with agents?

[odersky]

We don't have an extra mode bit.

[noti0na1]

After thinking about this, I think it's totally fine to access "internal" symbols created by repl; so there is no need to distinguish repl and tacit code.

[bracevac]

But the agent could enter an object that has a dollar in its name, no? The object would have tracked fields with anys, etc, but would not need to marked a capability type.

[noti0na1]

But the agent could enter an object that has a dollar in its name, no? The object would have tracked fields with anys, etc, but would not need to marked a capability type.

In safe mode, we cannot hide a capability, and should not be allowed to create any class/object with a dollar mark.

Then, the only objects available with a dollar mark should be repl objects (by name.isReplWrapperName && ctx.mode.is(Mode.Interactive)), and they are fine to be referred.

[bracevac]

But the agent could enter an object that has a dollar in its name, no? The object would have tracked fields with anys, etc, but would not need to marked a capability type.

In safe mode, we cannot hide a capability, and should not be allowed to create any class/object with a dollar mark.

Then, the only objects available with a dollar mark should be repl objects (by name.isReplWrapperName && ctx.mode.is(Mode.Interactive)), and they are fine to be referred.

Yes or no:

Could the agent right now enter into the REPL something of the form:

package snippet

object Snippet:
  val boom: AtomBomb^ = ...

// secret is some Classified[T] in the env
secret.map(s => Snippet.boom()) // ok,

Right now, anything that is in a package containing snippet and is an object named Snippet is exempt from rules about object formation and tracked fields.