Expected behavior of exercise transaction and transactions in general

[roehst]

Hello Folks,

I need to ask a quick question about a specific point in how transactions work.

Transfer transaction

The transfer transaction has a balance security ID and possibly many resulting security IDs.

So I understand that if a stakeholder owns 1000 shares and transfer 800, we should create a security for 200 shares (balance) and another one for 800 shares (result).

Now let's compare that to some lines from the sample dataset.

Open-Cap-Format-OCF/samples/Transactions.ocf.json

Lines 711 to 722 in 616d972

	{
	"object_type": "TX_STOCK_TRANSFER",
	"id": "test-stock-transfer-minimal",
	"security_id": "test-security-id",
	"date": "2022-02-01",
	"resulting_security_ids": [
	"resultant-security-id-1",
	"resultant-security-id-2",
	"resultant-security-id-3"
	],
	"quantity": "10"
	},

This creates 3 resulting securities.

So I have a question.

How can we tell how many shares each security owns? One hypothesis was that a new Issuance transaction would actually define how many shares each has. But I don't see that in the sample file. Is this how it should work?

Exercise transaction

In the same vein, I see that there is a sample exercise transaction that creates two securities.

Open-Cap-Format-OCF/samples/Transactions.ocf.json

Lines 272 to 282 in 616d972

	{
	"object_type": "TX_PLAN_SECURITY_EXERCISE",
	"id": "test-plan-security-exercise-minimal",
	"security_id": "test-security-id",
	"date": "2019-12-12",
	"resulting_security_ids": [
	"resultant-security-id-1",
	"resultant-security-id-2"
	],
	"quantity": "100"
	},

Again, how should I interpret this event? I expected that an exercise would create a single new security.

Thanks in advance

[JSv4]

