소개
첫 번째 레벨 제목
소개
Tinyram은 바이트 주소 지정이 가능한 랜덤 액세스 메모리와 입력 테이프가 있는 간단한 RISC 랜덤 액세스 시스템입니다. TinyRAM에는 두 가지 변형이 있습니다. 하나는 Harvard 아키텍처를 따르는 것이고 다른 하나는 von Neumann 아키텍처를 따르는 것입니다(이 기사에서는 주로 von Neumann 아키텍처에 대해 설명합니다).
SCIPR(Concise Computational Integrity and Privacy Research) 프로젝트는 TinyRAM 프로그램의 올바른 실행을 증명하기 위한 메커니즘을 구축했으며 TinyRAM은 이 경우 효율적으로 설계되었습니다. 그것은 "충분히 표현적이다"와 "충분히 단순하다"의 반대말 사이의 균형을 이룬다:
• 고급 프로그래밍 언어에서 컴파일할 때 짧고 효율적인 어셈블리 코드를 지원하는 충분한 표현력.TinyRam 소개
TinyRam 소개
첫 번째 레벨 제목
Tinyram 명령어 세트
Tinyram에는 총 29개의 명령어가 있으며 각 명령어는 opcode와 최대 3개의 피연산자로 구성됩니다. 피연산자는 레지스터의 이름(0과 K-1 사이의 정수) 또는 즉치 값(W 비트의 문자열)일 수 있습니다. 달리 지정하지 않는 한 명령어는 플래그를 개별적으로 수정하지 않습니다. vnTinyram i= 2W/8인 경우 각 명령어는 기본적으로 i(i % 2^W)만큼 pc를 증가시킵니다.
일반적으로 첫 번째 피연산자는 명령 계산을 위한 대상 레지스터이고 다른 피연산자는 명령에 필요한 매개변수를 지정하며 마지막으로 모든 명령을 실행하려면 기계의 한 사이클이 필요합니다.
비트 조작
정수 연산
• shl이들은 다양한 무부호 및 부호 정수 연산입니다. 각각의 경우에 플래그는 산술 오버플로 또는 오류(예: 0으로 나누기)가 발생하면 1로 설정되고 그렇지 않으면 0으로 설정됩니다.
• shr교대조작
명령어 shl ri rj A는 [rj]를 [A]u 비트만큼 왼쪽으로 이동하여 얻은 W 비트 문자열을 ri 레지스터에 저장합니다. 이동 후 빈 위치는 0으로 채워집니다. 또한 플래그는 [rj]의 최상위 비트로 설정됩니다.
명령 shr ri rj A는 [rj]를 [A]u 비트만큼 오른쪽으로 이동하여 얻은 W 비트 문자열을 ri 레지스터에 저장합니다. 이동 후 빈 위치는 0으로 채워집니다. 또한 플래그는 [rj]의 최하위 비트로 설정됩니다.
비교 연산
• mov비교 연산의 각 명령어는 레지스터를 수정하지 않으며 비교 결과는 플래그에 저장됩니다.
• cmov이동 작업
명령 mov ri A는 [A]를 ri 레지스터에 저장합니다.
명령 cmov ri A 플래그 = 1이면 [A]를 ri 레지스터에 저장합니다. 그렇지 않으면 ri 레지스터의 값이 변경되지 않습니다.
• jmp점프 동작
• cjmp이러한 점프 및 조건부 점프 명령어는 레지스터와 플래그를 수정하지 않고 pc를 수정합니다.
• cnjmp 명령어 jmp A는 [A]를 pc에 저장합니다.
명령 cjmp A는 플래그 = 1의 조건 하에서 pc에 [A]를 저장하고, 그렇지 않으면 pc는 1씩 증가합니다.
명령 cnjmp A는 flag = 0의 조건 하에서 pc에 [A]를 저장하고, 그렇지 않으면 pc는 1씩 증가합니다.
메모리 작업
이것은 단순한 메모리 로드 및 저장 작업으로, 메모리 주소는 즉치 값이나 레지스터의 내용에 의해 결정됩니다. 이것은 tinyram의 유일한 주소 지정 모드입니다. (tinyram은 일반적인 "base+offset" 주소 지정 모드를 지원하지 않습니다).
입력 작업
출력 작업
이 명령은 프로그램이 계산을 마쳤으므로 더 이상 작업이 허용되지 않음을 나타냅니다.
첫 번째 레벨 제목
명령어 세트 제약
Tinyram은 회로 제약에 R1CS 제약 형식을 사용하며 구체적인 형식은 다음과 같습니다.
R1CS 제약 조건은 a, b 및 c의 세 가지 linear_combination 표현을 가질 수 있습니다. R1CS 시스템의 모든 변수 할당은 기본 입력과 보조 입력의 두 부분으로 나눌 수 있습니다. 기본은 우리가 종종 "진술서"라고 부르는 것입니다. 보조는 "증인"입니다.
R1CS 제약 시스템에는 여러 R1CS 제약이 포함되어 있습니다. 각 제약 조건의 벡터 길이는 고정되어 있습니다(기본 입력 크기 + 보조 입력 크기 + 1).
• andTinyram은 libsnark의 코드 구현에서 많은 사용자 정의 장치를 사용하여 vm의 제약 조건과 opcode 실행 및 메모리의 제약 조건을 표현합니다. 특정 코드는 gadgetslib1/gadgets/cpu_checkers/tinyram 폴더에 있습니다.
비트 조작 제약
구속 공식:
R1CS는 파라미터 1과 파라미터 2의 제약 조건을 확인하고 곱셈 계산을 위해 비트 단위로 계산 결과를 확인합니다. 제약 조건 단계는 다음과 같습니다.
1. 계산 프로세스 제약 조건, 코드는 다음과 같습니다.
2. 결과 인코딩 제약
• or3. 계산 결과가 모두 0 제약 조건이 아닙니다(명령의 정의와 일관성 유지, 이 프로세스는 주로 제약 조건 플래그를 준비하는 것입니다).
4.플래그 제약
구속 공식:
구체적인 제약 단계는 다음과 같습니다.
1. 계산 프로세스 제약 조건, 코드는 다음과 같습니다.
2. 결과 코딩 제약 조건(위와 동일)
• xor3. 계산 결과가 모두 0개의 제약 조건이 아님(명령어의 정의와 일치하도록 유지, 이 프로세스는 주로 제약 조건 플래그를 준비하는 것임)(위와 동일)
4.플래그 제약(위와 동일)
구속 공식:
구체적인 제약 단계는 다음과 같습니다.
•not1. 계산 프로세스 제약 조건, 코드는 다음과 같습니다.
2, 3, 4단계 위와 동일
구속 공식:
구체적인 제약 단계는 다음과 같습니다.
•add2, 3, 4단계 위와 동일
정수 조작 제약
: 구속조건 공식:
구체적인 제약 단계는 다음과 같습니다.
1. 계산 프로세스 제약 조건, 코드는 다음과 같습니다.
•sub2. 디코딩 결과 제약 조건 및 부울 제약 조건
3. 코딩 결과 제약
: 구속조건 공식:
sub 제약 조건은 add보다 조금 더 복잡합니다. 중간 변수를 사용하여 a - b의 결과를 나타냅니다. 동시에 결과 계산이 다음과 같은 형태로 표현되도록 결과에 2^w를 더합니다. 양의 정수 및 기호. 구체적인 제약 단계는 다음과 같습니다.
1. 계산 프로세스 제약
•mull 、umulh、smulh2. 디코딩 결과 제약 조건 및 부울 제약 조건
3. 부호 비트 제약
구속 공식:
Mull 관련 제약 조건에는 다음 단계가 포함됩니다.
1. 곱셈 제약 조건 계산
•udiv 、umod2. 계산 결과 코딩 제약
구속 공식:
B는 제수, q는 몫, r은 나머지입니다. 나머지 합계는 제수를 초과할 수 없다는 조건을 충족해야 합니다. 특정 제약 조건 코드는 다음과 같습니다.
• shl、shr보조 제목
시프트 작업 제약
제약 공식cmpe、 cmpa 、cmpae、cmpg、cmpge비교 연산
. 비교 명령은 부호 있는 숫자의 비교와 부호 없는 숫자의 비교라는 두 가지 범주로 나눌 수 있습니다.두 가지 제약 프로세스의 핵심은 libsnark에 구현된 Comparison_gadget을 사용합니다.
나머지 절차는 부호 있는 비교 제약 조건과 동일합니다.
• mov보조 제목
이동 작업 제약
• cmov구속 공식:
구속 공식:
cmov의 제약 조건은 mov보다 더 복잡합니다. mov의 주요 동작은 플래그 값의 변경과 관련이 있습니다. 동시에 cmov는 플래그를 수정하지 않으므로 제약 조건은 플래그 값이 변경되지 않습니다. cmov의 코드는 다음과 같습니다.
보조 제목
• jmp
점프 작업 제약
• cjmp
이러한 점프 및 조건부 점프 명령어는 레지스터와 플래그를 수정하지 않고 pc를 수정합니다.
Jmp 연산은 명령 실행 결과와 일치하도록 pc 값을 제한합니다. 구체적인 제한 코드는 다음과 같습니다.
cjmp는 플래그 조건에 따라 점프합니다. 플래그 = 1이면 점프합니다. 그렇지 않으면 pc가 1씩 증가합니다.
• cnjmp
구속 공식은 다음과 같습니다.
제약 코드는 다음과 같습니다.
cnjmp는 플래그 조건에 따라 점프합니다. 플래그 = 0이면 점프합니다. 그렇지 않으면 pc가 1씩 증가합니다.
구속 공식은 다음과 같습니다.
메모리 작업 제약
• store.b 그리고 store.w
이는 단순한 메모리 로드 및 저장 작업으로, 메모리 주소는 즉치값 또는 레지스터의 내용에 의해 결정됩니다. 이것은 tinyram의 유일한 주소 지정 모드입니다. (tinyram은 일반적인 "base+offset" 주소 지정 모드를 지원하지 않습니다).
그리고
store.w의 경우 전체 arg1val의 값을 가져오고 store.b의 경우 opcode는 arg1val의 필요한 부분(예: 마지막 바이트)만 가져옵니다.제약 코드는 다음과 같습니다.
• load.b 및 load.w
• read
이 두 명령어에 대해 메모리에서 로드해야 하는 콘텐츠는 instruction_results에 저장됩니다. 제약 코드는 다음과 같습니다.
입력 운영 제약
읽기 작업은 테이프와 관련이 있으며 특정 제약 규칙은 다음과 같습니다.
1. 이전 테이프의 내용을 읽었으며 읽을 내용이 없으며 다음 테이프를 읽지 않습니다.
2. 이전 테이프의 내용을 읽었으며 읽을 내용이 없으며 플래그가 1로 설정됩니다.
3. 현재 실행중인 명령을 읽으면 읽은 내용이 테이프의 입력 내용과 일치합니다.
5. 결과가 0이 아닌 경우 플래그가 0임을 의미합니다.
제약 코드:
보조 제목
• answer
출력 작업 제약
프로그램의 출력 값이 수락되면 has_accepted가 1로 설정되고 프로그램의 반환 값이 정상적으로 수락될 수 있다는 것은 현재 명령이 응답이고 arg2 값이 0이라는 것을 의미합니다.
다른
제약 코드는 다음과 같습니다.
위 그림의 예에서 vnTinyram + zk-SNARKs를 사용하여 모든 EVM 작업을 검증하는 것은 불가능하며 소수의 명령어에 대한 계산 검증 검증에만 적합하다는 결론을 내릴 수 있습니다. EVM의 일부 계산 유형의 opcode를 확인합니다.
회사 소개
첫 번째 레벨 제목
회사 소개
GitHub | Twitter | Telegram | Medium| Mirror | HackMD | HackerNoon
IOS
Android