def bits.bound_va
bend-osdev-caps@0.1.0.0 · PROOF.bend:360
import bend-osdev-caps@0.1.0.0/PROOF.bend as PROOF
import Base
import bend-osdev-caps@0.1.0.0/caps.bend as C
360def bits.bound_va(+n: Nat, +i: Word(n), +fi: Word(n), +fp: Word(n), +b: Word(n), +a: Word(n)) -> {C.CapBits.subset(n, a, i) == True{} : Bool} -> {C.CapBits.subset(n, Word.or(n, Word.or(n, Word.and(n, i, fi), Word.and(n, fp, b)), a), Word.or(n, b, i)) == True{} : Bool}:
361 match n:
362 case 0n:
363 h0 => {==}
364 case 1n+n1:
365 match i fi fp b a:
366 case WCon{True{}, +it} WCon{True{}, +fit} WCon{True{}, +fpt} WCon{True{}, +bt} WCon{True{}, +at}:
367 h0 => bits.bound_va(n1, it, fit, fpt, bt, at)(h0)
368 case WCon{True{}, +it} WCon{True{}, +fit} WCon{True{}, +fpt} WCon{True{}, +bt} WCon{False{}, +at}:
369 h0 => bits.bound_va(n1, it, fit, fpt, bt, at)(h0)
370 case WCon{True{}, +it} WCon{True{}, +fit} WCon{True{}, +fpt} WCon{False{}, +bt} WCon{True{}, +at}:
371 h0 => bits.bound_va(n1, it, fit, fpt, bt, at)(h0)
372 case WCon{True{}, +it} WCon{True{}, +fit} WCon{True{}, +fpt} WCon{False{}, +bt} WCon{False{}, +at}:
373 h0 => bits.bound_va(n1, it, fit, fpt, bt, at)(h0)
374 case WCon{True{}, +it} WCon{True{}, +fit} WCon{False{}, +fpt} WCon{True{}, +bt} WCon{True{}, +at}:
375 h0 => bits.bound_va(n1, it, fit, fpt, bt, at)(h0)
376 case WCon{True{}, +it} WCon{True{}, +fit} WCon{False{}, +fpt} WCon{True{}, +bt} WCon{False{}, +at}:
377 h0 => bits.bound_va(n1, it, fit, fpt, bt, at)(h0)
378 case WCon{True{}, +it} WCon{True{}, +fit} WCon{False{}, +fpt} WCon{False{}, +bt} WCon{True{}, +at}:
379 h0 => bits.bound_va(n1, it, fit, fpt, bt, at)(h0)
380 case WCon{True{}, +it} WCon{True{}, +fit} WCon{False{}, +fpt} WCon{False{}, +bt} WCon{False{}, +at}:
381 h0 => bits.bound_va(n1, it, fit, fpt, bt, at)(h0)
382 case WCon{True{}, +it} WCon{False{}, +fit} WCon{True{}, +fpt} WCon{True{}, +bt} WCon{True{}, +at}:
383 h0 => bits.bound_va(n1, it, fit, fpt, bt, at)(h0)
384 case WCon{True{}, +it} WCon{False{}, +fit} WCon{True{}, +fpt} WCon{True{}, +bt} WCon{False{}, +at}:
385 h0 => bits.bound_va(n1, it, fit, fpt, bt, at)(h0)
386 case WCon{True{}, +it} WCon{False{}, +fit} WCon{True{}, +fpt} WCon{False{}, +bt} WCon{True{}, +at}:
387 h0 => bits.bound_va(n1, it, fit, fpt, bt, at)(h0)
388 case WCon{True{}, +it} WCon{False{}, +fit} WCon{True{}, +fpt} WCon{False{}, +bt} WCon{False{}, +at}:
389 h0 => bits.bound_va(n1, it, fit, fpt, bt, at)(h0)
390 case WCon{True{}, +it} WCon{False{}, +fit} WCon{False{}, +fpt} WCon{True{}, +bt} WCon{True{}, +at}:
391 h0 => bits.bound_va(n1, it, fit, fpt, bt, at)(h0)
392 case WCon{True{}, +it} WCon{False{}, +fit} WCon{False{}, +fpt} WCon{True{}, +bt} WCon{False{}, +at}:
393 h0 => bits.bound_va(n1, it, fit, fpt, bt, at)(h0)
394 case WCon{True{}, +it} WCon{False{}, +fit} WCon{False{}, +fpt} WCon{False{}, +bt} WCon{True{}, +at}:
395 h0 => bits.bound_va(n1, it, fit, fpt, bt, at)(h0)
396 case WCon{True{}, +it} WCon{False{}, +fit} WCon{False{}, +fpt} WCon{False{}, +bt} WCon{False{}, +at}:
397 h0 => bits.bound_va(n1, it, fit, fpt, bt, at)(h0)
398 case WCon{False{}, +it} WCon{True{}, +fit} WCon{True{}, +fpt} WCon{True{}, +bt} WCon{True{}, +at}:
399 h0 => bits.absurd(C.CapBits.subset(1n+n1, Word.or(1n+n1, Word.or(1n+n1, Word.and(1n+n1, WCon{False{}, it}, WCon{True{}, fit}), Word.and(1n+n1, WCon{True{}, fpt}, WCon{True{}, bt})), WCon{True{}, at}), Word.or(1n+n1, WCon{True{}, bt}, WCon{False{}, it})), h0)
400 case WCon{False{}, +it} WCon{True{}, +fit} WCon{True{}, +fpt} WCon{True{}, +bt} WCon{False{}, +at}:
401 h0 => bits.bound_va(n1, it, fit, fpt, bt, at)(h0)
402 case WCon{False{}, +it} WCon{True{}, +fit} WCon{True{}, +fpt} WCon{False{}, +bt} WCon{True{}, +at}:
403 h0 => bits.absurd(C.CapBits.subset(1n+n1, Word.or(1n+n1, Word.or(1n+n1, Word.and(1n+n1, WCon{False{}, it}, WCon{True{}, fit}), Word.and(1n+n1, WCon{True{}, fpt}, WCon{False{}, bt})), WCon{True{}, at}), Word.or(1n+n1, WCon{False{}, bt}, WCon{False{}, it})), h0)
404 case WCon{False{}, +it} WCon{True{}, +fit} WCon{True{}, +fpt} WCon{False{}, +bt} WCon{False{}, +at}:
405 h0 => bits.bound_va(n1, it, fit, fpt, bt, at)(h0)
406 case WCon{False{}, +it} WCon{True{}, +fit} WCon{False{}, +fpt} WCon{True{}, +bt} WCon{True{}, +at}:
407 h0 => bits.absurd(C.CapBits.subset(1n+n1, Word.or(1n+n1, Word.or(1n+n1, Word.and(1n+n1, WCon{False{}, it}, WCon{True{}, fit}), Word.and(1n+n1, WCon{False{}, fpt}, WCon{True{}, bt})), WCon{True{}, at}), Word.or(1n+n1, WCon{True{}, bt}, WCon{False{}, it})), h0)
408 case WCon{False{}, +it} WCon{True{}, +fit} WCon{False{}, +fpt} WCon{True{}, +bt} WCon{False{}, +at}:
409 h0 => bits.bound_va(n1, it, fit, fpt, bt, at)(h0)
410 case WCon{False{}, +it} WCon{True{}, +fit} WCon{False{}, +fpt} WCon{False{}, +bt} WCon{True{}, +at}:
411 h0 => bits.absurd(C.CapBits.subset(1n+n1, Word.or(1n+n1, Word.or(1n+n1, Word.and(1n+n1, WCon{False{}, it}, WCon{True{}, fit}), Word.and(1n+n1, WCon{False{}, fpt}, WCon{False{}, bt})), WCon{True{}, at}), Word.or(1n+n1, WCon{False{}, bt}, WCon{False{}, it})), h0)
412 case WCon{False{}, +it} WCon{True{}, +fit} WCon{False{}, +fpt} WCon{False{}, +bt} WCon{False{}, +at}:
413 h0 => bits.bound_va(n1, it, fit, fpt, bt, at)(h0)
414 case WCon{False{}, +it} WCon{False{}, +fit} WCon{True{}, +fpt} WCon{True{}, +bt} WCon{True{}, +at}:
415 h0 => bits.absurd(C.CapBits.subset(1n+n1, Word.or(1n+n1, Word.or(1n+n1, Word.and(1n+n1, WCon{False{}, it}, WCon{False{}, fit}), Word.and(1n+n1, WCon{True{}, fpt}, WCon{True{}, bt})), WCon{True{}, at}), Word.or(1n+n1, WCon{True{}, bt}, WCon{False{}, it})), h0)
416 case WCon{False{}, +it} WCon{False{}, +fit} WCon{True{}, +fpt} WCon{True{}, +bt} WCon{False{}, +at}:
417 h0 => bits.bound_va(n1, it, fit, fpt, bt, at)(h0)
418 case WCon{False{}, +it} WCon{False{}, +fit} WCon{True{}, +fpt} WCon{False{}, +bt} WCon{True{}, +at}:
419 h0 => bits.absurd(C.CapBits.subset(1n+n1, Word.or(1n+n1, Word.or(1n+n1, Word.and(1n+n1, WCon{False{}, it}, WCon{False{}, fit}), Word.and(1n+n1, WCon{True{}, fpt}, WCon{False{}, bt})), WCon{True{}, at}), Word.or(1n+n1, WCon{False{}, bt}, WCon{False{}, it})), h0)
420 case WCon{False{}, +it} WCon{False{}, +fit} WCon{True{}, +fpt} WCon{False{}, +bt} WCon{False{}, +at}:
421 h0 => bits.bound_va(n1, it, fit, fpt, bt, at)(h0)
422 case WCon{False{}, +it} WCon{False{}, +fit} WCon{False{}, +fpt} WCon{True{}, +bt} WCon{True{}, +at}:
423 h0 => bits.absurd(C.CapBits.subset(1n+n1, Word.or(1n+n1, Word.or(1n+n1, Word.and(1n+n1, WCon{False{}, it}, WCon{False{}, fit}), Word.and(1n+n1, WCon{False{}, fpt}, WCon{True{}, bt})), WCon{True{}, at}), Word.or(1n+n1, WCon{True{}, bt}, WCon{False{}, it})), h0)
424 case WCon{False{}, +it} WCon{False{}, +fit} WCon{False{}, +fpt} WCon{True{}, +bt} WCon{False{}, +at}:
425 h0 => bits.bound_va(n1, it, fit, fpt, bt, at)(h0)
426 case WCon{False{}, +it} WCon{False{}, +fit} WCon{False{}, +fpt} WCon{False{}, +bt} WCon{True{}, +at}:
427 h0 => bits.absurd(C.CapBits.subset(1n+n1, Word.or(1n+n1, Word.or(1n+n1, Word.and(1n+n1, WCon{False{}, it}, WCon{False{}, fit}), Word.and(1n+n1, WCon{False{}, fpt}, WCon{False{}, bt})), WCon{True{}, at}), Word.or(1n+n1, WCon{False{}, bt}, WCon{False{}, it})), h0)
428 case WCon{False{}, +it} WCon{False{}, +fit} WCon{False{}, +fpt} WCon{False{}, +bt} WCon{False{}, +at}:
429 h0 => bits.bound_va(n1, it, fit, fpt, bt, at)(h0)