Agoric SES, 11 Jan 2023

Previous Meeting Next Meeting

⏯

youtube image

►

From YouTube: SES Meeting: AsyncContext Security Review, Part 2

Description

Mark S. Miller (MarkM) did another deep dive into his investigation of the security properties of AsyncContext and the champion of that proposal, Justin Ridgewell of Vercel, was able to join us. There will be a Part III.

A

Kris “cowbert” kowal: all right., kris, “cowbert”, kowal:, all right., it's the ses meeting. it's january eleventh,, and we're going to talk again to this week about async contexts., and this time we have justin ridgewell, the champion of the proposal.

A

Kris “cowbert”, kowal: and mark has been doing an investigation, and will walk us through it again,, so that some of this will be a a brief recap of last week's meeting. Meeting. and yeah.

A

Kris “cowbert” kowal:, please take it. Welcome, justin,, take it away, mark.

B

Mark s., miller: okay,, so let me.

B

Mark s. miller: actually,, I'm gonna, say a few words before I start projecting.

B

Mark s. miller:, the.

B

Mark s. miller:, so justin mark s. miller:, together with agenda cannis and others have been have a proposal before tc. 39 called async context.

B

Mark s. miller: and mark s. miller: they've mark s. miller:. It's doing something. it's proposing to.

B

Mark s. miller: add to javascript something that.

B

Mark s. miller: would be available for general programming.

B

Mark s., miller: and mark s. miller: cannot be mark s. miller: done at the user level.

B

Mark s. miller: purely within object. an object capability system, you know, hardened.. If, if one started with simply hardened javascript.

B

Mark s. miller: and attempted to do mark s. miller: as in context as a library, as a context as it's proposed.

B

Mark s. miller: could not be done.

B

mark s. miller:, but a mark s. miller:, subset of it mark s. miller:. The synchronous subset of it can be done with perfect fidelity.

B

Mark s. miller: and the full proposal can be understood as a.

B

Mark s. miller: kind of temper,, a weirdly temporal extension.

B

Mark s. miller: of the one that can be done., so that was all quite mysterious.

B

Mark s. miller:, the hypothesis that I want us to examine here.

B

Mark s. miller: is mark s. miller: that mark s. miller:, although this cannot be done with it,, although it cannot be done at the user level.

B

Mark s. miller: within a.

B

Mark s. miller: synchronous,, a normal, synchronous, imperative, o cap language.

B

Mark s. miller: that mark s., miller: and it. and the reason it can't be done is it violates the foundational safety rules.

B

Mark s. miller:, the hypothesis is that it doesn't violate.

B

Mark s. miller:, the the safety purpose of those safety rules.

B

Mark s. miller:, to put it another way.

B

mark s. miller:, the safety rules underlying o caps.

B

Mark s. miller: we've spent decades literally many decades.

B

Mark s. miller:, depending on which community since mid sixteenth,, when o caps are invented.

B

Mark s. miller: exploring and appreciating the safety benefits that come from the foundational rules.

B

Mark s. miller:, so the the question that we're raising is actually quite a square scary question,, which is.

B

Mark s. miller: is there a relaxation?, the particular relaxation being proposed.

B

Mark s. miller: of the foundational.

B

Mark s. miller: that doesn't actually mark s. miller: break the safety purposes that we have found over. the decades are served by the safety rules.

B

Mark s. miller: and there's no simple way to explore this, because it's kind of you have to reason kind of backwards.

B

Mark s. miller:, because it's impossible to just you, know. there,, there's no procedure for reconstructing.

B

Mark s. miller:, all of the safety purposes that that that were derived from the safety rules and see which get broken. all we can do is kind of probe, for which particular things seem to have gotten broken.

B

Mark s. miller: so mark s. miller:, with all of that said, I am going to now project.

B

Mark s. miller:, sorry about the delay, here.

B

Mark s. miller:, okay? well,, I'm going to project.

B

now,, I'm gonna do this.

B

Mark s. miller:, okay?.

B

Mark s. miller:, okay. mark s. miller:, so mark s. miller:. This is the proposal itself.

B

Mark s. miller: and yeah, legitimate cass and justin ridgewell.

B

Mark s. miller:, I.

B

Mark s. miller: are the champions.

B

mark s. miller:. I think that the best summary of the proposal.

B

Mark s. miller: is the mark s. miller:, emulation of it.

B

Mark s. miller: within javascript,, not within hardened javascript,, but within.

B

Mark s. miller:, a full javascript, from which we can mark s. miller:, derive a closest approximation, hardened javascript., so so,, so just in slide. 11.

B

Mark s. miller: shows mark s. miller:, the most of the most of the api right here.

B

Mark s. miller: and then mark s. miller: and this part of the api mark s. miller:, is equivalent to something one could code in hardened javascript without breaking the rules.

B

Mark s. miller: there. so this part of the api by itself is equivalent to.

B

Mark s. miller: to the justin's earlier slide on.

B

Mark s. miller: slide 6, which,, as you can see,, has only changed the name async context to sync context.

B

Mark s. miller:, this one is equivalent to something that's safe.

B

Mark s. miller:, but the thing about asyn context on slide 11.

B

Mark s. miller: is that it is understood to be combined with.

B

Mark s. miller:, this rap function.

B

mark s. miller: and there's 2 levels; ambition, mark s. miller: with regard to rap., oh, and and justin.. Please interrupt me if I'm getting anything wrong, or if there's some crucial detail that needs to be interjected.

B

Mark s. miller:, the so it's understood., and so it should be understood in terms of this.

B

Mark s. miller:, additional rap function, and with the functionality of the rap function.

B

Mark s. miller:, you now have a semantics that cannot.

B

Mark s. miller: decoded in a mark, s. miller: in a declarative, o cap. language, including cannot be coded into.

B

Mark s. miller:, a hardened javascript.

B

Mark s. miller: and there's 2 levels of ambition for the rap function.. What rap does is it captures.

B

Mark s. miller:, a mark s. miller: and a the the the async context, bindings collectively.

B

Mark s. miller:, which are normally associated with being in a particular.

B

Mark s. miller: temporal context, being executing at a particular point in time.

B

Mark s. miller:, it does sort of the equivalent of closure capture of it.. It creates a closure that captures.

