miniroon_spec.pl (6439B)
1 :- module(miniroon_spec, 2 [ dcgappend/3 3 , netstring_prefix_for_payload/3 4 , netstring_bytes/3 5 , netstring_maplist_dcg/4 6 , phrase_length/4 7 , netstring_call_dcg/3 8 , miniroon_encoding/2 9 , miniroon_header/3 10 , miniroon_v0_caveat_list/3 11 ]). 12 :- use_module(library(debug), [assertion/1]). 13 :- use_module(library(dcg/basics), [digits/3]). 14 15 % pack_install(delay). => https://storage.googleapis.com/packs.ndrix.com/delay/delay-0.3.3.zip 16 % Also at: https://github.com/mndrix/delay 17 :- use_module(library(delay), [delay/1]). 18 19 :- multifile delay:mode/1. 20 21 delay:mode(lists:append(ground,_)). 22 delay:mode(lists:append(_,ground)). 23 24 delay:mode(system:string_bytes(ground,_,ground)). 25 delay:mode(system:string_bytes(_,ground,ground)). 26 27 %delay:mode(system:number_codes(ground,_)). 28 %delay:mode(system:number_codes(_,ground)). 29 30 %delay:mode(system:length(_,ground)). 31 %delay:mode(system:length(list,_)). 32 33 delay:mode(miniroon_spec:netstring_prefix_digits(list, _, _)). 34 delay:mode(miniroon_spec:netstring_prefix_digits(_, list, _)). 35 36 delay:mode(miniroon_spec:miniroon_v0_action(ground, _)). 37 delay:mode(miniroon_spec:miniroon_v0_action(_, list)). 38 39 delay:mode(miniroon_spec:phrase_length(nonvar, ground, _, _)). 40 delay:mode(miniroon_spec:phrase_length(ground, _, _, _)). 41 42 :- op(950, xfx, will_be). %< Shorthand operator for type and value checking 43 :- op(800, fx, ~). %< Shorthand operator for delayed goal 44 45 ~(Goal) :- delay(Goal). 46 47 %%% Helpers for DCGs: 48 49 % swapped arguments append for use in DCGs 50 % when called with instanced list as first argument it unifies it's content with DCG. 51 dcgappend([], L, L) :- !. 52 dcgappend([H|T], [H|R], L) :- 53 dcgappend(T, R, L). 54 55 % Non-cutting variant: 56 %dcgappend(List, L0, L1) :- append(List, L1, L0). 57 58 phrase_length_agg(List, Terminator, CurrentDepth, Length) :- 59 ( List == Terminator 60 -> CurrentDepth = Length 61 ; NextDepth is CurrentDepth + 1, 62 assertion(compound(List)), 63 List = [_|NextList], 64 phrase_length_agg(NextList, Terminator, NextDepth, Length) 65 ). 66 67 phrase_length(DCGBody, List, Rest, Length) :- 68 phrase(DCGBody, List, Terminator), 69 phrase_length_agg(List, Terminator, 0, Length), 70 Terminator = Rest. 71 72 %%% Helpers for type and value checking: 73 74 % apply check to value when bound 75 will_be(Value, Goal) :- 76 freeze(Value, assertion(call(Goal, Value))). 77 78 byte(Value) :- must_be(between(0, 255), Value). 79 nonzero_byte(Value) :- must_be(between(1, 255), Value). 80 81 nonnegative_integer(Value) :- must_be(nonneg, Value). 82 83 sequence_of_bytes([]). 84 sequence_of_bytes([First|Rest]) :- 85 First will_be byte, 86 Rest will_be sequence_of_bytes. 87 88 sequence_of_nonzero_bytes([]). 89 sequence_of_nonzero_bytes([First|Rest]) :- 90 First will_be nonzero_byte, 91 Rest will_be sequence_of_nonzero_bytes. 92 93 file_path(X) :- sequence_of_nonzero_bytes(X). 94 95 %%% Generic grammar definitions: 96 97 nonzero_digit(Code) --> 98 [Code], 99 { assertion(ground(Code)) }, 100 { member(Code, `123456789`) }. 101 102 %%% Netstring definitions: 103 104 % Netstring is a self-delimiting encoding of a sequence of bytes (bytestring). 105 % 106 netstring_bytes(PayloadBytes) --> %> Netstring is a sequence of bytes. 107 { PayloadBytes will_be sequence_of_bytes }, 108 netstring_prefix_for_payload(PayloadBytes), %> It consists of prefix, 109 PayloadBytes, %> payload, 110 `,`. %> and terminator. Terminator is single ASCII comma `,`. 111 112 netstring_string(PayloadString) --> 113 { ~ string_bytes(PayloadString, PayloadBytes, octet) }, 114 netstring_bytes(PayloadBytes). 115 116 %> Netstring prefix is the shortest ASCII decimal representation for length of 117 %^ payload in bytes, followed by ASCII colon `:`. 118 %^ That is number starting with non-zero digit unless payload is empty, 119 %^ in which case it's `0`. 120 netstring_prefix_for_payload(PayloadBytes, A, B) :- 121 ~ netstring_prefix_digits(Prefix, A, B), 122 ~ number_codes(PayloadLength, Prefix), 123 length(PayloadBytes, PayloadLength). 124 125 netstring_prefix_digits(`0`) --> `0:`, !. 126 netstring_prefix_digits([C|Cs]) --> 127 nonzero_digit(C), 128 !, 129 digits(Cs), 130 `:`. 131 132 netstring_call_dcg(DCGBody, L0, Rest) :- 133 ~ phrase_length(DCGBody,Payload,[44|Rest],PayloadLength), 134 ~ number_codes(PayloadLength, PrefixDigits), 135 netstring_prefix_digits(PrefixDigits, L0, Payload). 136 137 netstring_maplist_dcg(_, []) --> {true}. 138 netstring_maplist_dcg(DCGBody, [Item|Rest]) --> 139 netstring_call_dcg(call(DCGBody, Item)), 140 netstring_maplist_dcg(DCGBody, Rest). 141 142 %%% Miniroon definitions: 143 144 miniroon_encoding(Miniroon, Bytes) :- 145 Bytes will_be sequence_of_bytes, 146 phrase(netstring_call_dcg(miniroon_content(Miniroon)), Bytes). 147 148 % Miniroon is a netstring whose payload is concatenation of three parts: header, caveat list and signature. 149 miniroon_content(miniroon_v0(Identifier, Action, Caveats, Signature)) --> 150 netstring_call_dcg(miniroon_header(header_v0(Identifier, Action))), 151 %netstring_call_dcg(miniroon_v0_caveat_list(Caveats)), 152 netstring_call_dcg(netstring_maplist_dcg(miniroon_v0_caveat, Caveats)), 153 netstring_bytes(Signature). 154 155 miniroon_v0_action(revoke) --> `revoke`. 156 miniroon_v0_action(invoke) --> `invoke`. 157 miniroon_v0_action(invoke_once) --> `invoke-once`. 158 159 miniroon_header(header_v0(Identifier, Action)) --> 160 netstring_bytes(`capv0`), 161 netstring_bytes(Identifier), 162 netstring_call_dcg(miniroon_v0_action(Action)). 163 164 miniroon_v0_caveat(caveat_v0_env_is(VarName, Value)) --> 165 netstring_bytes(`env-is`), 166 netstring_string(VarName), 167 netstring_string(Value). 168 miniroon_v0_caveat(caveat_v0_env_absent(VarName)) --> 169 netstring_bytes(`env-absent`), 170 netstring_string(VarName). 171 miniroon_v0_caveat(caveat_v0_env_regmatch(VarName, Pattern)) --> 172 netstring_bytes(`env-re`), 173 netstring_string(VarName), 174 netstring_string(Pattern). 175 miniroon_v0_caveat(caveat_v0_env_glob(VarName, Pattern)) --> 176 netstring_bytes(`env-glob`), 177 netstring_string(VarName), 178 netstring_string(Pattern). 179 180 miniroon_v0_caveat_list([]) --> {true}. 181 miniroon_v0_caveat_list([Caveat|Rest]) --> 182 netstring_call_dcg(miniroon_v0_caveat(Caveat)), 183 miniroon_v0_caveat_list(Rest). 184 185 miniroon_is_catdir(CatalogDirectory) :- assertion(false). % TODO 186 miniroon_is_rundir(RunDirectory) :- assertion(false). % TODO 187 miniroon_is_environ(ExecutionEnvironment) :- assertion(false). % TODO 188 miniroon_is_verdict(deny). 189 miniroon_is_verdict(allow(Program, ResultEnvironment)) :- 190 miniroon_is_environ(ResultEnvironment), 191 file_path(Program). 192 miniroon_read_execution(InitialEnvironment, CatalogDirectory, Input, Verdict) :- 193 miniroon_is_environ(InitialEnvironment), 194 miniroon_is_catdir(CatalogDirectory), 195 Verdict will_be miniroon_is_verdict, 196 assertion(false). % TODO