1	import Base
2	import ./core.bend as Shape
3	import ./nat_proofs.bend as Nats
4	import ./LAWS.bend as Laws
5	
6	def within(-dims: List<&2, Nat>, capacity: Shape.Capacity<dims>) -> Bool:
7	  match capacity:
8	    case Shape.Within{size, exact, bound}:
9	      True{}
10	    case Shape.Beyond{}:
11	      False{}
12	
13	def bound_within(-dims: List<&2, Nat>, -size: Nat, -exact: {size == Shape.numel(dims) : Nat}, +decision: Shape.BoolCase<Nat.is_le(size, 1048576n)>, fits: {True{} == Nat.is_le(size, 1048576n) : Bool}) -> {True{} == within(dims, Shape.capacity.bound(dims, size, exact, decision)) : Bool}:
14	  match decision:
15	    case Shape.BFalse{equal}:
16	      Empty.absurd({True{} == False{} : Bool}, Nats.contradiction(Nat.is_le(size, 1048576n), fits, equal))
17	    case Shape.BTrue{equal}:
18	      {==}
19	
20	def scale_within(+head: Nat, -tail: List<&2, Nat>, +size: Nat, -exact: {size == Shape.numel(tail) : Nat}, +small: Shape.BoolCase<Bool.or(Nat.is_eq(size, 0n), Nat.is_le(head, 1048576n))>, fits_small: {True{} == Bool.or(Nat.is_eq(size, 0n), Nat.is_le(head, 1048576n)) : Bool}, fits_product: {True{} == Nat.is_le(Nat.mul(head, size), 1048576n) : Bool}) -> {True{} == within(head <> tail, Shape.capacity.scale(head, tail, size, exact, small)) : Bool}:
21	  match small:
22	    case Shape.BFalse{equal}:
23	      Empty.absurd({True{} == False{} : Bool}, Nats.contradiction(Bool.or(Nat.is_eq(size, 0n), Nat.is_le(head, 1048576n)), fits_small, equal))
24	    case Shape.BTrue{equal}:
25	      bound_within(head <> tail, Nat.mul(head, size), Equal.cong(Nat, Nat, value => Nat.mul(head, value), size, Shape.numel(tail), exact), Shape.bool_case(Nat.is_le(Nat.mul(head, size), 1048576n)), fits_product)
26	
27	def scale_fits(+p: Nat, +size: Nat, bound: Shape.LE(Nat.mul(1n+p, size), 1048576n)) -> {True{} == Bool.or(Nat.is_eq(size, 0n), Nat.is_le(1n+p, 1048576n)) : Bool}:
28	  match size:
29	    case 0n:
30	      {==}
31	    case 1n+q:
32	      Nats.le_true(1n+p, 1048576n, Nats.le_add_left(1n+p, Nat.mul(1n+p, q), 1048576n, Nats.le_rewrite(Nat.add(1n+p, Nat.mul(1n+p, q)), Nat.mul(1n+p, 1n+q), 1048576n, Nats.mul_succ_right(1n+p, q), bound)))
33	
34	def zero_small(+size: Nat) -> {True{} == Bool.or(Nat.is_eq(size, 0n), Nat.is_le(0n, 1048576n)) : Bool}:
35	  match size:
36	    case 0n:
37	      {==}
38	    case 1n+q:
39	      {==}
40	
41	def zero_within(-tail: List<&2, Nat>, +rest: Shape.Capacity<tail>) -> {True{} == within(0n <> tail, Shape.capacity.step(0n, tail, rest)) : Bool}:
42	  match rest:
43	    case Shape.Beyond{}:
44	      {==}
45	    case Shape.Within{+size, exact, bound}:
46	      scale_within(0n, tail, size, exact, Shape.bool_case(Bool.or(Nat.is_eq(size, 0n), Nat.is_le(0n, 1048576n))), zero_small(size), {==})
47	
48	def step_within(+p: Nat, +tail: List<&2, Nat>, +rest: Shape.Capacity<tail>, ih: {True{} == within(tail, rest) : Bool}, bound: Shape.LE(Nat.mul(1n+p, Shape.numel(tail)), 1048576n)) -> {True{} == within((1n+p) <> tail, Shape.capacity.step(1n+p, tail, rest)) : Bool}:
49	  match rest:
50	    case Shape.Beyond{}:
51	      Empty.absurd({True{} == within((1n+p) <> tail, Shape.capacity.step(1n+p, tail, Shape.Beyond{})) : Bool}, Shape.clash(ih))
52	    case Shape.Within{+size, +exact, fits}:
53	      +scaled = Nats.le_rewrite(Nat.mul(1n+p, size), Nat.mul(1n+p, Shape.numel(tail)), 1048576n, Equal.cong(Nat, Nat, value => Nat.mul(1n+p, value), Shape.numel(tail), size, Equal.sym(Nat, size, Shape.numel(tail), exact)), bound)
54	      scale_within(1n+p, tail, size, exact, Shape.bool_case(Bool.or(Nat.is_eq(size, 0n), Nat.is_le(1n+p, 1048576n))), scale_fits(p, size, scaled), Nats.le_true(Nat.mul(1n+p, size), 1048576n, scaled))
55	
56	def capacity_complete(+dims: List<&2, Nat>, +bound: Shape.LE(Shape.numel(dims), 1048576n)) -> {True{} == within(dims, Shape.capacity(dims)) : Bool}:
57	  match dims:
58	    case Nil{}:
59	      {==}
60	    case +head <> +tail:
61	      match head:
62	        case 0n:
63	          zero_within(tail, Shape.capacity(tail))
64	        case 1n+p:
65	          step_within(p, tail, Shape.capacity(tail), capacity_complete(tail, Nats.le_add_left(Shape.numel(tail), Nat.mul(p, Shape.numel(tail)), 1048576n, bound)), bound)
66	
67	def capacity_built(+input: List<&2, U32>, rank_bound: Shape.LE(Shape.rank_dimensions(input), 4n), +capacity: Shape.Capacity<Shape.naturals(input)>, fits: {True{} == within(Shape.naturals(input), capacity) : Bool}) -> {Laws.built(input, Shape.construct.capacity(input, rank_bound, capacity)) == Some{input} : Maybe<&2, List<&2, U32>>}:
68	  match capacity:
69	    case Shape.Beyond{}:
70	      Empty.absurd({Laws.built(input, Shape.construct.capacity(input, rank_bound, Shape.Beyond{})) == Some{input} : Maybe<&2, List<&2, U32>>}, Shape.clash(fits))
71	    case Shape.Within{size, exact, bound}:
72	      {==}
73	
74	def construction_complete(+input: List<&2, U32>, +decision: Shape.BoolCase<Nat.is_le(Shape.rank_dimensions(input), 4n)>, rank_fits: {True{} == Nat.is_le(Shape.rank_dimensions(input), 4n) : Bool}, capacity_bound: Shape.LE(Shape.logical_numel(input), 1048576n)) -> {Laws.built(input, Shape.construct.ranked(input, decision)) == Some{input} : Maybe<&2, List<&2, U32>>}:
75	  match decision:
76	    case Shape.BFalse{equal}:
77	      Empty.absurd({Laws.built(input, Shape.construct.ranked(input, Shape.BFalse{equal})) == Some{input} : Maybe<&2, List<&2, U32>>}, Nats.contradiction(Nat.is_le(Shape.rank_dimensions(input), 4n), rank_fits, equal))
78	    case Shape.BTrue{equal}:
79	      capacity_built(input, Shape.LE.from(Shape.rank_dimensions(input), 4n, equal), Shape.capacity(Shape.naturals(input)), capacity_complete(Shape.naturals(input), capacity_bound))