B

Mark s. miller:, the mark s. miller:, collective mark s. miller:, async bindings. All all these terms. I will come be coming back and explaining,, but it's easier to just state it and then explain. It.

B

Mark s. miller: captures all of those temporal mark s. miller: bindings collectively mark s. miller:, such that when the resulting closure returned by rap is executed.

B

Mark s. miller:, all those collective mark, s. miller:, bindings associated with that temporal context, or was stored.

B

Mark s. miller: and the 2 levels that condition with rap is rap could be exposed. Directly.

B

Mark s. miller:, which is what they propose on on slide 14.

B

Mark s. miller:, yeah. mark s. miller: and that's the the higher level of ambition., the lower level of ambition.

B

Mark s. miller: is that rap is to be understood only as being encapsulated within.

B

Mark s. miller:, the enhanced behavior of then.

B

Mark s., miller: and other semantics.

B

Mark s. miller:, having do with javascript asynchrony.

B

Mark s. miller: that is, essentially analogous to that, or it could be understood as derived from them., so there's in a in the spec.. There is an internal, then function.

B

Mark s. miller: and then the behavior of the original.

B

mark s. miller: promised,. I prototyped up then, as well as the behavior of the await syntax, or understood.

B

Mark s. miller: as being defined in terms of.

B

Mark s. miller:, the behavior of the internal, then function.

B

mark s. miller:. So in this mark s. miller:, a smaller ambition.

B

Mark s. miller: for being encapsulated,, it would only be projected temporarily forward.

B

Mark s., miller: but, in terms of those things that were defined in terms of the internal, then function.

B

Mark s. miller: okay.

B

mark s. miller:, so now let me mark s. miller:, explain what all of that mark s. miller: means, and to do that.

B

mark s. miller:. I will turn to.

B

Mark s. miller:, the read me on the pr. that I've created.

B

Mark s. miller: for exploring this., so this the pr is.

B

Mark s. miller:, the endo pr 1424.

B

Mark s. miller:, the pr. that I.

B

Mark s. miller:, the version of that that I presented last week.. I've created a snapshot to correspond exactly to the cess meeting recording.

B

Mark s. miller:, which is pr 1,428.

B

Mark s. miller:, but as the living pr. I modified 1424,, which is what I'll be showing today.

B

Mark s. miller:: this is the read me for 1,424,.

B

Mark s. miller: and mark s. miller:, it shows mark s. miller:, a mark s. miller: it.. It breaks down the exploration of the semantics.

B

Mark s. miller: of sync context: mark s. miller: into mark s. miller:. These 4 steps. sorry., 5, steps,, 0,, 1,, 2,, 3, and 4.

B

Mark s. miller:: these are all variations on the sync context.

B

Mark s. miller: and the reason is mark s. miller: that mark s. miller: number 4 mark s. miller: shows the.

B

Mark s. miller: minimal for the the the form of sync context.

B

Mark s. miller: that has the minimal mark s. miller: breakage of object, capability rules that enables.

B

Mark s. miller:, the mark s. miller: explanation of the full async contacts proposal.

B

Mark s. miller: and then so set step. 0. here is essentially.

B

Mark s. miller: justin's mark s. miller: slide 6,, showing the sync context.

B

Mark s. miller:, the but written in proper hardened javascript, with no extraneous mutability.

B

Mark s. miller: slide 5. here is essentially.

B

Mark s. miller: justin's slide 11 and slide 13.. That shows the asyn context with the rap function.

B

Mark s. miller: and then mark s. miller:, slide 6 mark s. miller: is to the analogy of slide. 6 is to slide 5.

B

Mark s. miller: as slide 4 is to slide 0. in other words,. The transition that I make from slide 0 through these other steps to get to slide 4.

B

Mark s. miller:, I then apply that transformation to slide, 5 to get to slide 6,.

B

Mark s. miller: and the result is that we can have the.

B

Mark s. miller: narrowest conversation mark s. miller: about the way in which.

B

Mark s. miller:, the full proposal mark s. miller: breaks the object. capability rules by.

B

Mark s. miller:, manipulating mark s. miller:, hidden,, mutable state.

B

Mark s. miller: okay. mark s. miller:, so I think at that point the going through the sequence. here is the best way to proceed.

B

Mark s. miller: and some of this will be.

B

Mark s. miller: a bit redundant with mark s. miller:. What we covered last week, so go through the redundant part quickly.. But it is fresh code because I rephrase the code to be.

B

Mark s. miller:, easier to understand.

B

Mark s. miller:, okay. mark s. miller:, so mark s. miller:. This is essentially mark s., miller:, justin's slide 6.

B

Mark s. miller:, but written in proper hardened javascript.

B

Mark s. miller: with no extraneous mutability., so no extraneous mutability.

B

Mark s. miller: is by hardening mark s. miller:, the sync context class,, which also,, which freezes the class and then freezes everything. That's that's reachable by property and prototype perversal.

B

Mark s. miller:, starting with the class, which means it, freezes the class,. It freezes the prototype.

B

Mark s. miller: and it freezes all of the inherited methods.

B

Mark s. miller: and in heart and javascript all the primordials are also.

B

Mark s. miller:, already implicitly frozen.

B

Mark s. miller:- and this is all necessary- mark s. miller:- to understand this.

B

Mark s. miller: code as being mark s. miller:, a shim of what of what is being proposed as a new primordial.. So in the proposal sync context.

B

Mark s. miller: well, really,, as in context,, is being proposed as a new primordial.

B

Mark s. miller: in hardened javascript., this would be considered.. You know we're we're we're considering.

B

Mark s. miller:, we would, you know,. If, if it were to go forward,, we would.

B

Mark s. miller: add it to hardened javascript as a.

B

Mark s. miller: white listed, and therefore considered to be safe and powerless, primordial.

B

Mark s. miller: and as a primordial and hardened javascript.

B

Mark s. miller:, it would be, in fact, hardened.

B

mark s. miller:. You would have no mark s. miller:, extraneous mutable state mark s. miller:, notice,, though, that it captures this. Let storage variable,, which is where.

B

Mark s. miller:, the source of all of the interesting angst about examining this proposal.

B

