Implement hints documentation #378

Iwueseiter · 2024-04-29T17:21:48Z

Resolves #327

… hint_examples_docs

cicr99 · 2024-05-03T11:16:22Z

docs/docs/vm-fundamentals/hints.md

+Sequencers and provers are tools used in formal verification, a process of accurately proving the correctness of programs.
+Applying hints in the Cario virtual machine leverages the execution trace and uses it to guide the verification process. Integration of hints with the Cairo VM's execution trace and verification tools enables developers to guide and customize the verification process, improving the efficiency and effectiveness of formal verification for smart contracts.


Could you point out the resource you used for this part? I'm not sure hints are related to formal verification techniques.

Also I would like to add in this documentation some information regarding the way we implement hints. You can use the content from https://github.com/NethermindEth/cairo-vm-go/blob/main/pkg/hintrunner/zero/README.md as reference.

… hint_examples_docs

rodrigo-pino · 2024-05-08T10:23:36Z

docs/package-lock.json

De-commit this file please

rodrigo-pino · 2024-05-08T10:24:42Z

docs/docs/vm-fundamentals/hints.md

-# Hints
+# Hint
+  ## HINTS  IN CAIRO VIRTUAL MACHINE
+Hints in Cairo are pieces of Python code only seen and executed by the prover and are not included in the bytecode. They instruct the prover on how to handle nondeterministic instructions. These nondeterministic instructions are programs that have different outcomes at execution.   


Only executed by the sequencer, and are not known during proving time

rodrigo-pino · 2024-05-08T10:27:06Z

docs/docs/vm-fundamentals/hints.md

+In Cairo, execution hints use the *hint* keyword, followed by a *hint name* and *a value*.
+
+ @example:
+
+ ```cairo  
+      func main() -> felt*:
+      // some code here
+      hint memory_behavior = MemoryBehavior.Sequential;
+      // more code here
+  ```
+  The memory_behavior hint informs the Cairo compiler that the code following the hint   
+ sequentially accesses memory.
+


Are you sure? I think hints are enclosed in a block defined by the following symbols %{ and }%

rodrigo-pino · 2024-05-08T10:29:31Z

docs/docs/vm-fundamentals/hints.md

+### MEMORY HINTS
+ These hints are memory aids that provide additional information to the prover on computing values in the Cairo program. They are functional when provers can't handle certain expressions implicitly.


That is not actual essence of hints. Cairo is a non-deterministic language, meaning, imagine a Turing Machine where you can visit different states at the same time (in theory). In practice, that's super expensive and can grow exponentially in memory. Hints are used to avoid all of this, and "hint" the VM to which state it should jump into (of the many possible)

rodrigo-pino · 2024-05-08T10:30:42Z

docs/docs/vm-fundamentals/hints.md

+### RESOURCE MANAGEMENT HINTS
+These hints provide additional information on managing resources like memory and stack space. They help the virtual Machine optimize resource usage and prevent resource leaks. Resource management hints need to be applied judiciously and only when necessary.
+
+@example:
+
+ ``` cairo
+    %{__resource_management_hint__ memory_pages_allocated = 10 %}
+        [ap] = 0, ap++;
+     for i in range(10):
+        [ap] = i, ap++;
+   %{__resource_management_hint__ memory_pages_allocated =  %}
+     for i in range(5):
+      [ap] = i * i, ap++;
+ ```
+
+The first hint will ensure the program has *`10`* memory pages to execute the first loop that stores *`10`* integers on the stack.
+The second hint will ensure the program does not use more memory than necessary.


This is not true. What source do you have?

rodrigo-pino · 2024-05-08T10:31:01Z

docs/docs/vm-fundamentals/hints.md

+### DEBUGGING HINTS
+They aid in troubleshooting and debugging Cairo programs. They identify and diagnose issues in the program. It debugs errors related to memory access and manipulation. Debugging hints are deleted from the program once the debugging is complete.
+
+ @example:
+
+```cairo
+    %{
+       import os
+       print("Debugging hint: Memory at address {}".format(memory[ap - 1]))
+    %}
+    [ap - 1] = 42, ap++;
+```
+
+The debugging hint prints the value stored in memory and the address stored in the register *ap - 1*.


rodrigo-pino · 2024-05-08T10:31:10Z

docs/docs/vm-fundamentals/hints.md

+### SECURITY HINTS
+Security hints in Cairo VM provide security features and protections for programs through directions for input validation, access control, or encryption to safeguard against potential vulnerabilities and threats.
+
+@example:
+
+```cairo
+     %{ 
+       import cairo 
+        cairo.set_max_stack_size(1024) 
+     %} 
+       [ap] = 42, ap++;
+ ```
+The security hint sets the maximum stack size for the program to *1024*.


rodrigo-pino · 2024-05-08T10:31:58Z

docs/docs/vm-fundamentals/hints.md

