feat: Add simple authorization for class members #109
Conversation
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
janmasrovira
force-pushed
the
authorization
branch
4 times, most recently
from
d1b2ab4 to
82e19b9
Compare
janmasrovira
changed the title
janmasrovira
force-pushed
the
authorization
branch
3 times, most recently
from
d3fffd6 to
e85f3aa
Compare
commit 35ebc97 Author: Jan Mas Rovira <[email protected]> Date: Mon Sep 22 17:28:56 2025 +0200 destructors commit 18fcdd3 Author: Jan Mas Rovira <[email protected]> Date: Mon Sep 22 13:39:48 2025 +0200 syntax commit 6df404c Author: Jan Mas Rovira <[email protected]> Date: Mon Sep 22 13:13:24 2025 +0200 constrs and destr commit 2165afe Author: Jan Mas Rovira <[email protected]> Date: Mon Sep 22 10:17:33 2025 +0200 sigs commit 82e19b9 Author: Jan Mas Rovira <[email protected]> Date: Sun Sep 21 23:39:58 2025 +0200 proofs commit 2e06fac Author: Jan Mas Rovira <[email protected]> Date: Fri Sep 19 16:33:54 2025 +0200 wip commit 72faad1 Author: Jan Mas Rovira <[email protected]> Date: Fri Sep 19 08:25:44 2025 +0200 noSignatures commit fb64072 Author: Jan Mas Rovira <[email protected]> Date: Thu Sep 18 15:23:58 2025 +0200 signatures wip commit 4a5495e Author: Jan Mas Rovira <[email protected]> Date: Wed Sep 17 17:29:26 2025 +0200 store owner commit dc14617 Author: Jan Mas Rovira <[email protected]> Date: Wed Sep 17 15:42:56 2025 +0200 basic authorization for class members
janmasrovira
force-pushed
the
authorization
branch
from
e85f3aa to
559b62c
Compare
lukaszcz
reviewed
Sep 23, 2025
| call Counter.Methods.Incr rx (x.count * 2 + y.count) | ||
| call Counter.Methods.Incr ry (y.count * 2 + x.count) | ||
| call Counter.Methods.Incr rx (x.count * 2 + y.count) noSignatures | ||
| call Counter.Methods.Incr ry (y.count * 2 + x.count) noSignatures |
There was a problem hiding this comment.
This is super annoying to be forced to specify these noSignatures everywhere. Can we make signatures implicit, or at least leave call etc. as they are and add new callSig etc. with signatures?
lukaszcz
reviewed
Sep 23, 2025
| def counterIncr : @Class.Method label .unit Methods.Incr := defMethod OwnedCounter | ||
| (body := fun (self : OwnedCounter) (step : Nat) => ⟪return self.incrementBy step⟫) | ||
| (invariant := fun (self : OwnedCounter) (_step : Nat) signatures => | ||
| checkSignature (signatures .owner) self.owner) |
There was a problem hiding this comment.
We have this with every member. It would seem more natural to make this signature check a class invariant.
There was a problem hiding this comment.
as it stands, class invariants don't have access to signatures. Perhaps this could be an extension. We would define a SignatureId for the class, and all members would be able to provide that signature.
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Member calls can be passed signatures. These signatures can then be checked in the invariant of the member. The signature ensures that the memberId and its arguments have been signed by some authorized entity.