Mark s. miller:, but so that's where the the the mark s. miller:, a fundamental mutability, is that we're going to be worried. About.

B

Mark s. miller:, but also I'm also hard, and added this constructor here to harden the instance.

B

Mark s. miller: so that we're getting rid of the extraneous mutability of the instance. there's no own properties of the instance.. So this isn't changing just in semantics. At all.

B

Mark s. miller:, it's just doing it the way it it, it would be.

B

Mark s. miller: done,, so that there is mark s. miller:, no additional mutability, that that confuses the issue. okay, now.

B

Mark s. miller:, what is this?

B

mark s. miller: to understand what this is doing.

B

Mark s. miller:, I'm going to take us mark s. miller:, first to mark s. miller:, the.

B

Mark s. miller: yeah,, the.

B

Mark s. miller:, yes. mark s. miller:, so I' what?, I'm what I'm doing this week. that's different than last week.

B

Mark s. miller:, is. mark s. miller:, I I did an experiment., which is what you're seeing here,, which is.

B

Mark s. miller: to mark s. miller: contain the complexity of the exploration.

B

Mark s. miller: is,, I mark s. miller: cried,, rephrasing it from using class.

B

Mark s. miller:, notation to using objects, is closure. Notation.

B

Mark s. miller: that I found that that really simplified the conversation tremendously,, but it means that it has less fidelity.

B

Mark s. miller: as a shame. mark s. miller:, the proposal was proposing it as a class,, the shimming it as a class.

B

Mark s. miller: so rephrasing the proposal in terms of objects, disclosures.

B

Mark s. miller: has some mark s. miller: differences from what's being proposed,, but no essential, differences.

B

Mark s. miller:, it just makes the the it may, it just.

B

Mark s. miller: makes the discussion of deviation from object capabilities.

B

Mark s. miller:, more constrained., so the differences are that, rather than a class,, we have a making function.

B

Mark s. miller:, there is no prototype.. The methods are not inherited from the prototype.

B

Mark s. miller:, rather, the methods are.

B

Mark s. miller:, our own properties of the async context, instance.

B

Mark s. miller:, but it's still the case that it breaks the rules, because there's still a.

B

Mark s. miller:, mutable variable,, this outer let variable, they close over.

B

Mark s. miller:, which would not be allowed if the maker were to be admitted as a power powerless.

B

Mark s. miller:, primary.

B

Mark s., miller: and but then to understand what this is doing,. Let's now go to my next slide.

B

Mark s. miller:, which is slide 2,, mark s. miller:, which is mark s. miller:, a shallow binding implementation of the same semantics. okay, now now,. I will explain about.

B

Mark s. miller:, with this in front of us., I will now explain about.

B

Mark s. miller:, dynamic, scoping., mark s. miller:, fluid,, scoping., mark s. miller:, shallow binding., mark s. miller: and then with my next slide, deep, blind.

B

Mark s. miller:, so these are all concepts.

B

Mark s. miller: from the historical mark, s. miller:, literature on.

B

Mark s. miller: lambda languages in particular. list, one you actually instead of saying landline,, which say, lispling the the the the history of list languages.

B

Mark s. miller:, so this mark s. miller: was understood as from the beginning, as being very close to them to calculus.

B

Mark s. miller:, but the original list, mark s. miller: john mccarthy's list in the 1,900 fiftys.

B

Mark s. miller: deviated from lamb to calculus by using dynamic scoping rather than fluid than lexical. scoping.

B

Mark s. miller: in mark s., miller:, dynamic, scoping.

B

mark s. miller:, a mark s. miller: variable mark s. miller: use mark s. miller: is mark s. miller: looked up. mark s. miller:, you know, to find the corresponding definition.. You know. What's the value of the variable?, you have to figure out. What's the binding occurrence.

B

Mark s. miller: that determines the value of the variable.

B

mark, s. miller: and mark s. miller: in mark s. miller:, the original list, with dynamic scoping,. You found the binding occurrence.

B

Mark s. miller: by literally looking backwards, stack, frame by stack frame.

B

Mark s. miller:, until you found a stack frame that defined.

B

Mark s. miller:, the binding for that variable, name.

B

Mark s. miller: and mark s. miller:, that's obvious. You know to modern, modern eyeballs.. That's obviously.

B

Mark s., miller:, non-modular and unstructured,, and in fact,, creates all of the problems that you would expect.. It creates.

B

Mark s. miller:, but they went surprisingly far with that.

B

Mark s. miller: and mark s. miller:, then in mark s. miller: in the early seventys there was a rediscovery through actors.

B

Mark s. miller: of the power of mark s. miller:, lexical, scoping and lambda calculus that the lisp languages were missing, and that led to the.

B

Mark s. miller: creation of the scheme language,, which was the the.

B

Mark s. miller:, which was was the next version of lisp,, and then that.

B

Mark s. miller: and scheme was a purely lexically scope. language very,, very close to an object. capability. Language is shown by the object capability schemes.

B

Mark s. miller: that were then later drive from it.

B

Mark s. miller: and essentially all modern languages are descendant from.

B

Mark s. miller:, our our lexically scope, languages, and if they're in the list. tradition, you're very much descendant from that rediscovery and scheme.

B

Mark s. miller: so mark s. miller: the to understand the difference between lexical scoping and dynamic scoping.. You can think of both of them.

B

Mark s. miller:, as mark s. miller:, defining intervals mark s. miller:, over which a variable is bound to a value.

B

Mark s. miller:, where those intervals can be nested.

B

Mark s. miller:, so in lexical scoping, mark s. miller:, the intervals are.

B

mark s. miller:, let's say, defined by open curly brackets in javascript.

B

Mark s. miller:, so the open, curly bracket, close curly bracket, defining a scope.

B

Mark s. miller:, where the scope contains the variable definition.

B

Mark s. miller: that variable definition mark s. miller: is mark s. miller:. The mark s. miller: I mark s. miller: is the one that determines the meaning of a use occurrence of the same variable. Name.

B

Mark s. miller:, within that interval of text between the open curly bracket and the call close call back black bracket., except for scopes in which that variable definition is shadowed.

B

Mark s. miller:, which are nested mark s., miller:, open., curly brackets close., call me bracket intervals.

B

Mark s. miller:, they contain, and a different definition of the same variable.

B

Mark s. miller:, the dynamic scoping can be understood.

B

Mark s. miller: has mark s., miller: also, in terms of nested intervals, doing shadowing., but now the nested intervals,, instead of being textual.

B

Mark s. miller:, our temporal.

B

mark s. miller:, so it begins with.

B

Mark s. miller:, a a function call creating a stack frame.

B

Mark s. miller: that contains a definition of a given variable.

B

Mark s. miller:, it ends when that function, call returns.

B

Mark s. miller: and while that function call is on the stack.

B

Mark s. miller:, it is shadowed by mark s. miller:. Another nested function. call mark s. miller: that defines a binding for the same variable. Name.

B

Mark s. miller:, so it's it's so the the nested intervals are associated with name.

B

Mark s. miller: over a given.

B

Mark s. miller:, a temporal interval. mark s. miller:, whereas lexical scoping associ, with name over a given textual interval.

B

Mark s. miller: and common lisp, by the way, is mostly lexically scoped,, but preserves dynamic scoping in the original lisp sense,, which is associated.

B

Mark s. miller:, with the with the variable name,, where there's no special privilege in being able to mention the variable name.

B

Mark s. miller: louis scoping mark s. miller:, was. mark s. miller:, an invention by scheme, programmers.

B

Mark s. miller: to recover some of the power that they associated with.

B

Mark s. miller:, dynamic scoping., but to do that within the rules of lexical scoping.

B

Mark s. miller: in a sequential, imperative language and scheme is scheme, unlike actors as a sequential, imperative language.

B

Mark s. miller:, now.

B

Mark s. miller:, and this this slide over here explains how they did that. so now.

B

Mark s. miller: in this slide over here. by the way,. This one does not break any o cap rules.. This is perfectly fine.

B

Mark s. miller: hardened javascript code., it's perfectly fine.

B

Mark s. miller: pardon javascript code for mark s. miller: being a shim for a new primordial,, which is therefore needs to be.

B

Mark s. miller:, immutable and powerless.

B

Mark s. miller: and the maker here is top level and hardened.

B

Mark s. miller: and therefore does not close over any mutable state.

B

Mark s. miller:, it makes instances, this return of hardened, open curly of these 2 methods.

B

Mark s. miller: and the instances are mutable. they close over this encapsulated state, variable, and they mutate it.

B

Mark s. miller: and mark s. miller: the way to think about mark s. miller:. What this is accomplishing is the instance.

B

Mark s. miller: is now mark s. miller:, a first-class object. from an o cap perspective. you either have access to the object, or you, don't.

B

Mark s. miller: and you only have access to an instance if you're granted, it.

B

Mark s. miller: because the maker is is global,, is ambient.. Anybody can make new instances, that's considered to be not.

B

Mark s. miller:, something that's that we intend to deny.. We intend to enable anybody to make new instances which is unthreatening, because anybody could have written this code. Anyway.

B

Mark s. miller:, but the instances are genuine capabilities that enable communication through this mutable state,, which is not surprising because mutable, the instances themselves.

B

Mark s. miller: or mutable. mark s. miller:, hmm. mark s. miller:, the we're going to to say that the instance represents a fluid variable,. So the the difference between dynamic scoping and fluid scoping.

B

Mark s. miller: is mark s. miller:, the and now the analogy to a dynamic variable is now a fluid variable where the fluid variable is no longer designated by a textual name,. It's designated by a first class object, or designated by the capability.

B

Mark s. miller: that that that designates this first class object.

B

Mark s. miller: and now mark s. miller:. This object has 2 methods:. The the particular api here is derived from from the as in context proposal, but it's,, but it's understood as analogous to any fluid scoping system.

B

Mark s. miller:, the 2 methods are run mark s. miller:, where you give a new binding mark s. miller: for the fluid variable. Where that new binding.

B

Mark s. miller: should be in temporal scope.

B

Mark s. miller: during the call to the call back. so.

B

Mark s. miller: cb is a call back,, which is called over here.

B

Mark s. miller:, the arguments are just for convenience, here.

B

Mark s. miller: it to be spread out over there.

B

Mark s. miller: there's nothing fundamental about that.

B

Mark s. miller:, but mark s. miller:, what's going on here, is that mark s. miller:. The implementation is remembering.

B

Mark s. miller:, the mark s. miller:, the the binding of this hidden state variable,, the binding of it to some value.

B

Mark s. miller:, before the call back happens.

B

mark s. miller:. It's then mark s. miller:, assigning the this value to the state variable.

B

Mark s. miller:, just during the call to the call back, and then, when the call back finishes, it's restoring.

B

Mark s. miller:, whatever the previous value of the state. variable, is.

B

Mark s. miller:, so so the mark s. miller:, so this get is just sort of directly reflects our notion of the temporal nesting.

B

Mark s. miller: and mark s. miller:, the and and the.

B

Mark s. miller: to read the current binding to do the equivalent of reading of of the way, a use value of the variable reads. The current binding of the variable.

B

Mark s. miller: there is to get method mark s., miller:, one., mark s. miller:, the fluid mark s. miller:, the the the fluid variable instance object.

B

Mark s. miller:, that simply reads the state. now,. When we talk about variables,, we have in javascript wet variables and constant variables.

B

Mark s. miller: and which are lexical concepts,. I don't.

B

Mark s. miller:, in both cases the and the.

B

Mark s. miller:, the association mark s. miller:, of a use occurrence to the binding to to the to the defining occurrence.

B

Mark s. miller: is lexical, but wet variables.

B

mark s. miller:, so support this additional concept of assignment.

B

Mark s. miller: we,, I should make very clear here.

B

mark s. miller:, and that was also the case, by the way, that some of the scheme implementations of fluid scoping.. I should make very clear here that over here we're doing the temporal analogy to cost.

B

Mark s. miller:, not the temporal analogy to let.

B

Mark s. miller:, it's only on spawning the nested temporal interval that we can associate a new value.

B

Mark s. miller: to the mark s. miller: to the first class object representing the fluid variable.

B

Mark s. miller: and during that we can only read.

B

Mark s. miller:, the corresponding binding. there's, no there's nothing analogous to assignment during that interval.

B