Hey @roehst, good question. At the moment our samples are not meant to be a read together as a single, internally-consistent cap table. The various objects in the samples are syntactically correct to show what OCF looks like, but are not meant to be read together. We do have an open issue to write detailed walkthroughs (#158 - see more below), so we will be creating some material that shows more accurately what "real world" OCF looks like.

So here:

Open-Cap-Format-OCF/samples/Transactions.ocf.json

Lines 711 to 722 in 616d972

	{
	"object_type": "TX_STOCK_TRANSFER",
	"id": "test-stock-transfer-minimal",
	"security_id": "test-security-id",
	"date": "2022-02-01",
	"resulting_security_ids": [
	"resultant-security-id-1",
	"resultant-security-id-2",
	"resultant-security-id-3"
	],
	"quantity": "10"
	},

You are correct there are three resulting_security_ids. If we use the paper analog of certificates, this basically means that we had a certificate outstanding with id (or certificate #) of test-security-id. Now, this OCF transfer event tells us that 1) there were three new security ids created as a result of the transfer and 2) there was no remaining_security_id, so the entirety of the shares represented on this "certificate" were transfered.

To create the new security ids, you'd need to create three Stock Issuance Events, one for each of the new security ids. Each issuance event would set for the number of applicable shares and the stakeholders who now own them, so that's how you'd determine ownership for the resulting securities.

So, to recap, to actually model this transfer in real life, you'd need four events: three issuance events and one transfer event. Each issuance will refer to its stakeholder. If they don't already exist, you'll need to add stakeholder objects for them too, but that doesn't require an event, you just add to the stakeholder ocf file / list.

As for the exercise, you are seeing a similar pattern. The exercise event example you noted would need two issuance events to create securities with ids resultant-security-id-1 and resultant-security-id-2. There'd be 100 shares total issued between the two certificates, and you'd apportion the actual amounts in the issuance events for each resulting issuance in its issuance object.

Since you're already working through this, do you have an interest in helping us write some walkthroughs / how-tos for basic transactions like this? We have an open issue #158 where we've been discussing the need for these kinds of how-tos for a while. If you want to write a short write-up for how to do a transfer, for example, or an option exercise, we'd certainly welcome the contribution.

[roehst]

For example, we can start from a naive model.

abstract sig Transaction {}

sig Security {
}

sig Stakeholder {
}

sig Issue extends Transaction {
    security : one Security,
    stakeholder : one Stakeholder
}

sig Transfer extends Transaction {
    security : one Security,
    from : one Stakeholder,
    to : one Stakeholder,
    balancingSecurity : lone Security,
    resultingSecurity : one Security
}

And we get pretty visualizations for the possible instances of this model.

Then, we can ask the model checker to find an instance with 2 transfers by issuing the command run { #Transfer = 2 }

And clearly there is a problem here, because Security$0 is both the balancingSecurity and resultingSecurity for Transfer$0.
This means we have to add further constraints to the model, but this is the general workflow.

[JSv4]

@roehst, that is really, really cool! One of our to-do items on our roadmap is to build in this kind of validation. I'm not familiar with Alloy, so I'll have to dig in more. It strikes me that's some pretty cool infrastructure that it'd be great to leverage. How much work do you think it'd be to maintain some kind of model of OCF in Alloy parallel to the schemas themselves (and is there a way to auto-convert them)?

[roehst]

Hard to give any meaningful estimate. It is a steep learning curve, but easy to use afterwards.

Structural models require understanding of tables and associations in SQL + some basic familiarity with set operations and logic certainly helps. Temporal models require understanding state machines.

The infra is pretty cool indeed, and Alloy exposes the model programmatically, so translating Alloy to JSON schema is possible in principle. So is generating SQL schemas.

Also in principle it is possible to generate test suites and test cases from Alloy specifications. All the information to do that is already there in the model (it can generate failing and passing test instances, for example).

I can certainly share introductory material on Alloy and formal methods and give a little tutorial if you wish to investigate this further.

Rodrigo

[naveedn]

Rodrigo, I'd love to learn if you have any introductory materials. This feels like an effective DSL for us to write test cases against.

[roehst]

Hi naveedn, I think those are good starting points:

1. Download the Alloy Analyzer from alloytools.org
2. Skim over the slides in https://alloytools.org/tutorials/day-course/ for an overview
3. Follow through the material in https://haslab.github.io/formal-software-design/overview/index.html
4. See https://alloy.readthedocs.io/ for reference on the standard library

And if you'd like to see in action, you can message me directly at ro.stevaux AT gmail.com.

In terms of writing test cases, alloy has excellent support for defining scenarios and checking if they are satisfiable/possible.

[roehst]

Just checking, I have so much to share on this issue after many months of research into the matter.

[victormimo]

Hi @roehst, I'm currently translating parts of this standard to be used on-chain. I've spent months also digging into OCF. Want to jump on a call to share notes?

my email is [email protected]

[roehst]

Hi victor, I would be glad to. I am finishing writing my master’s thesis on a formalized version of the model, and I do compare it to bitcoins utxo, so I would be interested to exchange ideas. I will reach you on email Em qui., 3 de ago. de 2023 às 20:16, Victor Mimo ***@***.***> escreveu:

…

Hi @roehst <https://github.com/roehst>, I'm currently translating parts of this standard to be used on-chain. I've spent months also digging into OCF. Want to jump on a call to share notes? my email is ***@***.*** — Reply to this email directly, view it on GitHub <#278 (reply in thread)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AFASTCZHA7G4633CI26MQHTXTQWLVANCNFSM6AAAAAARBT7MUM> . You are receiving this because you were mentioned.Message ID: <Open-Cap-Table-Coalition/Open-Cap-Format-OCF/repo-discussions/278/comments/6632528 @github.com>

[victormimo]

Awesome. We've got a group of ~4 crypto companies working on this together. So super interested. Will wait for your email.

[victormimo]

Hey guys, I have a few questions relating to security_id, custom_id, and shares_numbers_issued, the above discussion has helped but I'm looking for confirmation.

In this tutorial

We see that for a full transfer between Bob and Alice, we have 3 events (initial Bob issuance, Alice issuance, and Transfer). So far everything is clear. My assumption is that security_id is created during the TX_STOCK_ISSUANCE transaction right, does this imply that a security_id is an ID for the entire position of a stakeholder? so bob-stock-1 is an ID that maps to this issuance TX that indicates Bob has 1000 shares of SeriesA stock that was priced at USD 1/share. I'm currently operating with this assumption since every time a transfer is done, we need to create another issuance event for Bob (and I'm thinking this is for their new position). Let me know if that's accurate.

Now, if the assumption above is correct, how is the custom_id related to security_id? Eg. in the first issuance event below, security_id is "bob-stock-1" in a prod environment this would be a UUID, so custom_id: "PA-1" can indicate that this is the first position in Preferred Stock for Series A (assuming that stock_class_id is for preferred shares). So is custom_id used to make the position more human readable than security_id?

Lastly, can someone point me to a use-case where shares_numbers_issued would be used in practice? I gather from this description
"Range(s) of the specific share numbers included in this issuance. This is different from a certificate number you might include in the custom_id field or the security_id created in this issuance. This field should be used where, for whatever reason, shares are not fungible and you must track, with each issuance, which specific share numbers are included in the issuance - e.g. share numbers 1 - 100 and 250-300."
That it deals with non-fungible shares, I'm more so curious what this would look like in practice.

[
{
"object_type": "TX_STOCK_ISSUANCE",
"id": "give-bob-some-stock",
"security_id": "bob-stock-1",
"date": "2022-02-01",
"security_law_exemptions": [],
"stakeholder_id": "bob",
"custom_id": "PA-1",
"stock_class_id": "SeriesA",
"share_price": {
"amount": "1.00",
"currency": "USD"
},
"quantity": "1000",
"cost_basis": {
"amount": "1.00",
"currency": "USD"
},
"stock_legend_ids": [
"series-a-legend"
]
},
...
{
"object_type": "TX_STOCK_ISSUANCE",
"id": "give-alice-the-stock",
"security_id": "alice-stock-1",
"date": "2023-02-01",
"security_law_exemptions": [],
"stakeholder_id": "alice",
"custom_id": "PA-23",
"stock_class_id": "SeriesA",
"share_price": {
"amount": "2.73",
"currency": "USD"
},
"quantity": "1000",
"cost_basis": {
"amount": "2.73",
"currency": "USD"
},
"stock_legend_ids": [
"series-a-legend"
]
},
{
"object_type": "TX_STOCK_TRANSFER",
"id": "bob-transfer-to-alice",
"security_id": "bob-stock-1",
"date": "2023-02-01",
"resulting_security_ids": [
"alice-stock-1"
],
"quantity": "1000"
}
]

Thanks! I truly appreciate the work being done here.