Revamp storage vectors

Author: mohammadfawaz

pintc/src/asm_gen/asm_builder.rs

@@ -809,6 +809,8 @@ impl<'a> AsmBuilder<'a> {
                 }
 
                 match kind {
+                    ExternalIntrinsic::PanicIf => asm.push(PNCIF),
+
                     ExternalIntrinsic::RecoverSECP256k1 => asm.push(RSECP),
 
                     ExternalIntrinsic::Sha256 => asm.extend([PUSH(3), SHL, SHA2]),

pintc/src/expr/intrinsics.rs

@@ -49,6 +49,9 @@ pub enum ExternalIntrinsic {
     // Returns the address of a predicate in the same contract
     AddressOf,
 
+    // Panics if supplied condition is `true`
+    PanicIf,
+
     // Recovers the public key from a secp256k1 signature.
     RecoverSECP256k1,
 
@@ -75,6 +78,7 @@ impl Display for ExternalIntrinsic {
     fn fmt(&self, f: &mut Formatter) -> Result {
         match self {
             Self::AddressOf => write!(f, "__address_of"),
+            Self::PanicIf => write!(f, "__panic_if"),
             Self::RecoverSECP256k1 => write!(f, "__recover_secp256k1"),
             Self::Sha256 => write!(f, "__sha256"),
             Self::SizeOf => write!(f, "__size_of"),
@@ -92,6 +96,9 @@ impl ExternalIntrinsic {
             Self::AddressOf => vec![
                 string(), // path to a predicate in the contract
             ],
+            Self::PanicIf => vec![
+                r#bool(), // path to a predicate in the contract
+            ],
             Self::RecoverSECP256k1 => vec![
                 b256(),                             // data hash
                 tuple(vec![b256(), b256(), int()]), // signature
@@ -116,6 +123,7 @@ impl ExternalIntrinsic {
     pub fn ty(&self) -> Type {
         match self {
             Self::AddressOf => b256(),
+            Self::PanicIf => any(),
             Self::RecoverSECP256k1 => tuple(vec![b256(), int()]),
             Self::Sha256 => b256(),
             Self::SizeOf => int(),

pintc/src/parser/context.rs

@@ -495,6 +495,7 @@ impl<'a> ParserContext<'a> {
             kind: (
                 match &name.name[..] {
                     "__address_of" => IntrinsicKind::External(ExternalIntrinsic::AddressOf),
+                    "__panic_if" => IntrinsicKind::External(ExternalIntrinsic::PanicIf),
                     "__recover_secp256k1" => {
                         IntrinsicKind::External(ExternalIntrinsic::RecoverSECP256k1)
                     }

pintc/src/parser/tests.rs

@@ -264,10 +264,7 @@ fn storage_types() {
     // Multi dimensional vectors are not yet supported
     check(
         &run_parser!(storage_var_type, "int[][]"),
-        expect_test::expect![[r#"
-            expected `?`, found `[`
-            @18..19: expected `?`
-        "#]],
+        expect_test::expect!["int[][]"],
     );
 }
 

pintc/src/pint_parser.lalrpop

@@ -548,11 +548,12 @@ MapType: Type = {
     }
 }
 
-// This only allows single dimensional vectors for the time being
 VectorType: Type = {
-    <l:@L> <ty:TypeAtom> "[" "]" <r:@R> => Type::Vector {
-        ty: Box::new(ty),
-        span: (context.span_from)(l, r),
+    <l:@L> <ty:TypeAtom> <ranges: ("[" "]")+> <r:@R> => {
+        ranges.iter().rev().fold(ty, |acc, _| Type::Vector {
+            ty: Box::new(acc),
+            span: (context.span_from)(l, r),
+        })
     }
 }
 

pintc/src/predicate/transform.rs

@@ -1,10 +1,8 @@
-mod legalize;
 mod lower;
 mod unroll;
 mod validate;
 
 use crate::error::{ErrorEmitted, Handler};
-use legalize::legalize_vector_accesses;
 use lower::{
     coalesce_prime_ops, lower_aliases, lower_array_ranges, lower_casts, lower_ifs,
     lower_imm_accesses, lower_ins, lower_matches, lower_storage_accesses,
@@ -80,11 +78,8 @@ impl super::Contract {
         // (e.g., `option::none`) from Expr::Path to Expr::UnionVariant.
         lower_union_variant_paths(&mut self);
 
-        // Insert OOB checks for storage vector accesses
-        let _ = legalize_vector_accesses(handler, &mut self);
-
-        // Lower all storage accesses to __storage_get and __storage_get_extern intrinsics. Also
-        // add constraints on mutable keys
+        // Lower all storage accesses to storage intrinsics (`__pre_state`, `__pre_state_extern`,
+        // `_post_state`, and `__post_state_extern`). Also add constraints on mutable keys
         let _ = lower_storage_accesses(handler, &mut self);
 
         // Ensure that the final contract is indeed final