Mark s. miller: and mark s. miller:, so first of all,, before I go. so I'm. I'm. next, going to explain about why this is represents shallow binding rather than deep, binding as an implementation technique.. But before I do that.

B

Mark s. miller:, how clear was what I said so far.

B

Mark s. miller: and any questions, or any corrections, or any important.

B

Mark s. miller:, additional explanation that I omit.

B

C

Caridy: yes, so mark,, I'm still fossy about the difference between the one that you have in the screen on the one that you have before.

C

Caridy: or the the left was outside.

C

Mark s. miller:, right.

B

Mark s. miller: okay,, so so good.. So this slide slide, number one.

B

Mark s. miller: and slide number 2 mark s. miller: implement exactly the same semantics.

B

Mark s. miller:, but they implement the semantics in different ways.

B

Mark s. miller: and in particular, as a proposed, powerless primordial.

B

Mark s. miller:, this implementation violates.

B

Mark s. miller:, the rules for a primordial, for an object. capability, language.. The idea is that make.

B

Mark s. miller:, sync context: mark s. miller: would be. mark s. miller: pervasively shared among things that should not be able to talk to each other.

B

Mark s. miller:, but even after hardening it.

B

mark s. miller:, the the primordial object,, the maker.

B

Mark s. miller: has access to this mutable variable,, which it in fact mutates so to make very clear.

B

Mark s. miller:, the the the the in which this violates the rules.

B

Mark s. miller:, I see. is peter here today.

B

Mark s. miller:, nobody from audible, is here today.. I can see mark s. miller:, so peter was here last week.

B

mark s. miller: and I verified with him mark s. miller: that mark s. miller:. What I expected,, which is mark s. miller:, this code., make a sync context, passes his purity checker.

B

Mark s. miller:, make is in contacts, has no hidden mutability.

B

Mark s. miller:, so after hardening, there's no mutability left. it is, it is pure.

B

Mark s. miller:, the instances would fail a purity checker because they captured the state variable., but the state variable is only per instance.

B

Mark s. miller:, multiple purity checker applied to make,, as in context, over here on slide,, one.

B

Mark s. miller: fails the purity shutter.

B

Mark s. miller: and it fails the purity checker.

B

mark s. miller: because mark s. miller:, the the this function has captured this mutable state.

B

Mark s., miller: and mutable state, is it's a set.. It's it's.. You know we it.. This code would not work if we change that led to a cost.

B

Mark s., miller: and furthermore,, the value of that mutable state is itself something mutable.. This map,, where the map itself also has a central mutability that will be coming back. To.

B

Mark s. miller:, so this actually fails the the purity checker on 2 grounds.

B

Mark s. miller:, it fails because this is let variable, that's actually assigned to.

B

Mark s. miller:, but even if this were a const,, the value of the variable is itself.

B

Mark s. miller:, something that is essentially mutable.

B

Mark s. miller: and therefore sync context.

B

Mark s. miller:, because that mutable value is reachable from it.

B

Mark s. miller: sitting, the this maker object is also.

B

Mark s. miller:, not pure mark s. miller: and therefore by that check, would normally be disallowed.

B

Mark s. miller: has a primordial mark s. miller: and mark s. miller: in audible. in montreal's case. We can make this very, very concrete with regard to the issue of what can go into wrong.

B

Mark s. miller: over here mark s. miller:, may make you sync context.

B

Mark s. miller: can just go into wrong..

B

Mark s. miller: in the model. Implementation for embedded can just go into rom, with no extra book bookkeeping to simulate.

B

Mark s. miller: to emulate mutability.

B

mark s. miller:, whereas mark s. miller: this one with this implementation of make,, as in context, on my my slide, one.

B

Mark s. miller: could not mark s. miller: go into wrong without some magical extra bookkeeping.

C

Caridy: my question is,: what is the different between the 2 of them in functionality.

C

Mark s. miller:, the functionality? there's 0 difference., and that's that's really the point that I'm making.

B

Mark s. miller: is that the observable semantics is identical.

B

Mark s. miller: and therefore mark s. miller:, this slide is actually safe.

B

Mark s. miller: in terms of the semantics. it presents, and because this one is safe. in fact,. Even this slide is safe.

B

Mark s. miller:, which is justin's, slide 6.

B

Mark s. miller:, so justin's slide 6 mark s. miller:, even though it's implemented, you know, through techniques that break the o cap rules, the semantics,, the observable semantics that it proposes is safe. and therefore,. If this was the extent of what justin was proposing.

B

Mark s. miller:, there would be no o cap safety problem in accepting it into javascript.

C

Caridy: so so maybe the the question is really for for justin on line 19.

C

Justin ridgewell:, that's the one that confuse me if you're creating my and your person storage.. So the reason the code is written. This way is because it will build into async context,, which is the actual proposal., I'm using sync contacts in order to build an understanding and then transforming that into async context.

D

Justin ridgewell: that actually has the behavior. That's modeled. The code between sync context and async context is 100%. the same minus the class name binding the the the class name is changed., so the.

D

Justin ridgewell: map, clone that happens on 19, and the set that happens on 20 is in this code, because it has to happen in async context,. In order for ascent context, to behave. Correctly.

D

Justin ridgewell:, but in sync contacts the reason it.

D

Justin ridgewell: isn't necessary is because justin ridgewell: it only ever accesses its own key online 20 and online 30.

D

Justin ridgewell:, although it has access to the full map,, it only calls that mac, with this.

D

Justin ridgewell: value,, which is the asyn context or sorry, the sync context instance.. So you only access your own key in a map,, regardless of what that current map value is.

D

Caridy: okay. okay, mark,. Do you have the same thing for async?.

D

Mark s. miller: yes, you'll build into it later in this. yeah.. So let me just go back to my read me: a second. explain the entire expository sequence.

B

Kris “cowbert” kowal: and also we're down to 15 min,, which is really.

B

Mark s. miller:, okay.

B

mark s. miller:, so once again it's it's more important to get this right than to get this fast.

B

Mark s. miller: and so I'm going to.

B

Mark s. miller:, I'm gonna, I'm gonna hurry, through.

B

Mark s. miller:, I'm going to complete the current questions, mark s. miller: and explain as much more as I can explain.. But we're clearly going to need to continue this and later.