+## HOW HINTS WORK IN CAIRO VIRTUAL MACHINE
+
+1. **Execution Trace**: When executing a smart contract( a digital agreement signed and stored on a blockchain network, which executes automatically when the contract's terms and conditions (T&C) are satisfied) written in Cairo, the VM generates an execution trace. This trace contains information about the sequence of instructions executed, the values of variables at different points, and the instructions or function calls of an important program that are executed or evaluated.
+
+2. **Hinting Mechanism**: Cairo VM gives a procedure for developers to provide hints to the verification tool. These hints can come in various forms, such as assertions, assumptions, or annotations within the Cairo code.
+
+3. **Integration with Verification Tools**: Cairo VM integrates with external verification tools that analyze the execution traces and verify the features of the smart contracts. These tools can include assumptions provers, model checkers, or symbolic execution engines.
+
+4. **Guiding Verification with Hints**: During the verification process, the hints provided by developers serve as guides for analysis performed by the verification tools.
+
+For example:
+ - **Assertion Checking**: Developers or testers use specific statements, known as assertions, to validate the expected   behavior of a program or system. Verification tools check whether these assertions fail during the analysis.
+
+ - **Invariant Detection**: Hints may guide the tool to identify the uniformity of loop iteration or other program properties responsible for the accuracy of the contract. The tool then attempts to prove these properties using the execution trace.
+
+ - **Path Exploration**: Hints can help the tools explore specific paths or branches of the program that are considered fit for verification. It helps in focusing the analysis on relevant parts of the code.
+
+
+5. **Feedback Loop**: As the verification tool analyzes the execution trace and attempts to prove properties guided by the hints, it may encounter challenges or limitations. In such cases, feedback mechanisms allow developers to refine their hints or modify the code to improve the chances of successful verification.


This seems awfully generic, and untrue

rodrigo-pino · 2024-05-08T10:33:44Z

docs/docs/vm-fundamentals/hints.md

+
+Sequencers in Cairo are responsible for organizing the execution of transactions, managing instruction ordering and dependencies, exploiting multiple processors, and ensuring the integrity of the program's state throughout the execution process.   
+
+Provers attempt to mathematically prove the correctness of a program concerning a given specification. The prover uses these hints to access the program's behavior and verify that it satisfies specified properties and constraints. In this context, hints could guide the prover towards particular properties or parts of the codebase that are relevant to the proof.


Could you tell me what source you have? I don't think this to be correct

rodrigo-pino · 2024-05-08T10:35:07Z

docs/docs/vm-fundamentals/hints.md

+Sequencers in Cairo are responsible for organizing the execution of transactions, managing instruction ordering and dependencies, exploiting multiple processors, and ensuring the integrity of the program's state throughout the execution process.   
+


This seems awfully generic. Sequencers are the actors that produces blocks by executing transaction and updating the blockchain state. Everything else seems overly ambiguous to be of any use.

… hint_examples_docs

rodrigo-pino · 2024-05-10T09:42:36Z

Hey @Iwueseiter how is it going, let me know if I can help with anything

Iwueseiter · 2024-05-10T10:27:19Z

Hey @Iwueseiter how is it going, let me know if I can help with anything

I pushed some commits to the PR, you can look at it and leave a review.

rodrigo-pino · 2024-05-12T17:58:33Z

docs/docs/vm-fundamentals/hints.md

+
+### WHY HINTS RUN ON SEQUENCERS/ PROVERS AND NOT VERIFIERS
+
+The verifier in Cairo is responsible for ensuring that a program attaches safety and accuracy features. It checks that the program satisfies limitations such as memory safety, type safety, and functional correctness.


This is not true, the verifier doesn't do this. Please, let us not put anything which is not right. As a rule of a thumb if you don't know about it then don't write it. Let's discuss first if it is true or not. We have community calls every Wednesday if you want to pop in and ask all questions you might have.

rodrigo-pino · 2024-05-12T18:07:47Z

docs/docs/vm-fundamentals/hints.md

+Hints in Cairo are pieces of Python code only executed by the sequencer and are not included in the bytecode. They instruct the prover on how to handle nondeterministic instructions. These nondeterministic instructions are programs that have different outcomes at execution.   
+Hints are guides that developers can provide to the Cairo virtual machine to optimize execution or provide additional information about the program. These hints help improve performance or help the VM make better decisions during the execution of programs. 


This part is partially correct, I understand is a complex subject and that you want to explain the "why" of the hints. Let's reduce this paragraph to something simpler: "Hints are used to help the Virtual Machine determine the next path of execution it should take"

rodrigo-pino · 2024-05-12T18:10:47Z

docs/docs/vm-fundamentals/hints.md

+Example:
+The *'random'* instruction generates a random number, which can be different each time of instruction execution. The verifier cannot implement these instructions, as it would require access to nondeterministic information, which would beat the purpose of the zero-knowledge proof.


I don't think this random instruction exists

rodrigo-pino · 2024-05-12T18:12:48Z

docs/package-lock.json

Regarding this file, it should be actually included. It was so different from the old one that I thought it was a miss addition. This begs the question why did it changed so much

rodrigo-pino · 2024-05-12T18:13:07Z

docs/package.json

@@ -18,6 +18,7 @@
    "@docusaurus/preset-classic": "2.4.1",
    "@mdx-js/react": "^1.6.22",
    "clsx": "^1.2.1",
+    "docusaurus": "^1.14.7",


I don't understand why do you added this extra dependency here? This must be the reason why the lockfile is very different.

I didn't add up any dependency separately, I installed docusaurus. And that should be why they are differences.

Iwueseiter added 3 commits April 29, 2024 18:15

chore: implement hints docs

1b0181a

Merge branch 'main' of https://github.com/Iwueseiter/cairo-vm-go into…

ff502a6

… hint_examples_docs

fix: resolve conflict with base branch

185d0b8

cicr99 reviewed May 3, 2024

View reviewed changes

Iwueseiter added 8 commits May 3, 2024 17:32

fix Effected required chsnges

e464724

fix: format with markdown

717f14a

Merge branch 'main' of https://github.com/Iwueseiter/cairo-vm-go into…

64bdf7e

… hint_examples_docs

fix: format with markdown

659b0c2

fix: add more markdown formatter

a662c93

Merge branch 'main' of https://github.com/Iwueseiter/cairo-vm-go into…

ecad69c

… hint_examples_docs

fix: add more markdown formatter

9768dda

implementing hints in Cairo VM

8d60a57

rodrigo-pino reviewed May 8, 2024

View reviewed changes

Iwueseiter added 3 commits May 8, 2024 17:09

Merge branch 'main' of https://github.com/Iwueseiter/cairo-vm-go into…

e22e40a

… hint_examples_docs

fix: refactor hint docs

952696f

fix: remove package-lock.json

3659651

rodrigo-pino reviewed May 12, 2024

View reviewed changes

Iwueseiter closed this by deleting the head repository May 13, 2024

rodrigo-pino mentioned this pull request May 14, 2024

Docs: hints docs #409

Closed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Implement hints documentation #378

Implement hints documentation #378

Iwueseiter commented Apr 29, 2024

cicr99 May 3, 2024

rodrigo-pino May 8, 2024

rodrigo-pino May 8, 2024

rodrigo-pino May 8, 2024

rodrigo-pino May 8, 2024

rodrigo-pino May 8, 2024

rodrigo-pino May 8, 2024

rodrigo-pino May 8, 2024

rodrigo-pino May 8, 2024

rodrigo-pino May 8, 2024

rodrigo-pino May 8, 2024

rodrigo-pino commented May 10, 2024

Iwueseiter commented May 10, 2024

rodrigo-pino May 12, 2024

rodrigo-pino May 12, 2024

rodrigo-pino May 12, 2024

rodrigo-pino May 12, 2024

rodrigo-pino May 12, 2024

Iwueseiter May 13, 2024

		Sequencers and provers are tools used in formal verification, a process of accurately proving the correctness of programs.
		Applying hints in the Cario virtual machine leverages the execution trace and uses it to guide the verification process. Integration of hints with the Cairo VM's execution trace and verification tools enables developers to guide and customize the verification process, improving the efficiency and effectiveness of formal verification for smart contracts.

		### MEMORY HINTS
		These hints are memory aids that provide additional information to the prover on computing values in the Cairo program. They are functional when provers can't handle certain expressions implicitly.


		Sequencers in Cairo are responsible for organizing the execution of transactions, managing instruction ordering and dependencies, exploiting multiple processors, and ensuring the integrity of the program's state throughout the execution process.

		Provers attempt to mathematically prove the correctness of a program concerning a given specification. The prover uses these hints to access the program's behavior and verify that it satisfies specified properties and constraints. In this context, hints could guide the prover towards particular properties or parts of the codebase that are relevant to the proof.


		### WHY HINTS RUN ON SEQUENCERS/ PROVERS AND NOT VERIFIERS

		The verifier in Cairo is responsible for ensuring that a program attaches safety and accuracy features. It checks that the program satisfies limitations such as memory safety, type safety, and functional correctness.

		Hints in Cairo are pieces of Python code only executed by the sequencer and are not included in the bytecode. They instruct the prover on how to handle nondeterministic instructions. These nondeterministic instructions are programs that have different outcomes at execution.
		Hints are guides that developers can provide to the Cairo virtual machine to optimize execution or provide additional information about the program. These hints help improve performance or help the VM make better decisions during the execution of programs.

		Example:
		The 'random' instruction generates a random number, which can be different each time of instruction execution. The verifier cannot implement these instructions, as it would require access to nondeterministic information, which would beat the purpose of the zero-knowledge proof.

Implement hints documentation #378

Implement hints documentation #378

Conversation

Iwueseiter commented Apr 29, 2024

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

rodrigo-pino commented May 10, 2024

Iwueseiter commented May 10, 2024

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment