add command

Aegis/Commands.lean

@@ -101,6 +101,15 @@ initialize sierraSoundness : SimplePersistentEnvExtension (Identifier × Name)
     addImportedFn := fun ⟨pss⟩ => (HashMap.ofList (pss.map Array.toList).join)
   }
 
+initialize sierraContractCalls : SimplePersistentEnvExtension (Identifier × ContractCallData)
+    (HashMap (Nat × Nat) (Identifier × List ContractCallImplicit)) ←
+  registerSimplePersistentEnvExtension {
+    addEntryFn := fun specs (i, ⟨addr, sel, impl⟩) => specs.insert (addr.val, sel.val) (i, impl)
+    addImportedFn :=
+      let f ds := (ds.map fun (i, ⟨addr, sel, impl⟩) => ((addr.val, sel.val), (i, impl))).toList
+      fun ⟨pss⟩ => (HashMap.ofList (pss.map f).join)
+  }
+
 /- Provide elaboration functions for the commands -/
 
 def sierraLoadString (s : String) : CommandElabM Unit := do
@@ -200,5 +209,13 @@ elab "aegis_complete" : command => do
   for (i, _) in sf.declarations do
     unless (sierraSoundness.getState env).contains i do missingDecls := missingDecls.push i
   unless missingDecls.size = 0 do throwError
-    "Soundness proof not provided for the following declarations: {missingDecls}"
+    "Soundness proof not provided for the following {missingDecls.size} declarations: {missingDecls}"
   modifyEnv (loadedSierraFile.addEntry · default)  -- remove saved Sierra file after the command
+
+elab "aegis_register_contract_call" id:str addr:num sel:num : command => do
+  let .ok id ← liftCoreM <| parseIdentifier id.getString
+    | throwError "could not parse {id.getString} as Sierra identifier"
+  let addr := addr.getNat
+  let sel := sel.getNat
+  let data := { contractAddress := addr, selector := sel, implicits := [] }
+  modifyEnv (sierraContractCalls.addEntry · (id, data))

Aegis/Tests/Commands.lean

@@ -521,3 +521,5 @@ aegis_prove "test::foo" := fun _ a b ρ => by
   unfold Bool.toSierraBool
   unfold «spec_test::foo»
   aesop
+
+aegis_register_contract_call "bar" 42 23

Aegis/Types.lean

@@ -338,3 +338,16 @@ def FuncData.modifyConditions (fd : FuncData) (f : Expr → Expr) : FuncData whe
     { bd with condition := OfInputs.map f bd.condition }
 
 instance : Inhabited FuncData := ⟨{ }⟩
+
+/-- A structure to contain the information on the implicit that's added to the wrapper call
+for a registered contract call -/
+structure ContractCallImplicit where
+  (type : SierraType)
+  (pre : Q($type.toQuote))
+  (post : Q($type.toQuote))
+
+/-- A structure containing the data necessary to pin a contract call to a specific Sierra id -/
+structure ContractCallData where
+  (contractAddress : ContractAddress)
+  (selector : F)
+  (implicits : List ContractCallImplicit)