B

Justin ridgewell: later conversations., I think we might be able to skip directly to 4, and then 5 and 6, and skip 2 and 3 here..

B

Mark s. miller: I'll, try, that. mark s. miller: okay,, so mark s., miller:, the so the basic idea here.

B

Mark s. miller: is that mark s. miller: 6 is to 5 mark s. miller: as 4 is to 0.

B

Mark s. miller:, so I start with same context, which is a rule-breaking implementation of something that's actually safe..

B

Mark s. miller:, I then derive from it, for.

B

Mark s. miller:, which. mark s. miller: and still rule breaking, but is minimally rule-breaking in a way that still enables.

B

Mark s. miller:, the full proposal.

B

mark, s. miller: and then using the rule breaking of number 4.. I then drive number 6,.

B

Mark s. miller:, which leverages minimal breaking of 4 in order to.

B

Mark s. miller: give us the maximal ability to reason about what is potentially unsafe on the full proposal.

B

Mark s. miller: okay. mark s. miller:, so now I will mark s. miller: jump forward to 4.

B

Mark s. miller: so, for mark s. miller: still has mark s. miller: hey? mark s. miller:, mutable top-level, variable.

B

Mark s. miller:, which is actually mutated.

B

Mark s. miller:, so over here is an actual mutation of the mutable top-level variable.

B

Mark s. miller:, but mark s. miller:. It only has mark s. miller:, one mark s. miller: source of rule breaking mutability,, which is the let here, the the mutability,. The assignability of the top level, variable itself.

B

Mark s. miller:, it does not have the other.

B

Mark s. miller:, distracting mutability that we saw on earlier slides.

B

Mark s. miller:, which is the values bound to this mutable variable.. Each of those values are themselves.

B

Mark s. miller:, transitively, immutable and harmless.

B

Mark s. miller: so., so let's take a look at what those.

B

Mark s. miller: those values are., but to to do that, we will first take a look at where.

B

Mark s. miller:, the so the value of of dunker bar get.

B

Mark s. miller: is a function from a map.

B

Mark s. miller: to a value.

B

mark s. miller:, so.

B

Mark s. miller:, so where this is used, is in the get method,, which is an instance method.

B

Mark s. miller: of a mark s., miller: oh,, this should have. I'm sorry. This should have been. make async context.

B

Mark s. miller:, no,, no,, no, no!. This is slide, 4. I'm:, sorry. This is correct.

B

Mark s. miller:, this is still make sync context,, which is not.

B

Mark s. miller:, which is still implementing mark s. miller:, a non mark s. miller:, implementing a safe semantics by rule breaking meetings.

B

Mark s. miller: so mark s. miller:, so the so when we allocate an instance, we that we in allocate this encapsulated week, map.

B

Mark s. miller: and then mark s. miller:, the get instance method mark s. miller: uses whatever the current binding is of the global done of the encapsulated.

B

Mark s. miller: top level under get mark s. miller: variable mark s. miller:, using the encapsulated.

B

Mark s. miller: transpose map.

B

Mark s. miller:- that's that's specific to this fluid, variable specific to this instance.

B

Mark s. miller: of mark s. miller: of sync contacts.

B

Mark s. miller: and.

B

Mark s. miller:, so what we're doing here mark s. miller: is mark s. miller:, we're mark s., miller: saving, mark s. miller:, the previous.

B

mark s. miller:. So so each bind, each value associated with thunderbar get.

B

Mark s. miller: is a. It represents a different temporal interval.

B

Mark s. miller:, so we're we're stacking up.

B

Mark s. miller:, the previous temporal interval into this prev variable.

B

Mark s. miller:, we then create mark s. miller:, a frozen mark s. miller:, you empty, immutable object.

B

Mark s. miller:, sorry. yeah., just a frozen frozen, empty object,, which therefore is powerless and immutable.

B

Mark s. miller:, but has a unique, unfortunate identity,, which is key.

B

Mark s., miller: and that's corresponds because we're creating that.

B

Mark s. miller: that we're not creating that out here., so it doesn't.

B

Mark s. miller: represent. key does not represent the this,. The sync context, instance.

B

Mark s. miller:, he represents the call to run, doing it per call to run.

B

Mark s. miller:, so this so the key is specific.

B

Mark s. miller: to a given of fluid variable over a given temporal.

B

Mark s. miller: interval. in other words,, he represents a particular binding.

B

Mark s. miller: of the fluid variable instance.

B

mark s. miller:, but it does not contain the binding.. It is an immutable,, powerless object,, whose identity represents the blinding.

B

Mark s. miller:, but then, to actually get the bound value.

B

Mark s. miller:, the key is used to associate mark s. miller: the bound value in the transpose map with the key.

B

Mark s. miller:, the transpose map is specific to the fluid variable.

B

Mark s. miller:, the you know,, the fluid variable,, which is the same context, instance.

B

Mark s. miller:, so the value is still specific. to mark s. miller:. This is bound to this.

B

Mark s. miller: fluid, variable, as of this temporal interval.,.

B

Mark s. miller: and then mark s. miller:. Having created that binding,, then we create.

B

Mark s. miller:, this binding of mark s. miller:, the global mark s. miller:, get variable mark s. miller: that mark s. miller: that maps from any map.

B

Mark s. miller:, 2 mark s. miller:, a mark s. miller:, a deep bound lookup,, which is a look up. That's going to walk back through a linked list of.

B

Mark s. miller:, these get functions. so basically.

B

Mark s. miller:, you can see by inspection that the closure here.

B

Mark s. miller:, the closure here mark s. miller:, is capturing mark s. miller:. He mark s. miller: and capturing that's the the the very,, the the lexical variables captured by the closure.

B

Mark s. miller: so to verify that the closure mark s. miller: is pure., mark s. miller:. We verify that he is itself a pure object.. He would pass.

B

Mark s. miller:, models., purity, checker., mark s. miller: crev is the previous,, but is the value of the previous binding of.

B

Mark s., miller: and and and therefore by induction, it is pure.

B

Mark s. miller: and therefore mark s. miller:. This closure has captured no mutability, and by hardening the closure, the new binding of get is pure.

B

