nx_uv_precision_witness_t280.nx source
↩ module page · 32 lines · 3712 B
1import "nx_nxa_corner_checkpoint_candidate_t280.nx"
2import "nx_uv_gram_solver_candidate_t280.nx"
3import "nx_gate_verdict.nx"
4const UP_HEADER:i64=32
5const UP_ROW:i64=10
6const UP_TRIROW:i64=9
7func up_num(s:*u8)->i64{var n:i64=0;var i:i64=0;if s[0]==(0 as u8){return 0-1};while s[i]!=(0 as u8){let d:i64=(s[i] as i64)-48;if d<0{return 0-1};if d>9{return 0-1};if n>(NCP_MAX-d)/10{return 0-1};n=n*10+d;i=i+1};return n}
8func up_time(clock:*i64)->i64{sys_clock_gettime_mono(clock);return clock[0]*1000000+clock[1]/1000}
9func main(argc:i64,argv:*i64)->i64{
10 if argc!=7{return 2};let chart:i64=up_num(argv[4] as *u8);let budget:i64=up_num(argv[5] as *u8);let denominator:i64=up_num(argv[6] as *u8);if chart<0{return 2};if budget<1{return 2};if denominator<2{return 2}
11 let lens:*i64=sys_mmap_try(16) as *i64;let clock:*i64=sys_mmap_try(16) as *i64;if (lens as i64)<=0{return 3};if (clock as i64)<=0{return 3}
12 let src:*u8=sys_read_file(argv[1] as *u8,lens);if src==(0 as *u8){return 3};let bytes:i64=lens[0]
13 let checkpoint:*u8=sys_read_file(argv[2] as *u8,lens);if checkpoint==(0 as *u8){return 3}
14 let m:*i64=ncp_restore_topology(src,bytes,checkpoint,lens[0]);if m==(0 as *i64){return 4};if chart>=uv_chart_count(m){ncp_model_free(m);return 2}
15 let start:i64=up_time(clock);let s:*UvGramSolve=uls_begin(m,chart,1.0/__f64_from_i64(denominator));if s==(0 as *UvGramSolve){return 5};let setup:i64=up_time(clock)-start
16 var rc:i64=s.result;let begin:i64=up_time(clock);if rc==UV_E_NOTRUN{rc=uls_step(s,budget)};let elapsed:i64=up_time(clock)-begin
17 gv_puts("PRECISION chart=");gv_num(chart);gv_puts(" faces=");gv_num(s.nt);gv_puts(" iterations=");gv_num(s.iterations);gv_puts(" solveUs=");gv_num(elapsed);gv_puts(" result=");gv_num(rc);gv_puts("\n")
18 if rc!=UV_OK{uls_free(s);ncp_model_free(m);return 6}
19 let words:i64=UP_HEADER+s.n*UP_ROW+s.nt*UP_TRIROW;let p:*i64=sys_mmap_try(words*8) as *i64;if (p as i64)<=0{return 3}
20 p[0]=0x3151434e;p[1]=1;p[2]=UP_HEADER;p[3]=UP_ROW;p[4]=UP_TRIROW;p[5]=s.n;p[6]=s.nt;p[7]=chart;p[8]=bytes;p[9]=words;p[10]=rc;p[11]=s.iterations;p[12]=s.matvecs;p[13]=setup;p[14]=elapsed;p[15]=UV_PIN_SPAN;p[16]=UV_Q16;p[18]=m[UV_H_NV];p[19]=m[UV_H_NT];p[20]=s.storageBytes;p[21]=uv_words_used(m)*8;p[22]=uv_seam_count(m);p[23]=uv_chart_count(m);p[24]=denominator;p[25]=budget;p[26]=words*8
21 if sha256_digest_checked_native(src,bytes,((p as i64)+28*8) as *u8)!=0{return 7}
22 let raw:*i64=s.x as *i64;var i:i64=0;while i<s.n{
23 let o:i64=UP_HEADER+i*UP_ROW;let sv:i64=m[m[UV_O_UVSRC]+s.classes[i]];p[o]=sv;p[o+1]=uv_vx(m,sv);p[o+2]=uv_vy(m,sv);p[o+3]=uv_vz(m,sv);p[o+4]=raw[i];p[o+5]=raw[s.n+i];i=i+1
24 }
25 if uls_export(s)!=UV_OK{return 8};i=0;while i<s.n{let o:i64=UP_HEADER+i*UP_ROW;let cls:i64=s.classes[i];p[o+6]=m[m[UV_O_WU]+cls];p[o+7]=m[m[UV_O_WV]+cls];i=i+1}
26 if uvi_atlas(m)!=UV_OK{return 9};p[17]=uv_grid(m)
27 i=0;while i<s.n{let o:i64=UP_HEADER+i*UP_ROW;let cls:i64=s.classes[i];p[o+8]=m[m[UV_O_WU]+cls];p[o+9]=m[m[UV_O_WV]+cls];i=i+1}
28 let first:i64=m[m[UV_O_CSTART]+chart];var t:i64=0;while t<s.nt{let sourceTri:i64=m[m[UV_O_CORDER]+first+t];var k:i64=0;while k<3{let o:i64=UP_HEADER+s.n*UP_ROW+t*UP_TRIROW+k*3;p[o]=sourceTri;p[o+1]=k;p[o+2]=s.corners[t*3+k];k=k+1};t=t+1}
29 let fd:i64=sys_openat_exclusive(argv[3] as *u8,MODE_0600);if fd<0{return 10};var written:i64=0;while written<words*8{let n:i64=sys_write(fd,((p as i64)+written) as *u8,words*8-written);if n<=0{return 11};written=written+n};sys_close(fd)
30 gv_puts("PRECISION source indexed raw/work/atlas packet bytes=");gv_num(words*8);gv_puts(" grid=");gv_num(uv_grid(m));gv_puts("\n")
31 sys_munmap_direct(p as *u8,words*8);uls_free(s);ncp_model_free(m);sys_munmap_direct(lens as *u8,16);sys_munmap_direct(clock as *u8,16);return 0
32}