Skip to content

Commit 6f26796

Browse files
lefterislazarlefterislazar
committed
Typing nit and Rocq partial fixes
1 parent f942f78 commit 6f26796

File tree

2 files changed

+18
-26
lines changed

2 files changed

+18
-26
lines changed

‎src/Act/Coq.hs‎

Lines changed: 17 additions & 25 deletions
Original file line numberDiff line numberDiff line change
@@ -144,7 +144,7 @@ extStep main store = inductive
144144
localStore = contractStore main store
145145

146146
substep :: Id -> (SlotType, Integer) -> Maybe (T.Text, Maybe T.Text, T.Text)
147-
substep var (StorageValue (ContractType cid), _) = Just (extStepType <> "_" <> varp, Just (envDecl <+> stateDecl <+> envVar' <+> stateDecl'), body')
147+
substep var (StorageValue (TContract cid), _) = Just (extStepType <> "_" <> varp, Just (envDecl <+> stateDecl <+> envVar' <+> stateDecl'), body')
148148
where
149149
varp = T.pack var
150150
body' = indent 2 . implication . concat $
@@ -161,7 +161,7 @@ extStep main store = inductive
161161
substep _ _ = Nothing
162162

163163
subBounds :: Id -> Id -> (SlotType, Integer) -> Maybe T.Text
164-
subBounds stepVar var (StorageValue (ContractType cid), _) | var /= stepVar = Just $ T.pack cid <.> "integerBoundsRec" <+> parens (T.pack var <+> stateVar)
164+
subBounds stepVar var (StorageValue (TContract cid), _) | var /= stepVar = Just $ T.pack cid <.> "integerBoundsRec" <+> parens (T.pack var <+> stateVar)
165165
subBounds _ _ _ = Nothing
166166

167167

@@ -198,7 +198,7 @@ contractAddressIn name store = inductive
198198
localStore = contractStore name store
199199

200200
subCAddr :: Id -> (SlotType, Integer) -> Maybe (T.Text, Maybe T.Text, T.Text)
201-
subCAddr var (StorageValue (ContractType cid), _) = Just ("addressOf_" <> varp, Just $ parens ("p : address") <+> stateDecl, body')
201+
subCAddr var (StorageValue (TContract cid), _) = Just ("addressOf_" <> varp, Just $ parens ("p : address") <+> stateDecl, body')
202202
where
203203
varp = T.pack var
204204
body' = indent 2 . implication $
@@ -219,13 +219,13 @@ addressIn name store = inductive
219219
localStore = contractStore name store
220220

221221
subAddr :: Id -> (SlotType, Integer) -> Maybe (T.Text, Maybe T.Text, T.Text)
222-
subAddr var (StorageValue (PrimitiveType AbiAddressType), _) =
222+
subAddr var (StorageValue TAddress, _) =
223223
let varp = T.pack var in
224224
Just ("address_" <> varp, Just stateDecl, indent 5 $ addressInType <+> parens (varp <+> stateVar) <+> stateVar)
225225
subAddr _ _ = Nothing
226226

227227
slotContractName :: SlotType -> Maybe Id
228-
slotContractName (StorageValue (ContractType cid)) = Just cid
228+
slotContractName (StorageValue (TContract cid)) = Just cid
229229
slotContractName _ = Nothing
230230

231231
noAliasing :: Id -> Store -> T.Text
@@ -267,22 +267,18 @@ intBounds name store = inductive
267267
localStore = contractStore name store
268268

269269
go :: Id -> (SlotType, Integer) -> Maybe T.Text
270-
go v (StorageValue (ContractType cid), _) = Just $
270+
go v (StorageValue (TContract cid), _) = Just $
271271
"0 <=" <+> T.pack cid <.> addrField <+> parens (T.pack v <+> stateVar) <+> "<= UINT_MAX 160"
272-
go v (StorageValue (PrimitiveType (AbiUIntType n)), _) = Just $
272+
go v (StorageValue (TInteger n Unsigned), _) = Just $
273273
"0 <=" <+> T.pack v <+> stateVar <+> "<= UINT_MAX" <+> T.pack (show n)
274-
go v (StorageValue (PrimitiveType (AbiIntType n)), _) = Just $
274+
go v (StorageValue (TInteger n Signed), _) = Just $
275275
"INT_MIN" <+> T.pack (show n) <+> "<=" <+> T.pack v <+> stateVar <+> "<= INT_MAX" <+> T.pack (show n)
276-
go v (StorageValue (PrimitiveType (AbiBytesType n)), _) = Just $
277-
"0 <=" <+> T.pack v <+> stateVar <+> "<= UINT_MAX" <+> T.pack (show (8*n))
278-
go v (StorageMapping is (ContractType cid), _) = Just $ parens $
276+
go v (StorageMapping is (TContract cid), _) = Just $ parens $
279277
"forall" <+> ixs (length is) <> ", 0 <=" <+> T.pack cid <.> addrField <+> parens (T.pack v <+> stateVar <+> ixs (length is)) <+> "<= UINT_MAX 160"
280-
go v (StorageMapping is (PrimitiveType (AbiUIntType n)), _) = Just $ parens $
278+
go v (StorageMapping is (TInteger n Unsigned), _) = Just $ parens $
281279
"forall" <+> ixs (length is) <> ", 0 <=" <+> T.pack v <+> stateVar <+> ixs (length is) <+> "<= UINT_MAX" <+> T.pack (show n)
282-
go v (StorageMapping is (PrimitiveType (AbiIntType n)), _) = Just $ parens $
280+
go v (StorageMapping is (TInteger n Signed), _) = Just $ parens $
283281
"forall" <+> ixs (length is) <> ", INT_MIN" <+> T.pack (show n) <+> "<=" <+> T.pack v <+> stateVar <+> ixs (length is) <+> "<= INT_MAX" <+> T.pack (show n)
284-
go v (StorageMapping is (PrimitiveType (AbiBytesType n)), _) = Just $ parens $
285-
"forall" <+> ixs (length is) <> ", 0 <=" <+> T.pack v <+> stateVar <+> ixs (length is) <+> "<= UINT_MAX" <+> T.pack (show (n * 8))
286282
go _ _ = Nothing
287283

288284
ixs n = T.unwords $ T.pack . (<>) "i" . show <$> [0..(n-1)]
@@ -296,24 +292,20 @@ intBoundsRec name store = inductive
296292
localStore = contractStore name store
297293

298294
go :: Id -> (SlotType, Integer) -> [T.Text]
299-
go v (StorageValue (ContractType cid), _) =
295+
go v (StorageValue (TContract cid), _) =
300296
[ "0 <=" <+> T.pack cid <.> addrField <+> parens (T.pack v <+> stateVar) <+> "<= UINT_MAX 160"
301297
, T.pack cid <.> "integerBoundsRec" <+> parens (T.pack v <+> stateVar) ]
302-
go v (StorageValue (PrimitiveType (AbiUIntType n)), _) = pure $
298+
go v (StorageValue (TInteger n Unsigned), _) = pure $
303299
"0 <=" <+> T.pack v <+> stateVar <+> "<= UINT_MAX" <+> T.pack (show n)
304-
go v (StorageValue (PrimitiveType (AbiIntType n)), _) = pure $
300+
go v (StorageValue (TInteger n Signed), _) = pure $
305301
"INT_MIN" <+> T.pack (show n) <+> "<=" <+> T.pack v <+> stateVar <+> "<= INT_MAX" <+> T.pack (show n)
306-
go v (StorageValue (PrimitiveType (AbiBytesType n)), _) = pure $
307-
"0 <=" <+> T.pack v <+> stateVar <+> "<= UINT_MAX" <+> T.pack (show (8*n))
308-
go v (StorageMapping is (ContractType cid), _) =
302+
go v (StorageMapping is (TContract cid), _) =
309303
[ parens $ "forall" <+> ixs (length is) <> ", 0 <=" <+> T.pack cid <.> addrField <+> parens (T.pack v <+> stateVar <+> ixs (length is)) <+> "<= UINT_MAX 160"
310304
, parens $ "forall" <+> ixs (length is) <> "," <+> T.pack cid <.> "integerBoundsRec" <+> parens (T.pack v <+> stateVar <+> ixs (length is)) ]
311-
go v (StorageMapping is (PrimitiveType (AbiUIntType n)), _) = pure $ parens $
305+
go v (StorageMapping is (TInteger n Unsigned), _) = pure $ parens $
312306
"forall" <+> ixs (length is) <> ", 0 <=" <+> T.pack v <+> stateVar <+> ixs (length is) <+> "<= UINT_MAX" <+> T.pack (show n)
313-
go v (StorageMapping is (PrimitiveType (AbiIntType n)), _) = pure $ parens $
307+
go v (StorageMapping is (TInteger n Signed), _) = pure $ parens $
314308
"forall" <+> ixs (length is) <> ", INT_MIN" <+> T.pack (show n) <+> "<=" <+> T.pack v <+> stateVar <+> ixs (length is) <+> "<= INT_MAX" <+> T.pack (show n)
315-
go v (StorageMapping is (PrimitiveType (AbiBytesType n)), _) = pure $ parens $
316-
"forall" <+> ixs (length is) <> ", 0 <=" <+> T.pack v <+> stateVar <+> ixs (length is) <+> "<= UINT_MAX" <+> T.pack (show (n * 8))
317309
go _ _ = []
318310

319311
ixs n = T.unwords $ T.pack . (<>) "i" . show <$> [0..(n-1)]

‎src/Act/Type.hs‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -471,7 +471,7 @@ checkExpr env t1 e =
471471
maybe (maybeCast (getPosn e) t1 t2) (\Refl -> pure te) $ relaxedIntCheck t1 t2)
472472
where
473473
maybeCast :: Pn -> TValueType a -> TValueType b -> Exp b t -> Err (Exp a t)
474-
maybeCast pn TInteger (TContract c) te = pure $ Address pn c te) --TODO: is pn correct here?
474+
maybeCast pn TInteger (TContract c) te = pure $ Address pn c te --TODO: is pn correct here?
475475
-- maybeCast _ (SSArray _) s1' (SSArray _) s2 _ | s1' == s2 = -- TODO: cast of whole array of contracts?
476476
maybeCast pn t1' t2 _ = typeMismatchErr pn t1' t2
477477

0 commit comments

Comments
 (0)