Mark s. miller:, so there's so., so that's pure., mark s., miller: and then. mark s. miller:. Having done that, binding, mark s. miller: to the global get., we now call back the the the call, the call back.

B

Mark s. miller: and the key thing about calling the call back in this context.

B

Mark s. miller: is mark s. miller:, that of that that projects this temporal interval.

B

Mark s. miller: across any other use.

B

Mark s. miller: of mark s. miller: fluid scoping to further rebind the global get variable.

B

Mark s. miller: and then,, when we exit the temporal interval, we restore the previous context.

B

Mark s. miller: so now mark s. miller:, so I mark s. miller:. This code mark s. miller:, which is justin's slide mark s. miller:, 11 and 13.

B

mark s. miller:. The this mark s. miller: part over here mark s. miller: of justin's slide 11 mark s. miller: is identical to justin's slide 6,, except for name, change from sync context to asyn context.

B

Mark s. miller:, but then just in slide 13 mark s. miller: adds this rep function.

B

Mark s. miller:, which is mark s. miller:, makes use of the shared mark s. miller: top-level mutable variable storage.

B

Mark s. miller:, so so so so turning that into.

B

Mark s. miller:, the mark s. miller:, corresponding rule breaking.

B

Mark s. miller: that has minimal distracting mutability, so that we can reason most narrowly about the danger.

B

Mark s. miller:, this code up here make asyn context.

B

Mark s. miller: is equivalent to my slide, for,, except for the name change.

B

Mark s. miller:, but the what the rap function does.

B

Mark s. miller: is mark s. miller:, yet mark s. miller: when rap is called mark s. miller: during the call.

B

Mark s. miller: it mark s. miller: captures mark s. miller:, the mark s. miller: current mark s. miller: value of the shared mutable get variable. in other words,. It captures.

B

Mark s. miller:, the temporal context mark s. miller:, that is giving a binding to collectively.

B

Mark s. miller:, all of mark s. miller:, the fluid variables that have ever been created using this maker.

B

Mark s. miller: and the maker is assumed to be pervasively available., so you can say that that this capture, variable is capturing the.

B

Mark s. miller: well collectively, all of the the fluid bindings associated with the current instance in time,. The current.

B

Mark s. miller: temporal mark s. miller: context.

B

Mark s. miller: associated with now mark s., miller: and then,, when the and and then it's going to return. a hardened form of that closure.

B

Mark s. miller: that closure,, when called, will will.

B

Mark s. miller: stack mark s. miller:, the mark s. miller: temporal mark s. miller: contacts., the the the the stacked.

B

Mark s. miller:, the collective binding of all of the fluid variables.

B

Mark s. miller: at the point where the closure is called.

B

Mark s. miller:, it will then mark s. miller: re.. It will then restore mark s. miller:. The collective bindings associated with the moment.

B

Mark s. miller:, when rap was called.

B

mark s. miller:. It will then call the the the the call back called the function. That's being wrapped.

B

Mark s. miller:, with the restored captured.

B

Mark s. miller:, scope. mark s. miller: and then it will. and then, when, when this function, completes,, whether once again,, whether it returns or or throws, when it completes.

B

Mark s. miller:, the previous mark, s. miller:, binding.

B

Mark s. miller: before the rapt functions called, is restored, so that nobody outside that call sees it.

B

Mark s. miller: and mark s. miller:, so for. so first of all, before taking questions,. Let me verify with justin.

B

Mark s. miller: that I gave an accurate explanation.

B

Justin ridgewell: yes. mark s. miller:, okay.

B

Mark s. miller: and mark s. miller:, the mark s. miller: so., so the so the so the thing that's really intriguing about this from a safety perspective.

B

Mark s. miller: is that mark s. miller:, the mark s. miller:. There are mark s. miller: object, capability, languages which are not built on a sequential imperative. Base.

B

Mark s. miller:, there are the actor,, the fine-grained actor, languages.

B

Mark s. miller:, which have,, which which in which there's only a synchronous, message passing.

B

Mark s. miller:, in which sync context was essentially impossible. to write.

B

Mark s. miller: sync context became possible. to write.

B

Mark s. miller: when. mark s. miller: in specifically, when mark s. miller:, o caps is combined with.

B

Mark s. miller:, the temporal logic mark s. miller: of sequential imperative, programming.

B

Mark s. miller: javascript,, as well as hardened javascript, as well as hardened javascript, with endo.

B

Mark s. miller: is mark s. miller: combines o caps with something more than just sequential imperative. Programming.

B

Mark s. miller:, it combines o caps mark s. miller:. It also extends o caps over.

B

Mark s. miller:, asynchronous control. flow mark s. miller: in javascript, via then.

B

mark s. miller: and in hardened javascript, with endo via.

B

Mark s. miller: eventual send.

B

Mark s. miller:, which and over eventual sin.

B

Mark s. miller: to other vats, mark s. miller:, all of which are additional.

B

Mark s. miller: temporal extensions, which cannot be coded at the user level,.

B

Mark s. miller: in the way mark s. miller: they're available on hard and javascript, and and.

B

Mark s. miller: in particular, because then could not be coded.

B

Mark s. miller:, starting just from a sequential imperative, language, because then is primordial, but has access to the job. Queue.

B

Mark s. miller:, which is also mark s. miller:, top level. mark s. miller:, mutable state.. If we modeled the way in which he then has access to the job, queue.

B

Mark s. miller:, if we model that in javascript we would find the then the then method is not pure by a purity checker.

B

Mark s. miller: and the only reason it's pure by multiple purity checkers,, because it understands, then as being a primitive part of javascript..

B

Mark s. miller:, this is mark s. miller:, also mark s., miller: changing.. If, if this were accepted into an o cap, language, and.

B

Mark s. miller: then,, in order to judge that the results to be an o cap language,, we would have to judge the result to be an o cap language.

B

Mark s. miller:, under a different mark, s. miller:, notion of what temporal context is under sort of a different rearrangement.

B

Mark s. miller: of the association of time and binding.

B

Mark s. miller: did all of that?. Did all of that make sense.

C

Caridy: sorrow?

C

mark s. miller: okay. mark s. miller: go ahead., caridy:, yeah, I'm. still.

C

Caridy: try to get my head around it.

C

Caridy:, so I have 2 main.

