A. 열 네번째 빝데브(Bitdev Socratic Seminar) 회고 - P 참여자님의 핵심 크리틱 중심 요약


	1. 비교 렌즈로 보는 시도는 흥미롭지만 vote라는 단어를 전자투표 프로토콜과 섞어 쓸때 비트코인 구현 내용 정의, 논리적 전개가 부족하면 엄밀성이 무너짐. 

	   즉, 동일성 주장(identity claim) 하지 않을것을 확실하게 해야.  Bitcoin의 representation 문제와 voting의 representation 문제 비교 분석 목적임을 명시했어야.

           실제 진행되는 BIP110 기반 vote, signaling, consensus, validation, finality는 엄밀히 구분하여 전자투표 시스템의 컨텍스트 프리 상태에서 바라봐야


        2. 블록체인 기반 전자투표 시스템을 언급하며 조사/분석 하는 목적(bitdev socratic seminar 에서 다룰 범위 명시)은 새로 설계하려는 것이 아니라, 

	   투표시스템의 암호학적 핵심 성질을 이해하고 백서 4장의 vote 표현에 관한 해석과 PoW 시스템에 대입하며 비트코인 구현 메커니즘 이해도를 높이는 것 


        3. 비트코인 전체 시스템, 특히 PoW의 경제적 안전성·탈중앙성·사회적 합의까지 포함한 성질은 전자투표 프로토콜처럼 닫힌 수학적 모델로 형식검증은 불가능하고 증명되었다 ?

           비트코인 전체 시스템의 경제적 안전성·탈중앙성·사회적 합의까지 포함한 성질을 완전하게 형식검증할 수 없음과 그 증명에 대한 존재 언급

           다만 이것이 수학적으로 불가능함이 증명된 것인지, 혹은 현실적으로 모델링이 불가능한 것인지는 추가 확인이 필요.



         >> '형식검증 불가능성'은 '구현체 수준 | 합의 프로토콜 수준  | 경제적 인센티브 수준 | 사회적 합의 수준' 중 어느 계층을 의미하는지 필요. (증명가능 혹은 증명 불가능성 판단은 보류하는게)

         >> Bitcoin 에서 동작하는 Proof of Work 가 Nash equilibrium 의 수학적 모델을 추종하고 구현한 상태라는것을 어떤 근거로 주장할 수 있는지 엄밀하게 접근해야할 필요있음
						
         >> 내가 취하고자 하는 핵심 스탠스는 PoW·UTXO·BIP activation·finality 같은 구현 동작을 상태기계와 명세 관점에서 분해하는 시도하겠다는것

	    즉, 비트코인 전체의 형식검증의 불가능성이 증명되었다 하더라도, UTXO 상태 전이·BIP. 활성화·서명 검증 같은 결국 검증가능한 상태로 명세화 부분 형식검증화가 

	        기술적 탈중앙화 연구 관점에서 매우 중요하다고 판단. 부분 명세화는 가능하다는 관점에서 구현체 매커니즘의 수학적 정의 시도예정.

	

    B.  연구 노트 a - 열 다섯번째 빝데브 준비하며 질문 리스트 정리


	Q1. 비트코인의 Fomal verification 증명 불가능성이 증명되었나 ? 

	Q2. 만약 그렇다면, 비트코인 구현을 중심으로 공리화 하면서 닫힌계로 잘못 가정했기 때이문이 아닐까? 

	Q3. 만약 열린계로 가정하면 증명 가능한가? 

	Q4. 비트코인 구현의 공리화 연구의 현재는 어디까지왔나 ? 

	Q5. 분산시스템 주류 연구 관점에서 비트코인 컨센서스를 분석할 수 있는 효과적인 이론, 메서드, 툴은?

	Q6. OP_RETUEN 논쟁을 3문단 요약하면 ? 

	Q7. OP_RETURN 구현 디테일을 분석한다면 고려해야할 내용들은 ?
						


    C.  연구 노트 b - 스케치 노트

		
	- 비트코인 구현 공리화 연구 기초단계에서 조사, 정리해야할 기본을 요약해보면

              * ECDSA/Schnorr의 수학적 성질


              * Script System 성질


              * UTXO state transition

     
              * consensus rules

              * BIP 8,9 based Activation rule and state transition


	>>  Ideation 부분 형식화와 검증은 가능하지 않을까? 부분 형식화를 시도하기전에 공리화 과정에서 논리적 오류와 결점은 어떤 방법으로 사전에 검증 할 수 있는가?


	>>  예를들어, 유한체/실수체 정의부 : 유한체와 실수체를 같다고 하면 안됨. 수학적으로 엄밀하게 다른거임.

	              실수체는 연속성, 극한, 거리, 완비성의 성질을 가지고 있고 유한체는 모듈러 연산, 역원, 유한순환군, 이산적 대수 구조의 성질로 구성됨 엄밀하게 다른 체계임.

		      이 내용은 비트코인의 이해의 일반적 인식의오류를 만드는 원인이 타원곡선을 실수체 위에서 그리는 교육용 목적의 직관 설명이 있는데, 

                      비트코인의 secp256k1은 실제로는 유한체 위의 대수적 점 연산 임을 구분해야.

		fact : 실수체 위의 타원곡선 그림은 기하학적 직관을 제공하지만, ECDSA/Schnorr의 실제 계산은 유한체 위의 대수적 구조에서 수행된다.



    D. Wrap It Up


	- 비트코인을 형식적으로 다루려면 명세와 검증 가능성을 분리하고 부분 형식 검증 가능성을 중심으로한 정의 기반 접근이 필요

	- 비트코인 전체의 사회기술적 안전성은 완전 검증 불가능성에 관한 접근에 관한 의심은 지속되어야.