-
Notifications
You must be signed in to change notification settings - Fork 0
languageNotes
- Status of refactoring
- Status of modeling
- System refactoring
- System is building building
- At least communication is failing, maybe more
- Working big and useful refinement for communication
- Pulling hard coded "things" out of demo
- Working on much less brittle provisioning mechanism
- Discussed modeling status
- State monad is unchanged
- Working on measurement semantics model
- Status
- Modeling results
- Implementation results
- Models and reification plans big picture
- went through the full coq state monad model
- Status
- Discuss protocol assembly language
- Went through the coq model so far.
- Status
- Discuss protocol assembly language
- Discuss protocol monad
- Protocol Assembly Language
- Information gathering - measurement, vTPM, nested Appraisal
- Control - map, fold, sequence, conditional
- Communication - send, receive
- Bundling - ???
- Failure - ???
- Define and populate a coq data type for this that will become a Haskell data type
- Document properties as a monad
- Include non-proper Morphisms
- Protocol monad
- Has the form of the protocol language
- Capture in coq?
- All entitles in the same monad
- Different state components
- Communication becomes exchange
- Reify from this structure to the assembly language above
- Has the form of the protocol language
- Does the protocol monad need to exist in Haskell or can it be a coq structure only?
- How good is coq->Haskell synthesis?
- Can we write and verify the reification there?
- Would be a great paper for the CPP conference
- Continued discussion of protocol monad construction
- Discuss evidence bundling
- What to formalize and how
- Post papers from Joshua and Paul
- Protocol monad
- Communication mechanism
- Conditional handling
- Errors
- Bundling - Did not discuss in this meeting
- Single realm
- Multi-realm
- Long conversations about what 'send' means
Go from send and receive pairs to send as a function that sends a remote action that results in a local action (see notes below). Thus, the form:
x <- send c R a
is the result of evaluating L a that results from the send evaluating R a. Local effect of a remote effect.
Gets interesting when L a causes a nested send. That's the picture above. Also when sends either stack or continue. Specifically, does the result of a send that produces another send immediately resolve like traditional protocols or does it build a structure that is run like a state monad? This is an open discussion point.
- Write up protocols
- Wide mouth frog
- Neidham Shroeder
- CA cert protocol
- Start thinking about evidence
- Continued discussion of protocol monad construction
###Protocol Monad
- Went through the current protocol monad work looking at the first monad class specification and various proofs
- Don't know what the state monad laws say completely and need to find the paper that Andy pulled them from
- Having difficulty extending the basic monad to a state monad in a "proper" way
- An interesting realization is the form of send:
send :: R a -> L a
What's interesing here is that send has a return value. Specifically, the result of sending R a to some other process is a local effect L a.
-
L a could be another send. We can stack these things up to build larger structures.
-
Verification
- Andy talked about verifying several monad properties that he is interested in for the remote monad.
eval (strong e) = eval e
Note that this has the same form as the transform verifications that I'm currently doing in coq. But, the transforms in Coq are over syntax. I don't think this is. He proposed something like this
eval (strong M >>= k) = eval (M >>= k)
1. eval (strong M) = M
2. eval (strong k a) = eval (k a)
While this has the form of a congruence relation, I don't think it is. There's something wrong here in the way the induction is structured. I'm not sure quite what to tell him to do, but the appearance of a in t