Skip to content

Commit 82e19b9

Browse files
janmasrovirajanmasrovira
committed
proofs
1 parent 2e06fac commit 82e19b9

File tree

6 files changed

+107
-29
lines changed

6 files changed

+107
-29
lines changed

‎AVM/Class/Label.lean‎

Lines changed: 30 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -35,18 +35,21 @@ structure Label : Type 1 where
3535
[constructorsFinite : Fintype ConstructorId]
3636
[constructorsRepr : Repr ConstructorId]
3737
[constructorsBEq : BEq ConstructorId]
38+
[constructorsLawfulBEq : LawfulBEq ConstructorId]
3839

3940
DestructorId : Type := Empty
4041
DestructorArgs : DestructorId -> SomeType := fun _ => ⟨PUnit⟩
4142
[destructorsFinite : Fintype DestructorId]
4243
[destructorsRepr : Repr DestructorId]
4344
[destructorsBEq : BEq DestructorId]
45+
[destructorsLawfulBEq : LawfulBEq DestructorId]
4446

4547
MethodId : Type
4648
MethodArgs : MethodId -> SomeType
4749
[methodsFinite : Fintype MethodId]
4850
[methodsRepr : Repr MethodId]
4951
[methodsBEq : BEq MethodId]
52+
[methodsLawfulBEq : LawfulBEq MethodId]
5053