C

caridy:. Is that right? caridy:? I need to explore. caridy: the first one is why caridy: line number 2 is okay.

C

Caridy:, assuming that obviously line 13 is doing some more advance.. This is more power there and then.. The comparing this to.

C

Caridy: the audio implementation, was using some.

C

Caridy:, mac or or something that you were able to use to the storage one. so.

C

Caridy:, so that's that's one thing that I still done fully understand.. What's the difference between the 2 of them., I I think I get it by that to begin into one. what is this? more difficult? and the the second part is.

C

Caridy:, what you were mentioned: like. okay.

C

Caridy: so caridy:, what exactly is different in terms of.

C

Caridy: okay? or labeling javascript, as okay.

C

Caridy:, if we accept the stuff., I I I didn't quite get.

B

Mark s. miller: yeah., so the.

B

Mark s. miller:, so so the let me answer the the so it's 11 o'clock.. I will try to squeeze in an answer to the first question, and the second question.

B

Mark s. miller: truly, is the the the big, open-ended one that that could very that we should about the the first one,, though I'm more worried about the second one.

C

Mark s., miller: and caridy: be more specific. mark the.

C

Caridy:, the caridy:- I still don't get my head around.

C

Caridy:, the caridy:, the the problem with this coping that you're talking about in terms of.

C

Caridy: okay,: what is it that it's changing at the language level.

C

Caridy: that has this new thing that we can, that we have a hard time recently about it.

C

Caridy: from code. I I haven't seen how that is even possible to get your hands on something that.

C

Caridy:, wasn't there before some something that you just don't.

C

Caridy:, don't know who is changing, it. caridy: and I I don't feel like this- is introducing that, and it.. It feels to me that that's where your.

C

Mark s. miller: has it.

B

Mark s. miller: right?, so this this, the weird mark, s. miller:, coupling., mark s. miller:, the weird communication between parties.

B

Mark s. miller: that mark s. miller: would not be possible under mark s. miller:, normal o caps in a sequential imperative. okay.

B

Mark s. miller: that is possible in this extension.

B

Mark s. miller: is that mark s. miller:. Let's say that alice and bob are both inside the same.

B

Mark s. miller: hardened javascript system.

B

Mark s., miller: and they're, therefore sharing the same.

B

Mark s. miller: make async context, primordial.

B

Mark s. miller:, okay? mark s. miller: and mark s. miller: bob mark s. miller: makes mark s. miller: a mark s. miller:, a a a fluid variable and in instantiates. make a in context to create a new instance.

B

Mark s. miller: and then mark s. miller:, bob mark s. miller: mix mark s. miller: 2 calls to alice.

B

Mark s. miller: through a membrane., let's say.

B

Mark s. miller:, where the membrane mark s. miller: is mark s. miller:, going to prevent mark s. miller: is going to sensor, is going to prevent mark s. miller: anything mutable,, any any direct access to anything mutable from going through the membrane.

B

Mark s. miller:, so the membrane is, is imposed.. Let's say, by carol.

B

Mark s. miller:: that's trying to really reason about limits on the communication between allison bob.. How carol is trying to make it very hard for alice and bob to communicate.

B

Mark s. miller: in ways that carol cannot monitor.

B

Mark s. miller:, so now.

B

Mark s. miller: alice mark s. miller: during mark s. miller:. The call from bob.

B

Mark s. miller: falls back into bob.

B

Mark s., miller: and bob. mark s. miller: and tell that the time at which alice call back into bob.

B

Mark s. miller: is during mark s., miller: bob's call to alice.

B

mark s. miller: by virtue of the fact that that that bob's own fluid variable,, which he was not able to share with alice the asyn context instance, could not be shared with alice because of carol's sensor and membrane..

B

Mark s. miller:, but during the call back bob, can tell that the fluid variable has the binding.

B

Mark s. miller: that bob gave it because it was called back during the call to alice., but so far this no problem,, because one expects in a sequential imperative language that bob could tell that he's called back during the call to alice, anyway.

B

Mark s. miller: now let's say that we're in justin's full proposal.

B

Mark s. miller: now mark s. miller: bob calls back to alice, once.

B

Mark s. miller: binding the fluid variable to.

B

Mark s. miller:, through. mark s. miller: and then bob calls to alice again, binding the same fluid, variable to false.

B

Mark s. miller: and then. mark s. miller:, each time mark s. miller: alice, has done rap.

B

Mark s. miller: to capture one of those contexts.

B

Mark s. miller:, so the first time mark s. miller: alice calls the the rapt closure that.

B

Mark s. miller: calls it a. mark s. miller: in the second time. Alice calls the rap closure b.

B

Mark s. miller: at some later time.

B

mark s. miller:, when everything is returned,, there's nothing on stack, anymore.

B

Mark s. miller:, but mark s. miller:, alice spontaneously mark s. miller: calls some object of bob's again through the sensory membrane.

B

Mark s. miller: call some object of bob's that alice has access, to. alice has been given you, and carol has allowed all to have access to.

B

Mark s. miller:, but has censored mark s. miller:, all of the parameters. you know., let's say it's: it can pass 0 parameters., so alice now holds some object to bob passing 0 parameters.

B

Mark s. miller:, but depending on whether alice calls it using her a.

B

Mark s. miller: wrapper closure or be wrapper closure.

B

Mark s. miller: she communicates either a true or false to bomb.

B

Mark s. miller:, she can communicate one bit of information to bob.

B

Mark s. miller:, which is which of bob's calls to alice?, did alice temporarily capture and use for the call back.

B

Mark s. miller: and carol monitoring the sensory membrane.

B

Mark s. miller:, it looks like.

B

Mark s. miller: such an additional bit of communication, was not possible.

A

Kris “cowbert” kowal:. I think that we have to call here.

A

kris “cowbert” kowal: oh, thanks again, mark,, we'll presumably continue next week.

B

Mark s. miller:, okay,, very good., and I will. because I went over.

B

Mark s. miller: in a less confusing manner. what I went through last week in a self, and I think, in an adequately self-contained way,, I'm going to refer the for. I am folk to this recording, and not the previous recording.

A

Kris “cowbert” kowal: sounds good., kris “cowbert” kowal:, all right. thank you.

B