5154
MethodSignatureId : MethodId → Type := fun _ => Empty
5255
[signaturesFinite : (m : MethodId) → Fintype (MethodSignatureId m)]
@@ -86,8 +89,33 @@ instance Label.MemberId.hasBEq {lab : Class.Label} : BEq (Class.Label.MemberId l
8689
| _, destructorId _ => false
8790
| methodId m1, methodId m2 => lab.methodsBEq.beq m1 m2
8891

89-
instance Label.MemberId.instReflBEq {lab : Class.Label} : ReflBEq (Class.Label.MemberId lab) where
90-
rfl := sorry
92+
instance Label.MemberId.instReflBEq {lab : Class.Label} : ReflBEq lab.MemberId where
93+
rfl := by
94+
intro a
95+
have := lab.constructorsLawfulBEq
96+
have := lab.destructorsLawfulBEq
97+
have := lab.methodsLawfulBEq
98+
cases a
99+
iterate 3 {
100+
unfold BEq.beq Label.MemberId.hasBEq
101+
simp
102+
}
103+
104+
instance Label.MemberId.instLawfulBEq {lab : Class.Label} : LawfulBEq (Class.Label.MemberId lab) where
105+
eq_of_beq := by
106+
intro a b
107+
have := lab.constructorsLawfulBEq
108+
have := lab.destructorsLawfulBEq
109+
have := lab.methodsLawfulBEq
110+
unfold BEq.beq Label.MemberId.hasBEq
111+
match ae : a, b with
112+
| constructorId c1, constructorId c2 => simp
113+
| constructorId _, _ => grind
114+
| _, constructorId _ => subst ae; intro x; cases a <;> simp at x; congr
115+
| destructorId c1, destructorId c2 => simp
116+
| destructorId _, _ => grind
117+
| _, destructorId _ => subst ae; intro x; cases a <;> simp at x; congr
118+
| methodId m1, methodId m2 => simp
91119

92120
instance Label.MemberId.hasTypeRep (lab : Class.Label) : TypeRep (Class.Label.MemberId lab) where
93121
rep := Rep.composite "AVM.Class.Label.MemberId" [Rep.atomic lab.name]

‎AVM/Class/Translation/Logics.lean‎

Lines changed: 29 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -61,9 +61,6 @@ private def Method.Message.logicFun
6161
let! [selfRes] := consumedResObjs
6262
let try selfObj : Object classId := Object.fromResource selfRes
6363
check method.invariant selfObj argsData
64-
let signatures0 : msg.id.Signatures msg.args := msg.signatures
65-
let signatures : methodId.Signatures argsData := sorry
66-
check method.authorization selfObj argsData signatures
6764
let body := method.body selfObj argsData
6865
let try vals : body.params.Product := tryCast msg.vals
6966
let createdObject : Object classId := body |>.value vals
@@ -79,17 +76,35 @@ private def Method.Message.logicFun2
7976
(args : Logic.Args)
8077
: Bool :=
8178
let try msg : Message lab := Message.fromResource args.self
82-
83-
-- let try msg : Message lab := Message.fromResource args.self
84-
-- let try argsData := SomeType.cast msg.args
85-
-- let consumedResObjs := Logic.selectObjectResources args.consumed
86-
-- let createdResObjs := Logic.selectObjectResources args.created
87-
-- let! [selfRes] := consumedResObjs
88-
-- let try selfObj : Object classId := Object.fromResource selfRes
89-
-- check method.invariant selfObj argsData
90-
-- let signatures0 : msg.id.Signatures msg.args := msg.signatures
91-
-- let signatures : methodId.Signatures argsData := sorry
92-
-- false
79+
if h : msg.id == .classMember (Label.MemberId.methodId methodId)
80+
then
81+
have msgId := eq_of_beq h
82+
let argsData : methodId.Args.type := by
83+
refine cast ?_ msg.args
84+
rw [msgId]
85+
rfl
86+
let consumedResObjs := Logic.selectObjectResources args.consumed
87+
let createdResObjs := Logic.selectObjectResources args.created
88+
let! [selfRes] := consumedResObjs
89+
let try selfObj : Object classId := Object.fromResource selfRes
90+
check method.invariant selfObj argsData
91+
let body := method.body selfObj argsData
92+
let try vals : body.params.Product := tryCast msg.vals
93+
let signatures : methodId.Signatures argsData := by
94+
intro signer
95+
have s := msg.signatures (msgId ▸ signer)
96+
subst argsData
97+
refine cast ?_ s
98+
congr
99+
rw [msgId]
100+
apply HEq.symm
101+
apply cast_heq
102+
check method.authorization selfObj argsData signatures
103+
let createdObject : Object classId := body |>.value vals
104+
Logic.checkResourceValues [createdObject.toObjectValue] createdResObjs
105+
&& Logic.checkResourcesPersistent consumedResObjs
106+
&& Logic.checkResourcesPersistent createdResObjs
107+
else false
93108

94109
/-- The class logic checks if all consumed messages in the action correspond to
95110
class members, the single consumed object is the receiver, and there is

‎AVM/Class/Translation/Messages.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -72,7 +72,7 @@ def MultiMethod.message
7272
(args : multiId.Args.type)
7373
(vals : (method.body selves args).params.Product)
7474
: Message lab :=
75-
let res : MultiMethodResult multiId := body.value vals
75+
let res : MultiMethodResult multiId := method.body selves args |>.value vals
7676
let data := res.data
7777
{ id := .multiMethodId multiId
7878
logicRef := MultiMethod.Message.logic.{0, 0} method data |>.reference

‎AVM/Class/Translation/Tasks.lean‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -75,7 +75,7 @@ private partial def Body.tasks'
7575
let task := destr.task' adjust eco r (adjust self) args
7676
Tasks.task task.task fun vals =>
7777
Body.tasks' (task.adjust vals) eco next cont
78-
| .method classId methodId selfId args next =>
78+
| .method classId methodId selfId args signatures next =>
7979
let method := eco.classes classId |>.methods methodId
8080
Tasks.fetch selfId fun self => Tasks.rand fun r =>
8181
let task := method.task' adjust eco r (adjust self) args signatures
@@ -206,7 +206,7 @@ private partial def Class.Method.task'
206206
{ consumed := [consumedObj]
207207
created := [createdObject] }
208208
let mkMessage (vals : body.params.Product) : SomeMessage :=
209-
method.message ⟨body.params.Product⟩ vals self.uid args
209+
method.message ⟨body.params.Product⟩ vals self.uid args signatures
210210
Body.task' adjust eco body mkReturn mkActionData mkMessage
211211

212212
partial def Ecosystem.Label.MultiMethodId.task'
@@ -277,7 +277,7 @@ partial def Ecosystem.Label.MultiMethodId.task'
277277
ensureUnique := rands.reassembledNewUidNonces.toList }
278278

279279
let mkMessage (vals : body.params.Product) : SomeMessage :=
280-
⟨(eco.multiMethods multiId).message selves args body vals⟩
280+
⟨(eco.multiMethods multiId).message selves args vals⟩
281281

282282
Body.task' adjust eco body mkResult mkActionData mkMessage
283283

‎AVM/Ecosystem/Label/Base.lean‎

Lines changed: 43 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -11,6 +11,7 @@ structure Label : Type 1 where
1111
[classesEnum : FinEnum ClassId]
1212
[classesRepr : Repr ClassId]
1313
[classesBEq : BEq ClassId]
14+
[classesDecidableEq : DecidableEq ClassId]
1415

1516
MultiMethodId : Type := Empty
1617
/-- Type of multiMethod arguments excluding `self` arguments. -/
@@ -24,6 +25,7 @@ structure Label : Type 1 where
2425
[multiMethodsFinite : FinEnum MultiMethodId]
2526
[multiMethodsRepr : Repr MultiMethodId]
2627
[multiMethodsBEq : BEq MultiMethodId]
28+
[multiMethodsLawfulBEq : LawfulBEq MultiMethodId]
2729

2830
instance Label.hasTypeRep : TypeRep Label where
2931
rep := Rep.atomic "AVM.Ecosystem.Label"
@@ -127,6 +129,47 @@ inductive MemberId (lab : Ecosystem.Label) where
127129

128130
namespace MemberId
129131

132+
instance instBEq {lab : Ecosystem.Label} : BEq (MemberId lab) where
133+
beq a b :=
134+
have := lab.classesDecidableEq
135+
match a, b with
136+
| .multiMethodId m1, .multiMethodId m2 =>
137+
have := lab.multiMethodsBEq
138+
m1 == m2
139+
| .multiMethodId _ , _ => false
140+
| _, .multiMethodId _ => false
141+
| .classMember (classId := c1) m1, classMember (classId := c2) m2 =>
142+
if h : c1 = c2
143+
then m1 == h ▸ m2
144+
else false
145+
146+
instance instReflBEq {lab : Ecosystem.Label} : ReflBEq (MemberId lab) where
147+
rfl := by
148+
have := lab.multiMethodsLawfulBEq
149+
intro a; cases a
150+
unfold BEq.beq instBEq; simp
151+
case classMember classId classMem =>
152+
unfold BEq.beq instBEq;
153+
have i : ReflBEq classId.MemberId := @Class.Label.MemberId.instReflBEq classId.label
154+
simp
155+
156+
-- TODO simplify
157+
instance instLawfulBEq {lab : Ecosystem.Label} : LawfulBEq lab.MemberId where
158+
eq_of_beq := by
159+
intro a b e
160+
have i := lab.multiMethodsLawfulBEq
161+
unfold BEq.beq instBEq at e; simp at e; split at e; simp
162+
apply i.eq_of_beq
163+
assumption
164+
contradiction
165+
contradiction
166+
split at e
167+
case h_4.isTrue _ _ _ _ h =>
168+
subst h;
169+
have x := Class.Label.MemberId.instLawfulBEq.eq_of_beq e
170+
subst x; simp
171+
contradiction
172+
130173
abbrev SignatureId (lab : Ecosystem.Label) : MemberId lab → Type
131174
| .classMember m => m.SignatureId
132175
| _ => Empty
@@ -139,14 +182,6 @@ abbrev Args {lab : Ecosystem.Label} (memberId : MemberId lab) : SomeType :=
139182
abbrev Signatures {lab : Ecosystem.Label} (m : MemberId lab) (args : m.Args.type) : Type :=
140183
m.SignatureId → Signature args
141184

142-
instance hasBEq (lab : Ecosystem.Label) : BEq (Ecosystem.Label.MemberId lab) where
143-
beq a b :=
144-
match a, b with
145-
| multiMethodId c1, multiMethodId c2 => lab.multiMethodsBEq.beq c1 c2
146-
| multiMethodId _, _ => false
147-
| _, multiMethodId _ => false
148-
| classMember c1, classMember c2 => c1 === c2
149-
150185
def numObjectArgs {lab : Ecosystem.Label} (memberId : MemberId lab) : Nat :=
151186
match memberId with
152187
| multiMethodId f => f.numObjectArgs

‎Apps/KudosBank.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -78,7 +78,7 @@ instance hasTypeRep : TypeRep Check where
7878

7979
inductive Methods where
8080
| Transfer
81-
deriving Repr, BEq, Fintype
81+
deriving Repr, BEq, Fintype, DecidableEq
8282

8383
structure TransferArgs where
8484
newOwner : PublicKey

0 commit comments

Comments
 (0)